Frama_c_kernel.Base
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 variable_validity = private {
mutable weak : bool; | (* Indicate that the variable is weak, i.e. that it may represent multiple memory locations *) |
mutable min_alloc : Abstract_interp.Int.t; | (* First bit guaranteed to be valid; can be -1 *) |
mutable max_alloc : Abstract_interp.Int.t; | (* Last possibly valid bit *) |
max_allocable : Abstract_interp.Int.t; | (* Maximum valid bit after size increase *) |
}
Validity for variables that might change size.
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 Cil_types.varinfo * validity | (* Base for a standard C variable. *) |
| 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 address like |
| String of int * cstring | (*
|
| Allocated of Cil_types.varinfo * deallocation * validity | (* Base for a variable dynamically allocated via malloc/calloc/realloc/alloca *) |
and validity =
| Empty | (* For 0-sized bases *) |
| 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
|
| Variable of variable_validity | (* 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 with type t = base
include Datatype.S with type t = base
include Datatype.S_no_copy with type t = base
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 pretty : Stdlib.Format.formatter -> t -> unit
Pretty print each value in an user-friendly way.
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
module Hptshape :
Hptmap_sig.Shape with type key = t and type 'v map = 'v 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 : Stdlib.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 : Stdlib.Format.formatter -> validity -> unit
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
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
val to_varinfo : t -> Cil_types.varinfo
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 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
Access kind: read/write of k bits, or no access. Without any access, an offset must point into or just beyond the base ("one past the last element of the array object", non-array object being viewed as array of one element).
is_valid_offset access b offset
holds iff the ival offset
(expressed in bits) is completely valid for the access
of base b
(it only represents valid offsets for such an access). Returns false if offset
may be invalid for such an access.
Computes all offsets that may be valid for an access
of base t
. For bases with variable or unknown validity, the result may not satisfy is_valid_offset
, as some offsets may be valid or invalid. bitfield
is true by default: the computed offset may be offsets of bitfields. If it is set to false, the computed offsets are byte aligned (they are all congruent to 0 modulo 8).
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.
This is used to efficiently replace some bases by others in locations or in memory states, for instance in Locations
or Lmap_sig
.
type substitution = base Hptshape.map
Type used for the substitution between bases.
val substitution_from_list : (base * base) list -> substitution
Creates a substitution from an association list.