Frama-C:
Plug-ins:
Libraries:

Frama-C API - Mt_thread

type recompute_reason =
  1. | FirstIteration
  2. | NewMsgReceived
  3. | PotentialSharedVarsChanged
  4. | SharedVarsValuesChanged
  5. | InitialArgsChanged
  6. | InitialEnvChanged
  7. | InterferencesChanged
module RecomputeReason : sig ... end
module SetRecomputeReason : Stdlib.Set.S with type elt = recompute_reason
type priority =
  1. | PDefault
    (*

    No priority specified, but it is possible to specify one

    *)
  2. | PUnknown
    (*

    Contradictory priorities specified

    *)
  3. | PPriority of int
    (*

    Known priority

    *)
type thread
type thread_state = {
  1. th_eva_thread : Eva__.Thread.t;
  2. th_parent : thread_state option;
    (*

    Thread in which the thread is created. None for the root thread

    *)
  3. th_fun : Frama_c_kernel.Cil_types.kernel_function;
    (*

    Function which the thread executes

    *)
  4. th_stack : Eva.Callstack.t;
    (*

    Call stack resulting in the creation of the thread

    *)
  5. mutable th_init_state : Frama_c_kernel.Cvalue.Model.t;
    (*

    Memory state at the moment the thread is created

    *)
  6. mutable th_params : Frama_c_kernel.Cvalue.V.t list;
    (*

    Arguments to the the thread function

    *)
  7. mutable th_amap : Mt_types.Trace.t;
    (*

    map interesting statements to sets concurrent actions with their call stacks

    *)
  8. mutable th_to_recompute : SetRecomputeReason.t;
    (*

    Does this thread needs to be recomputed on the next iteration

    *)
  9. mutable th_read_written : Mt_shared_vars_types.AccessesByZone.map;
    (*

    Globals read and written by the thread, and at which statement

    *)
  10. mutable th_cfg : Mt_cfg_types.CfgNode.t;
    (*

    Cfg for the current thread

    *)
  11. mutable th_read_written_cfg : Mt_cfg_types.AccessesByZoneNode.map;
    (*

    Globals read and written by the thread, and at which node in the cfg

    *)
  12. mutable th_values_written : Mt_memory.Types.state;
    (*

    Join of all the values written by this thread in shared locations. Currently not contextual

    *)
  13. mutable th_projects : Frama_c_kernel.Project.t list;
    (*

    Copies of the analyses of the thread, most recent first

    *)
  14. mutable th_value_results : Eva__.Eva_results.results option;
    (*

    Result of the last Value analysis of this thread

    *)
  15. mutable th_priority : priority;
    (*

    determines which threads execute without the possibility of being preempted by another thread.

    *)
}

The representation of a thread

module ThreadState : sig ... end
type analysis_state = {
  1. all_threads : thread_state Eva__.Thread.Hashtbl.t;
    (*

    List of all threads. Is kept (and can thus increase) from one iteration to the next

    *)
  2. mutable all_mutexes : Eva__.Mutex.Set.t;
    (*

    Set of all mutexes of the analysis

    *)
  3. mutable all_queues : Eva__.Mqueue.Set.t;
    (*

    Set of all queues of the analysis

    *)
  4. mutable iteration : int;
    (*

    Current iteration of the analysis

    *)
  5. mutable main_thread : thread_state;
    (*

    Starting thread

    *)
  6. mutable curr_thread : thread_state;
    (*

    Thread currently running.

    *)
  7. mutable curr_events_stack : Mt_types.Trace.t list;
    (*

    Mthread events that have been found during the current analysis of the current thread. The list has the same height as curr_stack. The top of the list is the trace containing the events for the function being analyzed by Value, and so on until the top of the list. When the list is popped, the events of the callee are merged inside the trace of the caller.

    *)
  8. mutable memexec_cache : Mt_types.Trace.t Frama_c_kernel.Datatype.Int.Hashtbl.t;
    (*

    Cache for the results obtained during the analysis of the current thread

    *)
  9. mutable curr_stack : Eva.Callstack.t;
    (*

    stack of a multithread event. Asynchronously set by a callback and used by another, because of a slightly too restricted signature in the value analysis.

    *)
  10. mutable concurrent_accesses : Frama_c_kernel.Locations.Zone.t;
    (*

    Shared variables that have been detected in the analysis so far, with the crude analysis. Updated at the end of an iteration, and used to reach the fixpoint

    *)
  11. mutable precise_concurrent_accesses : Frama_c_kernel.Locations.Zone.t;
    (*

    Really shared variables that have been detected in the analysis so far, Subset of the previous field

    *)
  12. mutable concurrent_accesses_by_nodes : (Frama_c_kernel.Locations.Zone.t * Mt_cfg_types.SetNodeIdAccess.t) list;
    (*

    List of concurrent accesses that have been found. Used to compute the field precise_concurrent_accesses

    *)
}
val threads : analysis_state -> thread_state list
val thread_state : analysis_state -> thread -> thread_state
val fold_threads : analysis_state -> 'a -> (thread_state -> 'a -> 'a) -> 'a
val iter_threads : analysis_state -> (thread_state -> unit) -> unit
val curr_events : analysis_state -> Mt_types.Trace.t
val register_event : analysis_state -> ?top:Mt_cil.stack_elt -> Mt_types.event -> unit
val register_memory_states : analysis_state -> before:Mt_memory.Types.functions_states -> after:Mt_memory.Types.functions_states -> unit
val register_multiple_events : analysis_state -> Mt_types.Trace.t -> unit
val push_function_call : analysis_state -> unit
val pop_function_call : analysis_state -> unit
val should_compute_thread : thread_state -> bool
module OrderedThreads : sig ... end