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-28.1-Nickel.tar.gz

sha256=0220bc743b7da2468ceb926f331edc7ddfaa7c603ba47962de3e33c8e1e3f593

doc/frama-c.kernel/Frama_c_kernel/Dataflows/Simple_backward/argument-2-P/index.html

Parameter `Simple_backward.P`

include JOIN_SEMILATTICE

type t

val join : t -> t -> t

Must be idempotent (join a a = a), commutative, and associative.

val bottom : t

Must verify that forall a, join a bottom = a.

val is_included : t -> t -> bool

Must verify: a is_included b <=> a join b = b. The dataflow does not require this function.

val join_and_is_included : t -> t -> t * bool

This function is used by the dataflow algorithm to determine if something has to be recomputed. Joining and inclusion testing are similar operations, so it is often more efficient to do both at the same time (e.g. when joining with bottom).

Instead of defining it directly, it can be defined from join and equal, or from is_included, for instance by if is_included new old then (true,old) else (false, join old new) or let j = join old new in (equal j new, j).

val pretty : Format.formatter -> t -> unit

Display the contents of an element of the lattice.

val transfer_stmt : Cil_types.stmt -> t -> t

transfer_stmt s state must implement the transfer function for s.

val init : (Cil_types.stmt * t) list

The initial state after each statement. Statements in this list are given the associated value, and are added to the worklist. Other statements are initialized to bottom.

To get results for an entire function, this list should contain information for the following statements:

the final statement of the function (Kernel_function.find_return)
all the statements with no successors
at least one statement per non-terminating loop