package frama-c

  1. Overview
  2. Docs
package frama-c
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Mthread.Mt_threadSource

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

    No priority specified, but it is possible to specify one

    *)
  2. | PUnknown
    (*

    Contradictory priorities specified

    *)
  3. | PPriority of int
    (*

    Known priority

    *)
Sourcetype thread
Sourcetype 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

Sourcemodule ThreadState : sig ... end
Sourcetype 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

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

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct