package frama-c

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

Implementation of data flow analyses over user-supplied domains.

type 't action =
  1. | Default
    (*

    The default action

    *)
  2. | Done of 't
    (*

    Do not do the default action. Use this result

    *)
  3. | Post of 't -> 't
    (*

    The default action, followed by the given * transformer

    *)

possible kinds of action for backward analysis

type 't stmtaction =
  1. | SDefault
    (*

    The default action

    *)
  2. | SDone
    (*

    Do not visit this statement or its successors

    *)
  3. | SUse of 't
    (*

    Visit the instructions and successors of this statement as usual, but use the specified state instead of the one that was passed to doStmt

    *)
type 't guardaction =
  1. | GDefault
    (*

    The default state

    *)
  2. | GUse of 't
    (*

    Use this data for the branch

    *)
  3. | GUnreachable
    (*

    The branch will never be taken.

    *)

For if statements

module type StmtStartData = sig ... end
module StartData (X : sig ... end) : StmtStartData with type data = X.t

This module can be used to instantiate the StmtStartData components of the functors below. It is implemented through stmt-indexed hashtables.

Forwards Dataflow Analysis

module type ForwardsTransfer = sig ... end

Interface to provide for a backward dataflow analysis.

module Forwards (_ : ForwardsTransfer) : sig ... end

Backwards Dataflow Analysis

module type BackwardsTransfer = sig ... end

Interface to provide for a backward dataflow analysis.

module Backwards (_ : BackwardsTransfer) : sig ... end
val find_stmts : Cil_types.fundec -> Cil_types.stmt list * Cil_types.stmt list
  • returns

    (all_stmts, sink_stmts), where all_stmts is a list of the statements in a function, and sink_stmts is a list of the return statements (including statements that fall through the end of a void function). Useful when you need an initial set of statements for BackwardsDataFlow.compute.

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