module Translate_annots:sig
..end
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 : Cil_types.kernel_function -> Env.t -> Cil_types.funspec -> Env.t
Translate 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 Translate_annots.post_funspec
at the right time to pop the right
contract.
val post_funspec : Cil_types.kernel_function -> Env.t -> Env.t
Translate the postconditions of the current function contract in the environment.
The function contract previously built by Translate_annots.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 : Cil_types.kernel_function ->
Cil_types.stmt -> Env.t -> Cil_types.code_annotation -> Env.t
Translate 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 Translate_annots.post_code_annotation
at the right time
to pop the right contract.
val post_code_annotation : Cil_types.kernel_function ->
Cil_types.stmt -> Env.t -> Cil_types.code_annotation -> Env.t
Translate the postconditions of the current code annotation in the environment.
If necessarry, the statement contract previously built by
Translate_annots.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.