Module `Mthread.Mt_analysis_hooks`Source

Source

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

Sourceexception Hook_failure of int

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

Source

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

Source

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)

Source

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.

Install

Dune Dependency

Authors

Maintainers

Sources

doc/mthread/Mthread/Mt_analysis_hooks/index.html

Module `Mthread.Mt_analysis_hooks`Source

package frama-c

Install

Dune Dependency

Authors

Maintainers

Sources

doc/mthread/Mthread/Mt_analysis_hooks/index.html

Module Mthread.Mt_analysis_hooksSource

Module `Mthread.Mt_analysis_hooks`Source