Module Contract

module Contract: sig .. end

Translate a given ACSL contract (function or statement) into the corresponding C statement for runtime assertion checking.

type t = 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