Frama-C:
Plug-ins:
Libraries:

Frama-C API - 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?

type ctx
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 t = {
  1. before : bool;
  2. ki : Cil_types.stmt;
  3. zone : Locations.Zone.t;
}
type zone_info = t list option

list of zones at some program points. None means that the computation has failed.

type slices = {
  1. ctrl : Cil_datatype.Stmt.Set.t;
  2. stmt : Cil_datatype.Stmt.Set.t;
}

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.

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?

exception NYI of string

The following declarations are kept for compatibility and should not be used

val not_yet_implemented : string Stdlib.ref