Frama-C API - Contract
Translate a given ACSL contract (function or statement) into the corresponding C statement for runtime assertion checking.
type t = Contract_types.contractval create : loc:Frama_c_kernel.Cil_types.location -> Frama_c_kernel.Cil_types.spec -> tCreate a contract from a spec object (either function spec or statement spec)
val translate_preconditions : Frama_c_kernel.Cil_types.kernel_function -> Env.t -> t -> Env.tTranslate the preconditions of the given contract into the environement
val translate_postconditions : Frama_c_kernel.Cil_types.kernel_function -> Env.t -> Env.tTranslate the postconditions of the given contract into the environment