package frama-c

You can search for identifiers within the package.

in-package search v0.2.0

On This Page

Finding values *
Writing values into the state
Reducing the state
Misc

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-30.0-beta-Zinc.tar.gz

sha256=93a291a8764644df2f3618d7ea18258b5fbe0912ec98dfdfd180967afdf24474

doc/frama-c.kernel/Frama_c_kernel/Cvalue/Model/index.html

Module `Cvalue.Model`

Memories. They are maps from bases to memory slices

Functions inherited from Lmap_sig interface

include Lmap_sig.S
  with type v = V_Or_Uninitialized.t
   and type offsetmap = V_Offsetmap.t
   and type widen_hint_base = V_Or_Uninitialized.widen_hint

type v = V_Or_Uninitialized.t

type of the values associated to a location

type offsetmap = V_Offsetmap.t

type of the maps associated to a base

type widen_hint_base = V_Or_Uninitialized.widen_hint

widening hints for each base

type map

Maps from Base.t to offsetmap

type lmap = private

| Bottom
| Top
| Map of map

include Datatype.S_with_collections with type t = lmap

include Datatype.S with type t = lmap

include Datatype.S_no_copy with type t = lmap

include Datatype.Ty with type t = lmap

type t = lmap

see https://frama-c.com/download/frama-c-plugin-development-guide.pdf

val ty : t Type.t

see https://frama-c.com/download/frama-c-plugin-development-guide.pdf

val name : string

Unique name of the datatype.

val descr : t Descr.t

Datatype descriptor.

val packed_descr : Structural_descr.pack

Packed version of the descriptor.

val reprs : t list

List of representants of the descriptor.

val equal : t -> t -> bool

Equality: same spec than Stdlib.(=).

see https://frama-c.com/download/frama-c-plugin-development-guide.pdf

val compare : t -> t -> int

Comparison: same spec than Stdlib.compare.

val hash : t -> int

Hash function: same spec than Hashtbl.hash.

val mem_project : (Project_skeleton.t -> bool) -> t -> bool

mem_project f x must return true iff there is a value p of type Project.t in x such that f p returns true.

val copy : t -> t

Deep copy: no possible sharing between x and copy x.

module Set : Datatype.Set with type elt = t

module Map : Datatype.Map with type key = t

module Hashtbl : Datatype.Hashtbl with type key = t

val pretty : Format.formatter -> t -> unit

val pretty_debug : Format.formatter -> t -> unit

val pretty_filter : Format.formatter -> t -> Locations.Zone.t -> unit

pretty_filter m z pretties only the part of m that correspond to the bases present in z

val pretty_diff : Format.formatter -> t -> t -> unit

General shape

val top : t

val is_top : t -> bool

val empty_map : t

Empty map. Casual users do not need this except to create a custom initial state.

val is_empty_map : t -> bool

val bottom : t

Every location is associated to the value bottom of type v in this state. This state can be reached only in dead code.

val is_reachable : t -> bool

Join and inclusion

val join : t -> t -> t

val is_included : t -> t -> bool

module Make_Narrow (_ : sig ... end) : sig ... end

type widen_hint = Base.t -> widen_hint_base

Widening hint for each base.

val widen : ?priority:Base.Set.t -> ?hint:widen_hint -> t -> t -> t

widen ~priority ~hint m1 m2 performs a widening on m2, assuming that m1 was the previous state. The relation is_included m1 m2 must hold. priority is an optional set of bases that must be widened in priority. hint defines optional hint for each base.

val merge : into:t -> t -> t

merge ~into t adds all binding from t into into.

Finding values

val copy_offsetmap : 
  Locations.Location_Bits.t ->
  Integer.t ->
  t ->
  offsetmap Lattice_bounds.or_bottom

copy_offsetmap alarms loc size m returns the superposition of the ranges of size bits starting at loc within m. size must be strictly greater than zero. Return None if all pointed addresses are invalid in m.

raises Error_Top
when the location or the state are Top, and there is no Top value in the type v.

val find_base : Base.t -> t -> offsetmap Lattice_bounds.or_top_bottom

raises Not_found
if the varid is not present in the map.

val find_base_or_default : 
  Base.t ->
  t ->
  offsetmap Lattice_bounds.or_top_bottom

Same as find_base, but return the default values for bases that are not currently present in the map. Prefer the use of this function to find_base, unless you explicitly want to see if the base is bound.

Binding variables

val paste_offsetmap : 
  from:offsetmap ->
  dst_loc:Locations.Location_Bits.t ->
  size:Integer.t ->
  exact:bool ->
  t ->
  t

paste_offsetmap ~from ~dst_loc ~size ~exact m copies from, which is supposed to be exactly size bits, and pastes them at dst_loc in m. The copy is exact if and only if dst_loc is exact, and exact is true. Only the locations that may be valid are written.

val add_base : Base.t -> offsetmap -> t -> t

add_base b o m adds base b bound to o, replacing any previous bindings of b. No effect on Top or Bottom.

val add_base_value : 
  Base.t ->
  size:Integer.t ->
  v ->
  size_v:Integer.t ->
  t ->
  t

Creates the offsetmap described by size, v and size_v, and binds it to the base. No effect on Top or Bottom.

