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 -> 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