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 (23)

Authors

Maintainers

F

frama-ci-bot@frama-c.com

Sources

frama-c-29.0-Copper.tar.gz

sha256=d2fbb3b8d0ff83945872e9e6fa258e934a706360e698dae3b4d5f971addf7493

doc/frama-c-eva.core/Eva/Logic_inout/index.html

Module `Eva.Logic_inout`

Functions used by the Inout and From plugins to interpret predicate and assigns clauses. This API may change according to these plugins development.

val predicate_deps : 
  pre:Frama_c_kernel.Cvalue.Model.t ->
  here:Frama_c_kernel.Cvalue.Model.t ->
  Frama_c_kernel.Cil_types.predicate ->
  Frama_c_kernel.Locations.Zone.t option

predicate_deps ~pre ~here p computes the logic dependencies needed to evaluate the predicate p in cvalue state here, in a function whose pre-state is pre. Returns None on either an evaluation error or on unsupported construct.

val valid_behaviors : 
  Frama_c_kernel.Cil_types.kernel_function ->
  Frama_c_kernel.Cvalue.Model.t ->
  Frama_c_kernel.Cil_types.behavior list

Returns the list of behaviors of the given function that are active for the given initial state.

val assigns_inputs_to_zone : 
  Frama_c_kernel.Cvalue.Model.t ->
  Frama_c_kernel.Cil_types.assigns ->
  Frama_c_kernel.Locations.Zone.t

Evaluation of the memory zone read by the \from part of an assigns clause, in the given cvalue state.

val assigns_outputs_to_zone : 
  result:Frama_c_kernel.Cil_types.varinfo option ->
  Frama_c_kernel.Cvalue.Model.t ->
  Frama_c_kernel.Cil_types.assigns ->
  Frama_c_kernel.Locations.Zone.t

Evaluation of the memory zone written by an assigns clauses, in the given cvalue state.

type tlval_zones = {

under : Frama_c_kernel.Locations.Zone.t;
(*
Under-approximation of the memory zone.
*)
over : Frama_c_kernel.Locations.Zone.t;
(*
Over-approximation of the memory zone.
*)
deps : Frama_c_kernel.Locations.Zone.t;
(*
Dependencies needed to evaluate the address.
*)

}

Zones of an lvalue term of an assigns clause.

val assigns_tlval_to_zones : 
  Frama_c_kernel.Cvalue.Model.t ->
  Frama_c_kernel.Locations.access ->
  Frama_c_kernel.Cil_types.term ->
  tlval_zones option

Evaluation of the memory zones and dependencies of an lvalue term from an assigns clause, in the given cvalue state for a read or write access.

val verify_assigns : 
  Frama_c_kernel.Cil_types.kernel_function ->
  pre:Frama_c_kernel.Cvalue.Model.t ->
  Assigns.t ->
  unit

Evaluate the assigns clauses of the given function in its given pre-state, and compare them with the dependencies computed by the from plugin. Emits warnings if needed, and sets statuses to the assigns clauses.

val accept_base : 
  formals:bool ->
  locals:bool ->
  Frama_c_kernel.Kernel_function.t ->
  Frama_c_kernel.Base.t ->
  bool

accept_base ~formals ~locals kf b returns true if and only if b is:

a global
a formal or local of one of the callers of kf
a formal or local of kf and the corresponding argument is true.