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-27.1-Cobalt.tar.gz

sha256=5b13574a16a58971c27909bee94ae7f37b17d897852b40c768a3d4e2e09e39d2

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) 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 ref