Module Assert

module Assert: sig .. end

Module with the context to hold the data contributing to an assertion and general functions to create assertion statements.

Module with the context to hold the data contributing to an assertion and general functions to create assertion statements.


type t 

Type to hold the data contributing to an assertion.

External type representing the assertion context. Either Some data if we want to register some data in the context of None if we do not want to.

val empty : loc:Cil_types.location ->
Cil_types.kernel_function -> Env.t -> t * Env.t

Empty assertion context.

val no_data : t

No data assertion context.

Contrary to an empty assertion context, a "no data" assertion context will always have no data in it, even when calling register on it. The goal is to have a context to pass to functions that need one even if we do not need it afterwards. For instance there is no following assertion statement.

val with_data_from : loc:Cil_types.location ->
Cil_types.kernel_function -> Env.t -> t -> t * Env.t

with_data_from ~loc kf env from creates a new assertion context with the same data than the from assertion context. If from is a "no data" assertion context, then the new context is also a "no data" assertion context.

val merge_right : loc:Cil_types.location ->
Cil_types.kernel_function ->
Env.t -> t -> t -> t * Env.t

merge_right ~loc kf env adata1 adata2 merges the assertion data of adata1 into adata2 if adata2 is not a "no data" assertion context.

val clean : loc:Cil_types.location ->
Cil_types.kernel_function -> Env.t -> t -> Env.t

clean ~loc kf env adata generates a call to the C cleanup function for the assertion context. This function *must* be used if the assertion context is not given to runtime_check or runtime_check_with_msg, otherwise the memory allocated in the C structure will not be freed.

val register : loc:Cil_types.location ->
Cil_types.kernel_function ->
Env.t ->
?force:bool -> string -> Cil_types.exp -> t -> t * Env.t

register ~loc kf env ?force name e adata registers the data e corresponding to the name name to the assertion context adata. If force is false (default), the data is not registered if the expression is a constant. If force is true, the data is registered even if the expression is a constant.

val register_term : loc:Cil_types.location ->
Cil_types.kernel_function ->
Env.t ->
?force:bool ->
Cil_types.term -> Cil_types.exp -> t -> t * Env.t

register_term ~loc kf env ?force t e adata registers the data e corresponding to the term t to the assertion context adata. The parameter force has the same signification than for the function register.

val register_pred : loc:Cil_types.location ->
Cil_types.kernel_function ->
Env.t ->
?force:bool ->
Cil_types.predicate -> Cil_types.exp -> t -> t * Env.t

register_pred ~loc kf env ?force p e adata registers the data e corresponding to the predicate p to the assertion context adata. The parameter force has the same signification than for the function register.

val runtime_check : adata:t ->
pred_kind:Cil_types.predicate_kind ->
Smart_stmt.annotation_kind ->
Cil_types.kernel_function ->
Env.t -> Cil_types.exp -> Cil_types.predicate -> Cil_types.stmt * Env.t

runtime_check ~adata ~pred_kind kind kf env e p generates a runtime check for predicate p by building a call to __e_acsl_assert. e (or !e if reverse is set to true) is the C translation of p. adata is the assertion context holding the data contributing to the assertion. pred_kind indicates if the assert should be blocking or not. kind is the annotation kind of p. kf is the current kernel_function. env is the current environment.

val runtime_check_with_msg : adata:t ->
loc:Cil_types.location ->
string ->
pred_kind:Cil_types.predicate_kind ->
Smart_stmt.annotation_kind ->
Cil_types.kernel_function -> Env.t -> Cil_types.exp -> Cil_types.stmt * Env.t

runtime_check_with_msg ~adata ~loc msg ~pred_kind kind kf env e generates a runtime check for e (or !e if reverse is true) by building a call to __e_acsl_assert. adata is the assertion context holding the data contributing to the assertion. loc is the location printed in the message if the runtime check fails. msg is the message printed if the runtime check fails. pred_kind indicates if the assert should be blocking or not. kind is the annotation kind of p. kf is the current kernel_function. env is the current environment.