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/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__.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?