Module Initial_state

module Initial_state: sig .. end
Creation of the initial state for Value

val dkey : Log.category
exception Initialization_failed
val add_initialized : Cvalue.Model.t -> Locations.location -> Cvalue.V.t -> Cvalue.Model.t
Those functions intentionally ignore 'const' attributes. Functions of Eval_op should not be used in this module, unless they have a 'reducing' argument.
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 loc_of_typoffset : Base.t -> Cil_types.typ -> Cil_types.offset -> Locations.location
val reject_empty_struct : Base.t -> Cil_types.offset -> Cil_types.typ -> unit
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