Frama-C API - 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
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
val packed_descr : Structural_descr.pack
Packed version of the descriptor.
val reprs : t list
List of representants of the descriptor.
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
.
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 : Stdlib.Format.formatter -> t -> unit
val pretty_debug : Stdlib.Format.formatter -> t -> unit
val pretty_filter : Stdlib.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
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
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.
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
.
val find_base : Base.t -> t -> offsetmap Lattice_bounds.or_top_bottom
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.
add_base b o m
adds base b
bound to o
, replacing any previous bindings of b
. No effect on Top
or Bottom
.
Creates the offsetmap described by size
, v
and size_v
, and binds it to the base. No effect on Top
or Bottom
.
Filters
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 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
.
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.
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
.
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
isV.bottom
, the value is the most precise value ofV
approximating the sequence of bits present atl..l+loc.size-1
- if
l..l+loc.size-1
points toV.bottom
everywhere, the value isbottom
. - if
conflate_bottom
istrue
and at least one bit pointed to byl..l+loc.size-1
isV.bottom
, the value isV.bottom
- if
conflate_bottom
isfalse
and at least one bit pointed to byl..l+loc.size-1
is notV.bottom
, the value is an approximation of the join of all the bits atl..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