Logic_deps (frama-c.Frama_c_kernel.Logic

val compute_term_deps : 
  ( Cil_types.stmt -> Cil_types.term -> Locations.Zone.t option ) Stdlib.ref

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 = {

before : bool;

ki : Cil_types.stmt;

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 decl = {

var : Cil_datatype.Varinfo.Set.t;

lbl : Cil_datatype.Logic_label.Set.t;

}

type pragmas = {

ctrl : Cil_datatype.Stmt.Set.t;

stmt : Cil_datatype.Stmt.Set.t;

}

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?

exception NYI of string

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

val not_yet_implemented : string Stdlib.ref