Frama_c_kernel.Logic_deps
val compute_term_deps :
(Cil_types.stmt -> Cil_types.term -> Locations.Zone.t option) Stdlib.ref
val is_slice_directive : Cil_types.acsl_extension -> bool
Is an ACSL extension a directive for the slicing plug-in?
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.
Related to slice directives slice_preserve_stmt and slice_preserve_ctrl
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) * slices
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) * slices
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) * slices
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_annot: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?