package frama-c

You can search for identifiers within the package.

in-package search v0.2.0

On This Page

Alarms
Forward Offset Operations
Forward Locations Operations
Backward Operations

Platform dedicated to the analysis of source code written in C

Install

dune-project

Dependency

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

Authors

Maintainers

F

frama-ci-bot@frama-c.com

Sources

frama-c-28.0-Nickel.tar.gz

sha256=29612882330ecb6eddd0b4ca3afc0492b70d0feb3379a1b8e893194c6e173983

doc/frama-c-eva.gui/Eva_gui/Gui_eval/Make/argument-1-X/Loc/index.html

Module `X.Loc`

type value = Val.t

type location

abstract locations

type offset

abstract offsets

val top : location

val equal_loc : location -> location -> bool

val equal_offset : offset -> offset -> bool

val pretty_loc : Format.formatter -> location -> unit

val pretty_offset : Format.formatter -> offset -> unit

val to_value : location -> value Eva.Eval.or_bottom

val size : location -> Frama_c_kernel.Int_Base.t

val replace_base : Frama_c_kernel.Base.substitution -> location -> location

replace_base substitution location replaces the variables represented by the location according to substitution.

Alarms

These functions are used to create the alarms that report undesirable behaviors, when a location abstraction does not meet the prerequisites of an operation. Thereafter, the location is assumed to meet them to continue the analysis. See the documentation of Abstract_value.truth for more details.

val assume_no_overlap : 
  partial:bool ->
  location ->
  location ->
  [ `False
  | `Unknown of location * location
  | `True
  | `TrueReduced of location * location
  | `Unreachable ]

Assumes that two locations do not overlap. If partial is true, the concrete locations may be equal, but different locations must not overlap. Otherwise, the locations must be completely separate.

val assume_valid_location : 
  for_writing:bool ->
  bitfield:bool ->
  location ->
  [ `False
  | `Unknown of location
  | `True
  | `TrueReduced of location
  | `Unreachable ]

Assumes that the given location is valid for a read or write operation, according to the for_writing boolean. Used to emit memory access alarms. If the location is not completely valid, reduces it to its valid part. bitfield indicates whether the location may be the one of a bitfield; if it is false, the location can be assumed to be byte aligned.

Forward Offset Operations

val no_offset : offset

val forward_field : 
  Frama_c_kernel.Cil_types.typ ->
  Frama_c_kernel.Cil_types.fieldinfo ->
  offset ->
  offset

Computes the field offset of a fieldinfo, with the given remaining offset. The given type must the one of the structure or the union.

val forward_index : Frama_c_kernel.Cil_types.typ -> value -> offset -> offset

forward_index typ value offset computes the array index offset of (Index (ind, off)), where the index expression ind evaluates to value and the remaining offset off evaluates to offset. typ must be the type pointed by the array.

Forward Locations Operations

Evaluation of the location of an lvalue, when the offset has already been evaluated. In case of a pointer, its expression has also been evaluated to a value.

val forward_variable : 
  Frama_c_kernel.Cil_types.typ ->
  Frama_c_kernel.Cil_types.varinfo ->
  offset ->
  location Eva.Eval.or_bottom

Var case in the AST: the host is a variable.

val forward_pointer : 
  Frama_c_kernel.Cil_types.typ ->
  value ->
  offset ->
  location Eva.Eval.or_bottom

Mem case in the AST: the host is a pointer.

val eval_varinfo : Frama_c_kernel.Cil_types.varinfo -> location

Backward Operations

For an unary forward operation F, the inverse backward operator B tries to reduce the argument values of the operation, given its result.

It must satisfy: if B arg res = v then ∀ a ⊆ arg such that F a ⊆ res, a ⊆ v

i.e. B arg res returns a value v larger than all subvalues of arg whose result through F is included in res.

If F arg ∈ res is impossible, then v should be bottom.

Any n-ary operator may be considered as a unary operator on a vector of values, the inclusion being lifted pointwise.

val backward_variable : 
  Frama_c_kernel.Cil_types.varinfo ->
  location ->
  offset Eva.Eval.or_bottom

val backward_pointer : 
  value ->
  offset ->
  location ->
  (value * offset) Eva.Eval.or_bottom

val backward_field : 
  Frama_c_kernel.Cil_types.typ ->
  Frama_c_kernel.Cil_types.fieldinfo ->
  offset ->
  offset Eva.Eval.or_bottom

val backward_index : 
  Frama_c_kernel.Cil_types.typ ->
  index:value ->
  remaining:offset ->
  offset ->
  (value * offset) Eva.Eval.or_bottom

val structure : location Eva__.Abstract.Location.structure

val mem : 'a Eva__.Structure.Key_Location.key -> bool

Tests whether a key belongs to the module.

val get : 'a Eva__.Structure.Key_Location.key -> (location -> 'a) option

For a key of type k key:

if the values of type t contain a subpart of type k from a module identified by the key, then get key returns an accessor for it.
otherwise, get key returns None.

val set : 'a Eva__.Structure.Key_Location.key -> 'a -> location -> location

For a key of type k key:

if the values of type t contain a subpart of type k from a module identified by the key, then set key v t returns the value t in which this subpart has been replaced by v.
otherwise, set key _ is the identity function.

Iterators on the components of a structure.

type polymorphic_iter_fun = {

iter : 'a. 'a Eva__.Structure.Key_Location.key -> (module Eva__.Abstract_location.S with type location = 'a) -> 'a -> unit;

}

val iter : polymorphic_iter_fun -> location -> unit

type 'b polymorphic_fold_fun = {

fold : 'a. 'a Eva__.Structure.Key_Location.key -> (module Eva__.Abstract_location.S with type location = 'a) -> 'a -> 'b -> 'b;

}

val fold : 'b polymorphic_fold_fun -> location -> 'b -> 'b

type polymorphic_map_fun = {

map : 'a. 'a Eva__.Structure.Key_Location.key -> (module Eva__.Abstract_location.S with type location = 'a) -> 'a -> 'a;

}

val map : polymorphic_map_fun -> location -> location