Module Builtins_malloc

module Builtins_malloc: sig .. end
Dynamic allocation related builtins. Most functionality is exported as builtins.

Dynamically allocated bases



val fold_dynamic_bases : (Base.t -> Value_types.Callstack.t -> 'a -> 'a) -> 'a -> 'a
fold_dynamic_bases f init folds f to each dynamically allocated base, with initial accumulator init. Note that this also includes bases created by alloca and VLAs.
val alloc_size_ok : Cvalue.V.t -> Alarmset.status
val free_automatic_bases : Value_types.Callstack.t -> Cvalue.Model.t -> Cvalue.Model.t
Performs the equivalent of free for each location that was allocated via alloca() in the current function (as per Value_util.call_stack ()). This function must be called during finalization of a function call.