exec_spec_unverified

vstd::contrib::exec_spec

Macro exec_spec_unverified 

exec_spec_unverified!() { /* proc-macro */ }
Expand description

Automatically compiles spec items to exec items, but without proofs of functional correctness. This means that,iIn contrast to exec_spec_verified!, all specifications on compiled executable code generated by exec_spec_unverified! are trusted.

Supports all of the features supported by exec_spec_verified!, as well as these additional features:

  • More general bounded quantifiers. Quantifier expressions must match this form: forall |x1: <type1>, x2: <type2>, ..., xN: <typeN>| <guard1> && <guard2> && ... && <guardN> ==> <body> or exists |x1: <type1>, x2: <type2>, ..., xN: <typeN>| <guard1> && <guard2> && ... && <guardN> && <body>, where:
    • <guardI> is of the form: <lowerI> <op> xI <op> <upperI>, where:
      • <op> is either <= or <
      • <lowerI> and <upperI> can mention xJ for all J < I
    • <typeI> is a Rust primitive integer (i<N>, isize, u<N>, usize) or char. Note that char is not supported by quantifiers in exec_spec_verified!.