E_ACSL.Contract
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:Frama_c_kernel.Cil_types.location ->
Frama_c_kernel.Cil_types.spec ->
t
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