Mthread.Mt_analysis_hooksSourceval main_thread :
Frama_c_kernel.Cil_types.kernel_function ->
Mt_memory.Types.state ->
Mt_thread.thread_stateA correct value for the main thread
Exception to be returned when a hook did not process fully correctly, to be caught the level of hook registration. The int is the erro code
val mthread_builtins :
(string
* (Mt_thread.analysis_state ->
Mt_memory.Types.state ->
(Eva.Eva_ast.exp * Mt_memory.Types.value) list ->
Mt_memory.Types.state * Mt_memory.Types.value option))
listList of builtins that are to be registered by Mthread. We use a simplified interface compared to what the value analysis can require. The callbacks can raise Hook_failure if they did not proceed correctly
Function to register with Cvalue_callbacks.register_call_hooks (called before each function call processed in the analysis)
val catch_functions_record :
Mt_thread.analysis_state ->
Eva.Cvalue_callbacks.call_results_hookFunction to register with Cvalue_callbacks.register_call_results_hook (called after each function call processed by the analysis.