E_ACSL.ContractTranslate 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