Frama-C:
Plug-ins:
Libraries:

Frama-C API - Mt_lib

val array_threads : unit -> Frama_c_kernel.Cil_types.varinfo

Variable __fc_mthread_threads in mthread.c

val array_mutexes : unit -> Frama_c_kernel.Cil_types.varinfo

Variable __fc_mthread_mutexes in mthread.c

val array_queues : unit -> Frama_c_kernel.Cil_types.varinfo

Variable __fc_mthread_queues in mthread.c

val var_thread_created : unit -> Frama_c_kernel.Cil_types.varinfo

Variable __fc_mthread_threads_running in mthread.c

val check_mthread_library : unit -> unit

Checks that all variables above are in the source files.

type threads_lib =
  1. | BuiltinsOnly
    (*

    Only Mthread built-ins are available.

    *)
  2. | Pthreads
    (*

    Pthreads stubs and Mthread built-ins.

    *)

Threading library stubbed by Mthread.

val load_threads_library : threads_lib -> unit

Load the given threads library into Frama-C.

val warn_on_unsupported_library_function : Frama_c_kernel.Cil_types.kernel_function -> unit

Aborts if kf is from a library whose stubs have not been loaded; warn if kf is an unsupported function from a loaded library.