Frama-C API - Mt_analysis_hooks
val 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
val catch_functions_calls : Mt_thread.analysis_state -> Eva.Cvalue_callbacks.call_hookFunction 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.