module Initial_state: sig
.. end
Creation of the initial state for Value
exception Initialization_failed
val typeHasAttribute : string -> Cil_types.typ -> bool
val add_initialized : Cvalue.Model.t -> Locations.location -> Cvalue.V.t -> Cvalue.Model.t
val add_unitialized : Cvalue.Model.t -> Locations.location -> Cvalue.Model.t
val make_well : filled:bool ->
Base.Hptset.elt -> Cvalue.Model.t -> Locations.location -> Cvalue.Model.t
val warn_unknown_size_aux : (Format.formatter -> 'a -> unit) -> 'a -> string * Cil_types.typ -> unit
val warn_unknown_size : Cil_types.varinfo -> string * Cil_types.typ -> unit
type
validity_hidden_base =
| |
Invalid |
| |
UnknownValidity |
| |
KnownThenUnknownValidity of Integer.t |
val create_hidden_base : valid:validity_hidden_base ->
hidden_var_name:string -> name_desc:string -> Cil_types.typ -> Base.t
val initialize_var_using_type : Cil_types.varinfo -> Cvalue.Model.t -> Cvalue.Model.t
initialize_var_using_type varinfo state
uses the type of varinfo
to create an initial value in state
.
val init_var_zero : Cil_types.varinfo -> Cvalue.Model.t -> Cvalue.Model.t
val initialized_padding : unit -> Value_parameters.InitializedPaddingGlobals.t
val init_trailing_padding : Cvalue.Model.t ->
last_bitsoffset:int ->
abs_offset:int -> Cil_types.typ -> Cil_types.lval -> Cvalue.Model.t
val eval_single_initializer : Cvalue.Model.t -> Cil_types.lval -> Cil_types.exp -> Cvalue.Model.t
val eval_initializer : Cvalue.Model.t -> Cil_types.lval -> Cil_types.init -> Cvalue.Model.t
val eval_const_initializer : Cvalue.Model.t -> Cil_types.lval -> Cil_types.init -> Cvalue.Model.t
val initial_state_only_globals : unit -> Cvalue.Model.t
Initial value for globals and NULL in no-lib-entry mode (everything
initialized to 0).
module ContextfreeGlobals: State_builder.Option_ref
(
Cvalue.Model
)
(
sig
val name : string
val dependencies : State.t list
end
)
val initial_state_contextfree_only_globals : unit -> ContextfreeGlobals.data
Initial state in -lib-entry
mode