Module Base

module Base: sig .. end
Abstraction of the base of an addressable memory zone, together with the validity of the zone.

type cstring = 
| CSString of string
| CSWstring of Escape.wstring (*This type abstracts over the two kinds of constant strings present in strings. It is used in a few modules below Base.*)
type base = private 
| Var of Cil_types.varinfo * validity (*Base for a standard C variable.*)
| Initialized_Var of Cil_types.varinfo * validity (*Base for a variable with a non-standard initial value. This exact value is defined in module Cvalue.Default_offsetmap.*)
| CLogic_Var of Cil_types.logic_var * Cil_types.typ * validity (*Base for a logic variable that has a C type.*)
| Null (*Base for an addresse like (int* )0x123*)
| String of int * cstring (*contents of the constant string*)
type validity = 
| Known of Abstract_interp.Int.t * Abstract_interp.Int.t (*Valid between those two bits*)
| Unknown of Abstract_interp.Int.t * Abstract_interp.Int.t option * Abstract_interp.Int.t (*Unknown(b,k,e) indicates: If k is None, potentially valid between b and e If k is Some k, then b <= k <= e, and the base is
  • valid between b and k;
  • potentially valid between k+1 and e: Accesses on potentially valid parts will succeed, but will also raise an alarm.
*)
| Periodic of Abstract_interp.Int.t * Abstract_interp.Int.t * Abstract_interp.Int.t (*Period*)
| Invalid (*Valid nowhere. Typically used for the NULL base, or for function pointers.*)
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.