Struct Config 

pub struct Config {
    pub embed_spec: bool,
    pub emit_print: bool,
    pub emit_panic: bool,
}

Fields

embed_spec: bool

emit_print: bool

emit_panic: bool

Implementations

impl Config

pub fn instrument_item_struct( &self, spec: DataSpec, item_struct: ItemStruct, ) -> Result<TokenStream>

pub fn instrument_item_enum( &self, spec: DataSpec, item_enum: ItemEnum, ) -> Result<TokenStream>

impl Config

pub fn instrument_fn( &self, spec: &Spec, sig: &Signature, body: &mut Block, ) -> Result<()>

pub fn build_spec_fn_sig(prefix: &str, sig: &Signature) -> Signature

pub fn build_qualifier_const_item<SomeConstItem: Parse>( attrs: &[Attribute], prefix: &str, qualifiers: FnQualifiers, fn_ident: &Ident, ) -> SomeConstItem

pub fn build_qualifier_check_stmt( fn_ident: &Ident, impl_type: &Type, trait_path: &Path, ) -> Stmt

pub fn build_precondition_fn_body(conditions: &[PreCondition]) -> Block

pub fn build_poscondition_fn_body( captures: &[Capture], conditions: &[PostCondition], return_type: &ReturnType, ) -> Result<Block>

impl Config

pub fn instrument_loops_in_fn_body(&self, body: &mut Block) -> Result<()>

pub fn instrument_expr_while(&self, spec: LoopSpec, expr_while: &mut ExprWhile)

pub fn instrument_expr_for_loop( &self, spec: LoopSpec, expr_for_loop: &mut ExprForLoop, )

impl Config

pub fn instrument_trait( &self, spec: DataSpec, the_trait: ItemTrait, ) -> Result<ItemTrait>

Expand trait items by mangling each method and adding a wrapper default impl.

Mangling a function involves the following:

1. Rename the function following the pattern: fn add -> fn __anodized_add.
2. Make a new function with the original name that has a default impl; the default impl performs runtime validation and calls the mangled function.

pub fn instrument_trait_impl( &self, spec: DataSpec, the_impl: ItemImpl, ) -> Result<ItemImpl>

Expand impl items by mangling methods for trait impls.

The #[spec] attribute on an impl fn must narrow the #[spec] of the trait fn:

• The impl’s preconditions must follow from the trait’s preconditions.
• The impl’s postconditions must entail the trait’s postconditions.

impl Config

pub fn emit_anything(&self) -> bool

pub fn instrument_item_fn( &self, spec: Spec, item_fn: ItemFn, ) -> Result<TokenStream>

pub fn instrument_item_trait( &self, spec: DataSpec, item_trait: ItemTrait, ) -> Result<TokenStream>

pub fn instrument_item_trait_impl( &self, spec: DataSpec, item_impl: ItemImpl, ) -> Result<TokenStream>