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 must_translate : Property.t -> bool
Return true if the given property must be translated (ie. if the valid
properties must be translated or if its status is not True
), false
otherwise.
val must_translate_opt : Property.t option -> bool
Same than must_translate
but for Property.t option
. Return false if the
option is None
.
val pre_funspec : Cil_types.kernel_function ->
Cil_types.kinstr -> 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 -> Cil_types.kinstr -> 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.