Frama-C API - Contract

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

Create 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.t

Translate the preconditions of the given contract into the environement

val translate_postconditions : Frama_c_kernel.Cil_types.kernel_function -> Env.t -> Env.t

Translate the postconditions of the given contract into the environment