Mthread.Mt_analysis_hooks
val main_thread :
Frama_c_kernel.Cil_types.kernel_function ->
Mt_memory.Types.state ->
Mt_thread.thread_state
A 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))
list
List 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_hook
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_hook
Function to register with Cvalue_callbacks.register_call_results_hook
(called after each function call processed by the analysis.