Module X.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__.Analysis_location.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 : Frama_c_kernel.Cil_types.kernel_function -> Eva__.Eva_automata.vertex -> Eva__.Eva_automata.vertex -> state -> state

Inject current interferences to an abstract state. If activated, 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.

val is_empty : Eva__.Eva_automata.transition -> bool

Are there any interferences to inject after the given transition?