module Base:sig
..end
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
base = private
| |
Var of |
(* |
Base for a standard C variable.
| *) |
| |
Initialized_Var of |
(* |
Base for a variable with a non-standard initial value. This exact
value is defined in module
Cvalue.Default_offsetmap . | *) |
| |
CLogic_Var of |
(* |
Base for a logic variable that has a C type.
| *) |
| |
Null |
(* |
Base for an addresse like
(int* )0x123 | *) |
| |
String of |
(* |
contents of the constant string
| *) |
type
validity =
| |
Known of |
(* |
Valid between those two bits
| *) |
| |
Unknown of |
(* |
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
| *) |
| |
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
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 variableval typeof : t -> Cil_types.typ option
Bit_utils.pretty_bits
, typically.val pretty_validity : Format.formatter -> validity -> unit
val validity : t -> validity
val validity_from_type : Cil_types.varinfo -> validity
val valid_range : validity -> Int_Intervals_sig.itv option
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
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
Base.null
.val min_valid_absolute_address : unit -> Abstract_interp.Int.t
val max_valid_absolute_address : unit -> Abstract_interp.Int.t
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
Not_valid_offset
if the offset may be invalid.val base_max_offset : t -> Ival.t
Ival.bottom
for invalid bases. Returns an interval for bases with an unknown validity.val is_read_only : t -> bool
const
attribute is not currently taken into account.val id : t -> int
val is_aligned_by : t -> Abstract_interp.Int.t -> bool
val register_initialized_var : Cil_types.varinfo -> validity -> t
val register_memory_var : Cil_types.varinfo -> validity -> t
vsource
is set to false.