package frama-c

Overview
Docs

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

M

Michele Alberti
T

Thibaud Antignac
G

Gergö Barany
P

Patrick Baudin
N

Nicolas Bellec
T

Thibaut Benjamin
A

Allan Blanchard
L

Lionel Blatter
F

François Bobot
R

Richard Bonichon
V

Vincent Botbol
Q

Quentin Bouillaguet
D

David Bühler
Z

Zakaria Chihani
L

Loïc Correnson
J

Julien Crétin
P

Pascal Cuoq
Z

Zaynah Dargaye
B

Basile Desloges
J

Jean-Christophe Filliâtre
P

Philippe Herrmann
M

Maxime Jacquemin
F

Florent Kirchner
A

Alexander Kogtenkov
R

Remi Lazarini
T

Tristan Le Gall
J

Jean-Christophe Léchenet
M

Matthieu Lemerre
D

Dara Ly
D

David Maison
C

Claude Marché
A

André Maroneze
T

Thibault Martin
F

Fonenantsoa Maurica
M

Melody Méaulle
B

Benjamin Monate
Y

Yannick Moy
P

Pierre Nigron
A

Anne Pacalet
V

Valentin Perrelle
G

Guillaume Petiot
D

Dario Pinto
V

Virgile Prevosto
A

Armand Puccetti
F

Félix Ridoux
V

Virgile Robles
J

Jan Rochel
M

Muriel Roger
J

Julien Signoles
N

Nicolas Stouls
K

Kostyantyn Vorobyov
B

Boris Yakobowski

Maintainers

F

frama-ci-bot@frama-c.com

Sources

frama-c-29.0-Copper.tar.gz

sha256=d2fbb3b8d0ff83945872e9e6fa258e934a706360e698dae3b4d5f971addf7493

doc/frama-c.kernel/Frama_c_kernel/Dataflow2/Forwards/argument-1-_/StmtStartData/index.html

Module `_.StmtStartData`

For each statement id, the data at the start. Not found in the hash table means nothing is known about the state at this point. At the end of the analysis this means that the block is not reachable.

type data = t

val clear : unit -> unit

val mem : Cil_types.stmt -> bool

val find : Cil_types.stmt -> data

val replace : Cil_types.stmt -> data -> unit

val add : Cil_types.stmt -> data -> unit

val iter : (Cil_types.stmt -> data -> unit) -> unit

val length : unit -> int