Frama-C:
Plug-ins:
Libraries:

Frama-C API - Interferences

type state = Dom.t
type add_result =
  1. | Updated
  2. | NoChanges
val reset : unit -> unit

reset () resets the current interferences state. Must be called between two analyses.

val add_last_analysis : Eva__.Thread.t -> Eva__.Position.Local.Set.t -> Frama_c_kernel.Base.Hptset.t -> add_result

Add the last Eva analysis results to the given interferences abstract representation.

val inject_init_state : Eva__.Thread.t -> Frama_c_kernel.Cil_types.kernel_function -> state -> state

inject_init_state th kf state injects current interferences to the initial state of the analysis for thread th starting at the entry point kf. If enabled, the Mthread domain helps filtering applicable interferences. This function is the identity if the Mthread domain can infer that no other thread can interfere with the current thread.

val inject_after_change : Eva__.Inout_access.t -> state -> state

inject_after_change access state injects current interferences to the given state that has just been changed by a transfer function with the given accesses. If enabled, the Mthread domain helps filtering applicable interferences. This function is the identity if the Mthread domain can infer that no shared memory has been read or written during the last transfer function.