Module Mthread.Mt_libSource

Sourceval array_threads : unit -> Frama_c_kernel.Cil_types.varinfo

Variable __fc_mthread_threads in mthread.c

Sourceval array_mutexes : unit -> Frama_c_kernel.Cil_types.varinfo

Variable __fc_mthread_mutexes in mthread.c

Sourceval array_queues : unit -> Frama_c_kernel.Cil_types.varinfo

Variable __fc_mthread_queues in mthread.c

Sourceval var_thread_created : unit -> Frama_c_kernel.Cil_types.varinfo

Variable __fc_mthread_threads_running in mthread.c

Sourceval check_mthread_library : unit -> unit

Checks that all variables above are in the source files.

Sourcetype threads_lib =
  1. | BuiltinsOnly
    (*

    Only Mthread built-ins are available.

    *)
  2. | Pthreads
    (*

    Pthreads stubs and Mthread built-ins.

    *)

Threading library stubbed by Mthread.

Sourceval load_threads_library : threads_lib -> unit

Load the given threads library into Frama-C.

Sourceval 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.