package frama-c

You can search for identifiers within the package.

in-package search v0.2.0

Platform dedicated to the analysis of source code written in C

Install

Dune Dependency

frama-c.com Readme Edit opam file Versions (25)

Authors

Maintainers

F

frama-ci-bot@frama-c.com

Sources

frama-c-31.0-Gallium.tar.gz

sha256=a94384f00d53791cbb4b4d83ab41607bc71962d42461f02d71116c4ff6dca567

doc/mthread/Mthread/Mt_thread/index.html

Module `Mthread.Mt_thread`Source

Sourcetype recompute_reason =

| FirstIteration
| NewMsgReceived
| PotentialSharedVarsChanged
| SharedVarsValuesChanged
| InitialArgsChanged
| InitialEnvChanged
| InterferencesChanged

Sourcemodule RecomputeReason : sig ... end

module SetRecomputeReason : Stdlib.Set.S with type elt = recompute_reason

Sourcetype priority =

| PDefault
(*
No priority specified, but it is possible to specify one
*)
| PUnknown
(*
Contradictory priorities specified
*)
| PPriority of int
(*
Known priority
*)

Sourcemodule Priority : Frama_c_kernel.Datatype.S with type t = priority

Sourcetype thread

Sourcetype thread_state = {

th_eva_thread : Eva__.Thread.t;
th_parent : thread_state option;
(*
Thread in which the thread is created. None for the root thread
*)
th_fun : Frama_c_kernel.Cil_types.kernel_function;
(*
Function which the thread executes
*)
th_stack : Eva.Callstack.t;
(*
Call stack resulting in the creation of the thread
*)
mutable th_init_state : Frama_c_kernel.Cvalue.Model.t;
(*
Memory state at the moment the thread is created
*)
mutable th_params : Frama_c_kernel.Cvalue.V.t list;
(*
Arguments to the the thread function
*)
mutable th_amap : Mt_types.Trace.t;
(*
map interesting statements to sets concurrent actions with their call stacks
*)
mutable th_to_recompute : SetRecomputeReason.t;
(*
Does this thread needs to be recomputed on the next iteration
*)
mutable th_read_written : Mt_shared_vars_types.AccessesByZone.map;
(*
Globals read and written by the thread, and at which statement
*)
mutable th_cfg : Mt_cfg_types.CfgNode.t;
(*
Cfg for the current thread
*)
mutable th_read_written_cfg : Mt_cfg_types.AccessesByZoneNode.map;
(*
Globals read and written by the thread, and at which node in the cfg
*)
mutable th_values_written : Mt_memory.Types.state;
(*
Join of all the values written by this thread in shared locations. Currently not contextual
*)
mutable th_projects : Frama_c_kernel.Project.t list;
(*
Copies of the analyses of the thread, most recent first
*)
mutable th_value_results : Eva__.Eva_results.results option;
(*
Result of the last Value analysis of this thread
*)
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 = {

all_threads : thread_state Eva__.Thread.Hashtbl.t;
(*
List of all threads. Is kept (and can thus increase) from one iteration to the next
*)
mutable all_mutexes : Eva__.Mutex.Set.t;
(*
Set of all mutexes of the analysis
*)
mutable all_queues : Eva__.Mqueue.Set.t;
(*
Set of all queues of the analysis
*)
mutable iteration : int;
(*
Current iteration of the analysis
*)
mutable main_thread : thread_state;
(*
Starting thread
*)
mutable curr_thread : thread_state;
(*
Thread currently running.
*)
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.
*)
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
*)
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.
*)
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
*)
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
*)
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 calling_ki : analysis_state -> Frama_c_kernel.Cil_types.kinstr

Sourceval current_fun : analysis_state -> Frama_c_kernel.Cil_types.kernel_function

Sourceval curr_events : analysis_state -> Mt_types.Trace.t

Source

val register_event : 
  analysis_state ->
  ?top:Mt_cil.stack_elt ->
  Mt_types.event ->
  unit

Source

val 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