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
S

Sylvain Chiron
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
B

Benjamin Jorge
F

Florent Kirchner
A

Alexander Kogtenkov
R

Remi Lazarini
T

Tristan Le Gall
K

Kilyan Le Gallic
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
C

Cécile Ruet-Cros
J

Julien Signoles
N

Nicolas Stouls
K

Kostyantyn Vorobyov
B

Boris Yakobowski

Maintainers

F

frama-ci-bot@frama-c.com

Sources

frama-c-31.0-Gallium.tar.gz

sha256=a94384f00d53791cbb4b4d83ab41607bc71962d42461f02d71116c4ff6dca567

doc/frama-c-e-acsl.core/E_ACSL/Inductive/Derived_functions/index.html

Module `Inductive.Derived_functions`

extract_predicate may generate auxiliary logic functions. Such a logic function f is stored in an hash table of this module table with the predicate p (from which f has been derived) as a key and f as a value. There may be multiple logic functions associated with a predicate.

val iter : 
  (Frama_c_kernel.Cil_types.logic_info ->
    Frama_c_kernel.Cil_types.logic_info ->
    unit) ->
  unit