module Base: sig
.. end
Abstraction of the base of an addressable memory zone, together with
the validity of the zone.
type
cstring =
type
base = private
type
validity =
| |
Known of Abstract_interp.Int.t * Abstract_interp.Int.t |
| |
Unknown of Abstract_interp.Int.t * Abstract_interp.Int.t option * Abstract_interp.Int.t |
| |
Periodic of Abstract_interp.Int.t * Abstract_interp.Int.t * Abstract_interp.Int.t |
| |
Invalid |
module Base: sig
.. end
include Datatype.S_with_collections
module Hptset: Hptset.S
with type elt = t
and type 'a shape = 'a Hptmap.Shape(Base).t
module SetLattice: Lattice_type.Lattice_Hashconsed_Set
with module O = Hptset
val pretty_addr : Format.formatter -> t -> unit
pretty_addr fmt base
pretty-prints the name of base
on fmt
, with
a leading ampersand if it is a variable
val typeof : t -> Cil_types.typ option
Type of the memory block that starts from the given base. Useful to give to
the function
Bit_utils.pretty_bits
, typically.
Validity
val pretty_validity : Format.formatter -> validity -> unit
val validity : t -> validity
val validity_from_type : Cil_types.varinfo -> validity
val valid_range : validity -> Lattice_Interval_Set.Int_Intervals.t
Finding bases
val of_varinfo : Cil_types.varinfo -> t
val of_string_exp : Cil_types.exp -> t
val of_c_logic_var : Cil_types.logic_var -> t
Must only be called on logic variables that have a C type
Origin of the variable underlying a base
exception Not_a_C_variable
val to_varinfo : t -> Cil_types.varinfo
Raises Not_a_C_variable
otherwise.
Returns the variable's varinfo if the base corresponds to a C variable
(in particular, not a logic variable).
val is_formal_or_local : t -> Cil_types.fundec -> bool
val is_any_formal_or_local : t -> bool
val is_any_local : t -> bool
val is_global : t -> bool
val is_formal_of_prototype : t -> Cil_types.varinfo -> bool
val is_local : t -> Cil_types.fundec -> bool
val is_formal : t -> Cil_types.fundec -> bool
val is_block_local : t -> Cil_types.block -> bool
val is_function : t -> bool
NULL base
val null : t
val is_null : t -> bool
val min_valid_absolute_address : unit -> Abstract_interp.Int.t
val max_valid_absolute_address : unit -> Abstract_interp.Int.t
Bounds for option absolute-valid-range
Size of a base
val bits_sizeof : t -> Int_Base.t
exception Not_valid_offset
val is_valid_offset : for_writing:bool -> Abstract_interp.Int.t -> t -> Ival.t -> unit
Is the given bits-expressed offset guaranteed to be valid? Does nothing in
this case, and raises Not_valid_offset
if the offset may be invalid.
val base_max_offset : t -> Ival.t
Maximal valid offset (in bits) of the given base. Returns Ival.bottom
for invalid bases. Returns an interval for bases with an unknown validity.
Misc
val is_read_only : t -> bool
Is the base valid as a read/write location, or only for reading.
The const
attribute is not currently taken into account.
val id : t -> int
val is_aligned_by : t -> Abstract_interp.Int.t -> bool
Registering bases
This is only useful to create an initial memory state for analysis,
and is never needed for normal users.
val register_initialized_var : Cil_types.varinfo -> validity -> t
val register_memory_var : Cil_types.varinfo -> validity -> t
Memory variables are variables not present in the source of the program.
They are created only to fill the contents of another variable, or
through dynamic allocation. Their field vlogic
is set to true.