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 -> Env.t -> t -> Env.t
Translate the preconditions of the given contract into the environement
val translate_postconditions : Cil_types.kernel_function -> Env.t -> Env.t
Translate the postconditions of the given contract into the environment