Type
General space-profiling statistics for the profiler invocation.
MLWORKS.Profile
MLWorks.Profile
datatype space_header = Space of {data_allocated: int, functions: int, collections: int, total_profiled : function_space_profile}
General space-profiling statistics for the profiler invocation. These statistics are gathered regardless of whether the profiling manner in use gathered space-profiling information for its function_profile
.
data_allocated
functions
collections
total_profiled
function_space_profiles
. This will be zero if space-profiling was not requested for any function.