Frama_c_kernel.Logic_deps
val compute_term_deps :
( Cil_types.stmt -> Cil_types.term -> Locations.Zone.t option ) Stdlib.ref
val mk_ctx_func_contract : ?before:bool -> Cil_types.kernel_function -> ctx
To build an interpretation context relative to function contracts.
val mk_ctx_stmt_contract :
?before:bool ->
Cil_types.kernel_function ->
Cil_types.stmt ->
ctx
To build an interpretation context relative to statement contracts.
val mk_ctx_stmt_annot : Cil_types.kernel_function -> Cil_types.stmt -> ctx
To build an interpretation context relative to statement annotations.
type zone_info = t list option
list of zones at some program points. * None means that the computation has failed.
val from_term : Cil_types.term -> ctx -> zone_info * decl
Entry point to get zones needed to evaluate the term
relative to the ctx
of interpretation.
val from_terms : Cil_types.term list -> ctx -> zone_info * decl
Entry point to get zones needed to evaluate the list of terms
relative to the ctx
of interpretation.
val from_pred : Cil_types.predicate -> ctx -> zone_info * decl
Entry point to get zones needed to evaluate the predicate
relative to the ctx
of interpretation.
val from_preds : Cil_types.predicate list -> ctx -> zone_info * decl
Entry point to get zones needed to evaluate the list of predicates
relative to the ctx
of interpretation.
val from_stmt_annot :
Cil_types.code_annotation ->
(Cil_types.stmt * Cil_types.kernel_function) ->
(zone_info * decl) * pragmas
Entry point to get zones needed to evaluate an annotation on the given stmt.
val from_stmt_annots :
( Cil_types.code_annotation -> bool ) option ->
(Cil_types.stmt * Cil_types.kernel_function) ->
(zone_info * decl) * pragmas
Entry point to get zones needed to evaluate annotations of this stmt
.
val from_func_annots :
( ( Cil_types.stmt -> unit ) -> Cil_types.kernel_function -> unit ) ->
( Cil_types.code_annotation -> bool ) option ->
Cil_types.kernel_function ->
(zone_info * decl) * pragmas
Entry point to get zones needed to evaluate annotations of this kf
.
val code_annot_filter :
Cil_types.code_annotation ->
threat:bool ->
user_assert:bool ->
slicing_pragma:bool ->
loop_inv:bool ->
loop_var:bool ->
others:bool ->
bool
To quickly build an annotation filter
val to_result_from_pred : Cil_types.predicate -> bool
Does the interpretation of the predicate rely on the interpretation of the term result?