Module bytecode::verification_analysis

Analysis which computes an annotation for each function on whether this function should be verified or inlined. It also calculates the set of global invariants that are applicable to each function as well as collect information on how these invariants should be handled (i.e., checked after bytecode, checked at function exit, or deferred to caller).

Structs

• InvariantAnalysisData
  Analysis info saved for the global_invariant_instrumentation phase
• InvariantRelevance
  A named tuple for holding the information on how an invariant is relevant to a function.
• VerificationAnalysisProcessor
• VerificationInfo
  The annotation for information about verification.

Functions

• get_info
  Get verification information for this function.
• is_invariant_checking_delegated
• is_invariant_checking_disabled
• is_invariant_suspendable