Filters

val filter_base : (Base.t -> bool) -> t -> t

Remove from the map all the bases that do not satisfy the predicate.

val filter_by_shape : 'a Hptmap.Shape(Base.Base).t -> t -> t

Remove from the map all the bases that are not also present in the given Base.t-indexed tree.

val remove_base : Base.t -> t -> t

Removes the base if it is present. Does nothing otherwise.

val replace_base : Base.substitution -> t -> t

replace_bases substitition map replaces some bases in map according to substitution. If substitution conflates different bases, the offsetmaps bound to these bases are joined.

Iterators

Notice that some iterators require an argument of type map: the cases Top and Bottom must be handled separately. All the iterators below only present bases that are bound to non-default values, according to the function is_default_offsetmap of the function Lmap.Make_Loffset.

val iter : (Base.base -> offsetmap -> unit) -> map -> unit

val fold : (Base.t -> offsetmap -> 'a -> 'a) -> map -> 'a -> 'a

Cached iterators

These functions are meant to be partially applied to all their arguments but the final one (the map). They must be called at the toplevel of OCaml modules, as they create persistent caches.

val cached_fold : 
  f:(Base.t -> offsetmap -> 'a) ->
  cache_name:string ->
  temporary:bool ->
  joiner:('a -> 'a -> 'a) ->
  empty:'a ->
  map ->
  'a

val cached_map : 
  f:(Base.t -> offsetmap -> offsetmap) ->
  cache:(string * int) ->
  temporary:bool ->
  t ->
  t

Misc

val shape : map -> offsetmap Hptmap.Shape(Base.Base).t

Shape of the map. This can be used for simultaneous iterations on other maps indexed by type Base.Base.t.

val clear_caches : unit -> unit

Clear the caches local to this module. Beware that they are not project-aware, and that you must call them at every project switch.

include Lattice_type.With_Narrow with type t := t

val narrow : t -> t -> t

over-approximation of intersection

Finding values *

val find_indeterminate : 
  ?conflate_bottom:bool ->
  t ->
  Locations.location ->
  V_Or_Uninitialized.t

find_indeterminate ~conflate_bottom state loc returns the value and flags associated to loc in state. The flags are the union of the flags at all the locations and offsets corresponding to loc. The value is the join of all the values pointed by l..l+loc.size-1 for all l among the locations in loc. For an individual l, the value pointed to is determined as such:

if no part of l..l+loc.size-1 is V.bottom, the value is the most precise value of V approximating the sequence of bits present at l..l+loc.size-1
if l..l+loc.size-1 points to V.bottom everywhere, the value is bottom.
if conflate_bottom is true and at least one bit pointed to by l..l+loc.size-1 is V.bottom, the value is V.bottom
if conflate_bottom is false and at least one bit pointed to by l..l+loc.size-1 is not V.bottom, the value is an approximation of the join of all the bits at l..l+loc.size-1.

As a rule of thumb, you must set conflate_bottom=true when the operation you abstract really accesses loc.size bits, and when undeterminate values are an error. This is typically the case when reading a scalar value. Conversely, if you are reading many bits at once (for example, to approximate the entire contents of a struct), set conflate_bottom to false -- to account for the possibility of padding bits. The default value is true.

val find : ?conflate_bottom:bool -> t -> Locations.location -> V.t

find ?conflate_bottom state loc returns the same value as find_indeterminate, but removes the indeterminate flags from the result.

Writing values into the state

val add_binding : exact:bool -> t -> Locations.location -> V.t -> t

add_binding state loc v simulates the effect of writing v at location loc in state. If loc is not writable, bottom is returned. For this function, v is an initialized value; the function add_indeterminate_binding allows to write a possibly indeterminate value to state.

val add_indeterminate_binding : 
  exact:bool ->
  t ->
  Locations.location ->
  V_Or_Uninitialized.t ->
  t

Reducing the state

The functions below can be used to refine the value bound to a given location. In both cases, the location must be exact.

val reduce_previous_binding : t -> Locations.location -> V.t -> t

reduce_previous_binding state loc v reduces the value associated to loc in state; use with caution, as the inclusion between the new and the old value is not checked.

val reduce_indeterminate_binding : 
  t ->
  Locations.location ->
  V_Or_Uninitialized.t ->
  t

Same behavior as reduce_previous_binding, but takes a value with 'undefined' and 'escaping addresses' flags.

Misc

val uninitialize_blocks_locals : Cil_types.block list -> t -> t

val remove_variables : Cil_types.varinfo list -> t -> t

For variables that are coming from the AST, this is equivalent to uninitializing them.

val cardinal_estimate : t -> CardinalEstimate.t

On This Page

Finding values *
Writing values into the state
Reducing the state
Misc

package frama-c

Install

dune-project Dependency

Authors

Maintainers

Sources

doc/frama-c.kernel/Frama_c_kernel/Cvalue/Model/index.html

Module Cvalue.Model

General shape

Join and inclusion

Finding values

Binding variables

Filters

Iterators

Cached iterators

Misc

Finding values *

Writing values into the state

Reducing the state

Misc

dune-project
Dependency

Module `Cvalue.Model`