module Contract:sig
..end
Translate a given ACSL contract (function or statement) into the corresponding C statement for runtime assertion checking.
typet =
Contract_types.contract
val create : loc:Cil_types.location -> Cil_types.spec -> t
Create a contract from a spec
object (either function spec or statement
spec)
val translate_preconditions : Cil_types.kernel_function -> Cil_types.kinstr -> Env.t -> t -> Env.t
Translate the preconditions of the given contract into the environement
val translate_postconditions : Cil_types.kernel_function -> Cil_types.kinstr -> Env.t -> Env.t
Translate the postconditions of the given contract into the environment
val must_translate_ppt_ref : (Property.t -> bool) Stdlib.ref
val must_translate_ppt_opt_ref : (Property.t option -> bool) Stdlib.ref