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-project

Dependency

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

Authors

Maintainers

F

frama-ci-bot@frama-c.com

Sources

frama-c-32.0-beta-Germanium.tar.gz

sha256=868d57ef8007fe6c0836cd151d8c294003af34aa678285eff9547662cad36aa3

doc/frama-c-eva.gui/Eva_gui/Gui_eval/Make/argument-1-X/Interferences/index.html

Module `X.Interferences`

type state = Dom.t

type add_result =

| Updated
| 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.