module Builtins_nonfree_malloc:sig
..end
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 -> ('a * Cvalue.V.t * 'b) list -> Value_types.call_result
val uninitialized : Cvalue.V_Or_Uninitialized.un_t
val offsm_from_validity : Base.validity -> Cvalue.V_Offsetmap.v -> Cvalue.V_Offsetmap.t
val type_from_nb_elems : loc:Cil_types.location ->
Cil_types.typ -> Abstract_interp.Int.t -> Cil_types.typ
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.FilledStringSet
(
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 |
| |
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
free
functionexception 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.t -> 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