package frama-c

  1. Overview
  2. Docs
package frama-c
Legend:
Library
Module
Module type
Parameter
Class
Class type
type t

States propagated by the dataflow analysis.

val join : t -> t -> t

Merges two states coming from different paths.

val widen : t -> t -> t widening

widen v1 v2 is called on loop heads after each iteration of the analysis on the loop body: v1 is the previous state before the iteration, and v2 the new state after the iteration. The function must return Fixpoint if the analysis has reached a fixpoint for the loop: this is usually the case if join v1 v2 is equal to v1, as a new iteration would have the same entry state as the last one. Otherwise, it must return the new entry state for the next iteration, by over-approximating the join between v1 and v2 such that any sequence of successive widenings is ultimately stationary, i.e. …widen (widen (widen x0 x1) x2) x3… eventually returns Fixpoint. This ensures the analysis termination.

val transfer : vertex -> vertex edge -> t -> t option

Transfer function for edges: transfer v e s computes the state after the transition e.edge_transition from the state s before, at vertex v. Returns None if the end of the transition is not reachable from the given state.

OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct