Frama-C API - Translate_annots
Functions that translate a given ACSL annotation into the corresponding C statements (if any) for runtime assertion checking. These C statements are part of the resulting environment.
val pre_funspec : Frama_c_kernel.Cil_types.kernel_function -> Env.t -> Frama_c_kernel.Cil_types.funspec -> Env.tTranslate the preconditions of the given function contract in the environment. The contract is attached to the kernel_function.
The function contract is pushed in the environment, some care should be taken to call post_funspec at the right time to pop the right contract.
val post_funspec : Frama_c_kernel.Cil_types.kernel_function -> Env.t -> Env.tTranslate the postconditions of the current function contract in the environment.
The function contract previously built by pre_funspec is popped from the environment. Some care should be taken to call this function at the right time to pop the right contract.
val pre_code_annotation : Frama_c_kernel.Cil_types.kernel_function -> Frama_c_kernel.Cil_types.stmt -> Env.t -> Frama_c_kernel.Cil_types.code_annotation -> Env.tTranslate the preconditions of the given code annotation in the environment.
If available, the statement contract is pushed in the environment, some care should be taken to call post_code_annotation at the right time to pop the right contract.
val post_code_annotation : Frama_c_kernel.Cil_types.kernel_function -> Frama_c_kernel.Cil_types.stmt -> Env.t -> Frama_c_kernel.Cil_types.code_annotation -> Env.tTranslate the postconditions of the current code annotation in the environment.
If necessarry, the statement contract previously built by pre_code_annotation is popped from the environment. Some care should be taken to call this function at the right time to pop the right contract.