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.kernel/Frama_c_kernel/Dataflow2/index.html

Module `Frama_c_kernel.Dataflow2`

Implementation of data flow analyses over user-supplied domains.

see https://frama-c.com/download/frama-c-plugin-development-guide.pdf

type 't action =

| Default
(*
The default action
*)
| Done of 't
(*
Do not do the default action. Use this result
*)
| Post of 't -> 't
(*
The default action, followed by the given transformer
*)

possible kinds of action for backward analysis

type 't stmtaction =

| SDefault
(*
The default action
*)
| SDone
(*
Do not visit this statement or its successors
*)
| 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 =

| GDefault
(*
The default state
*)
| GUse of 't
(*
Use this data for the branch
*)
| 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