Frama-C:
Plug-ins:
Libraries:

Frama-C API - Mt_summary

Summary of an Mthread analysis, used by server requests for the dedicated component in Ivette.

val compute : Mt_thread.analysis_state -> unit

Computes the summary from an analysis state.

val clear : unit -> unit

Clears summary.

Summary for each thread.

type mutex_summary = {
  1. taken : Mutex.Set.t;
    (*

    Set of locks taken.

    *)
  2. released : Mutex.Set.t;
    (*

    Set of locks released.

    *)
}
type queue_summary = {
  1. created : Mqueue.Set.t;
    (*

    Set of message queues created.

    *)
  2. receivers : Mqueue.Set.t;
    (*

    Set of message queues receiving some message.

    *)
  3. senders : Mqueue.Set.t;
    (*

    Set of message queues sending some messages.

    *)
}
type shared_var_summary = {
  1. read : Frama_c_kernel.Locations.Zone.Set.t;
    (*

    Shared locations read.

    *)
  2. written : Frama_c_kernel.Locations.Zone.Set.t;
    (*

    Shared locations written.

    *)
}
type thread_summary = {
  1. locks : mutex_summary;
  2. mqueues : queue_summary;
  3. shared_vars : shared_var_summary;
}

Table binding each analyzed thread to its summary.

Summary of accesses to shared memory.

type access

An access is a combination between a zone accessed, a kind of access (read, write) and a protection status.

Memory zone of an access.

Kind of an access: read or write.

val access_protection : access -> Mt_shared_vars_types.protection

Mutex protection of an access.

val access_id : access -> string

Unique id of an access.

Table binding each access to the set of source code locations where it occurs.