package frama-c

You can search for identifiers within the package.

in-package search v0.2.0

On This Page

Backward dataflow
Forward dataflow
1. Helper functions for forward dataflow.

Platform dedicated to the analysis of source code written in C

Install

dune-project

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/Dataflows/index.html

Module `Frama_c_kernel.Dataflows`

Implementation of data flow analyses over user-supplied domains.

module type FUNCTION_ENV = sig ... end

Environment relative to the function being processed, and function to create them from Kf.

val function_env : Cil_types.kernel_function -> (module FUNCTION_ENV)

module type JOIN_SEMILATTICE = sig ... end

Backward dataflow

module type BACKWARD_MONOTONE_PARAMETER = sig ... end

Statement-based backward dataflow. Contrary to the forward dataflow, the transfer function cannot differentiate the state before a statement between different predecessors.

module Simple_backward
  (_ : FUNCTION_ENV)
  (P : BACKWARD_MONOTONE_PARAMETER) : 
  sig ... end

Forward dataflow

module type FORWARD_MONOTONE_PARAMETER = sig ... end

Edge-based forward dataflow. It is edge-based because the transfer function can differentiate the state after a statement between different successors. In particular, the state can be reduced according to the conditions in if statements.

module Simple_forward
  (_ : FUNCTION_ENV)
  (P : FORWARD_MONOTONE_PARAMETER) : 
  sig ... end

Helper functions for forward dataflow.

val transfer_if_from_guard : 
  (Cil_types.stmt -> Cil_types.exp -> 'a -> 'a * 'a) ->
  Cil_types.stmt ->
  'a ->
  (Cil_types.stmt * 'a) list

transfer_if_from_guard implements FORWARD_MONOTONE_PARAMETER.transfer_stmt for the If statement, given a function transfer_guard.

transfer_guard receives a conditional expression, the current statement, and the current state, and must return two states in which the conditional is assumed to be true and false respectively. Returning twice the current state is a valid, albeit imprecise, result.

val transfer_switch_from_guard : 
  (Cil_types.stmt -> Cil_types.exp -> 'a -> 'a * 'a) ->
  Cil_types.stmt ->
  'a ->
  (Cil_types.stmt * 'a) list

Same as transfer_if_from_guard, but for a Switch statement. The same function transfer_guard can be used for transfer_if_from_guard and transfer_switch_from_guard.