Frama-C API - Builtins_malloc
Dynamic allocation related builtins. Most functionality is exported as builtins.
val fold_dynamic_bases : (Frama_c_kernel.Base.t -> Callstack.t -> 'a -> 'a) -> 'a -> 'afold_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 : Frama_c_kernel.Cvalue.V.t -> Alarmset.statusval free_automatic_bases : Callstack.t -> Frama_c_kernel.Cvalue.Model.t -> Frama_c_kernel.Cvalue.Model.tPerforms the equivalent of free for each location that was allocated via alloca() in the current function (as per Eva_utils.call_stack ()). This function must be called during finalization of a function call.
val freeable : Frama_c_kernel.Cvalue.V.t -> Frama_c_kernel.Abstract_interp.truthEvaluates the ACSL predicate \freeable(value): holds if and only if the value points to an allocated memory block that can be safely released using the C function free. Note that \freeable(\null) does not hold, despite NULL being a valid argument to the C function free.