Module Builtins_nonfree_malloc

module Builtins_nonfree_malloc: sig .. end
Builtin for free function

Dynamic allocation related builtins. Most functionality is exported as builtins.


exception Invalid_CEA_alloc
val make_size : Cvalue.V.t -> Abstract_interp.Int.t
module Dynamic_Alloc_Infinite_Table: State_builder.Hashtbl(Datatype.String.Hashtbl)(Locations.Location_Bytes)(sig
val dependencies : State.t list
val size : int
val name : string
end)
module Dynamic_Alloc_Bases: State_builder.Ref(Base.Hptset)(sig
val dependencies : State.t list
val name : string
val default : unit -> Base.Hptset.t
end)
val register_malloced_base : Base.Hptset.elt -> unit
val frama_c_alloc_infinite : Cvalue.V_Offsetmap.v ->
Cvalue.Model.t ->
(Cil_types.exp * Cvalue.V.t * 'a) list -> Value_types.call_result
val uninitialized : Cvalue.V_Or_Uninitialized.t
val offsm_from_validity : Base.validity -> Cvalue.V_Offsetmap.v -> Cvalue.V_Offsetmap.t
module MallocReturnsNull: Value_parameters.False(sig
val option_name : string
val help : string
end)
val alloc_abstract : loc:Cil_types.location ->
string ->
Cil_types.typ ->
Abstract_interp.Int.t * Abstract_interp.Int.t ->
Cvalue.Model.t ->
Locations.Location_Bytes.t * Cvalue.Model.t * Cil_types.varinfo
val malloc_var : loc:Cil_types.location ->
string ->
Cil_types.typ ->
Abstract_interp.Int.t * Abstract_interp.Int.t ->
Cvalue.Model.t -> Value_types.call_result * Cil_types.varinfo
val alloc_with_validity : Cvalue.Model.t ->
(Cil_types.exp * Cvalue.V.t * 'a) list -> Value_types.call_result
module MallocedByStack: State_builder.Hashtbl(Value_types.Callstack.Hashtbl)(Cil_datatype.Varinfo)(sig
val name : string
val size : int
val dependencies : State.t list
end)
val fresh_base : (Kernel_function.t * Cil_types.kinstr) list -> string
module MallocFunctions: Value_parameters.Filled_string_set(sig
val option_name : string
val arg_name : string
val help : string
val default : Datatype.String.Set.t
end)
val filter_callstack : (Kernel_function.t * 'a) list -> (Kernel_function.t * 'a) list
val guess_intended_malloc_type : ('a * Cil_types.kinstr) list ->
Abstract_interp.Int.t -> Cil_types.typ * Abstract_interp.Int.t
type alloc_size = 
| Constant_size of Abstract_interp.Int.t
| Variable_size
val size_non_constant_malloc : Abstract_interp.Int.t
val alloc_once_by_stack : Db.Value.builtin_sig
val free : exact:bool -> Base.Hptset.t -> Cvalue.Model.t -> Cvalue.Model.t
val resolve_bases_to_free : Cvalue.V.t -> Base.Hptset.t * int
val abstract_free : Cvalue.Model.t -> Cvalue.V.t -> Cvalue.Model.t
val frama_c_free : Cvalue.Model.t -> ('a * Cvalue.V.t * 'b) list -> Value_types.call_result
Builtin for free function
exception Problem
val realloc : Cvalue.Model.t ->
(Cil_types.exp * Cvalue.V.t * 'a) list -> Value_types.call_result
exception Not_leaked
val check_if_base_is_leaked : Base.t -> Cvalue.Model.lmap -> bool
val check_leaked_malloced_bases : Cvalue.Model.t -> 'a -> Value_types.call_result
module RankedMallocedByStack: State_builder.Hashtbl(Value_types.Callstack.Hashtbl)(Datatype.Pair(Cil_datatype.Varinfo)(Datatype.Int))(sig
val name : string
val size : int
val dependencies : State.t list
end)
val dkey : Log.category
exception Allocation_rank of int
module MallocPrecision: Value_parameters.Int(sig
val option_name : string
val default : int
val arg_name : string
val help : string
end)
val alloc_multiple_by_stack : Db.Value.builtin_sig