module Base:sig
..end
Abstraction of the base of an addressable memory zone, together with the validity of the zone.
type
cstring =
| |
CSString of |
|||
| |
CSWstring of |
(* | This type abstracts over the two kinds of constant strings present in strings. It is used in a few modules below Base. | *) |
type
variable_validity = private {
|
mutable weak : |
(* | Indicate that the variable is weak, i.e. that it may represent multiple memory locations | *) |
|
mutable min_alloc : |
(* | First bit guaranteed to be valid; can be -1 | *) |
|
mutable max_alloc : |
(* | Last possibly valid bit | *) |
|
max_allocable : |
(* | Maximum valid bit after size increase | *) |
Validity for variables that might change size.
type
deallocation =
| |
Malloc |
| |
VLA |
| |
Alloca |
Whether the allocated base has been obtained via calls to
malloc/calloc/realloc (Malloc
), alloca (Alloca
), or is related to a
variable-length array (VLA
).
type
base = private
| |
Var of |
(* | Base for a standard C variable. | *) |
| |
CLogic_Var of |
(* | Base for a logic variable that has a C type. | *) |
| |
Null |
(* | Base for an address like | *) |
| |
String of |
(* | contents of the constant string | *) |
| |
Allocated of |
(* | Base for a variable dynamically allocated via malloc/calloc/realloc/alloca | *) |
type
validity =
| |
Empty |
(* | For 0-sized bases | *) |
| |
Known of |
(* | Valid between those two bits | *) |
| |
Unknown of |
(* | Unknown(b,k,e) indicates:
If k is
| *) |
| |
Variable of |
(* | Variable(min_alloc, max_alloc) means:
| *) |
| |
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_Set
with module O = Hptset
module Validity:Datatype.S
with type t = validity
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.
val pretty_validity : Format.formatter -> validity -> unit
val validity : t -> validity
val validity_from_size : Abstract_interp.Int.t -> validity
validity_from_size size
returns Empty
if size
is zero,
or Known (0, size-1)
if size > 0
.
size
must not be negative.
val validity_from_type : Cil_types.varinfo -> validity
type
range_validity =
| |
Invalid_range |
| |
Valid_range of |
val valid_range : validity -> range_validity
valid_range v
returns Invalid_range
if v
is Invalid
,
Valid_range None
if v
is Empty
, or Valid_range (Some (mn, mx))
otherwise, where mn
and mx
are the minimum and maximum (possibly)
valid bounds of v
.
val is_weak_validity : validity -> bool
is_weak_validity v
returns true iff v
is a Weak
validity.
val create_variable_validity : weak:bool ->
min_alloc:Abstract_interp.Int.t ->
max_alloc:Abstract_interp.Int.t -> variable_validity
val update_variable_validity : variable_validity ->
weak:bool ->
min_alloc:Abstract_interp.Int.t -> max_alloc:Abstract_interp.Int.t -> unit
Update the corresponding fields of the variable validity. Bases already weak cannot be made 'strong' through this function, and the validity bounds can only grow.
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
exception Not_a_C_variable
val to_varinfo : t -> Cil_types.varinfo
Not_a_C_variable
otherwise.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
val null : t
val is_null : t -> bool
val null_set : Hptset.t
Set containing only the base Base.null
.
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
val bits_sizeof : t -> Int_Base.t
val offset_is_in_validity : Abstract_interp.Int.t -> validity -> Ival.t -> bool
is_offset_in_validity size validity ival
checks that ival
is a valid
offset for an access of size size
according to validity
.
val is_valid_offset : for_writing:bool -> Abstract_interp.Int.t -> t -> Ival.t -> bool
is_valid_offset ~for_writing size b offset
checks that offset
(expressed in bits) plus size
bits is valid in b
.
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 is_weak : t -> bool
Is the given base a weak one (in the sens that its validity is Weak
).
Only possible for Allocated
bases.
val id : t -> int
val is_aligned_by : t -> Abstract_interp.Int.t -> bool
This is only useful to create an initial memory state for analysis, and is never needed for normal users.
val register_allocated_var : Cil_types.varinfo -> deallocation -> validity -> t
Allocated variables are variables not present in the source of the
program, but instead created through dynamic allocation. Their field
vsource
is set to false.
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.
Their field vsource
is set to false.