package frama-c

You can search for identifiers within the package.

in-package search v0.2.0

Platform dedicated to the analysis of source code written in C

Install

Dune Dependency

frama-c.com Readme Edit opam file Versions (25)

Authors

Maintainers

F

frama-ci-bot@frama-c.com

Sources

frama-c-31.0-Gallium.tar.gz

sha256=a94384f00d53791cbb4b4d83ab41607bc71962d42461f02d71116c4ff6dca567

doc/frama-c.kernel/Frama_c_kernel/Logic_deps/index.html

Module `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?

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

ctrl : Cil_datatype.Stmt.Set.t;
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.

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?

exception NYI of string

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

val not_yet_implemented : string Stdlib.ref