Module Translate_annots

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.