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
T

Thibaut Benjamin
A

Allan Blanchard
L

Lionel Blatter
F

François Bobot
R

Richard Bonichon
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
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
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
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-27.1-Cobalt.tar.gz

sha256=5b13574a16a58971c27909bee94ae7f37b17d897852b40c768a3d4e2e09e39d2

doc/frama-c.kernel/Frama_c_kernel/Float_interval/index.html

Module `Frama_c_kernel.Float_interval`

module Make
  (Float : Float_sig.S) : 
  Float_interval_sig.S
    with type float := Float.t
     and type widen_hints := Float.widen_hints

Builds a semantics of floating-point intervals for different precisions, from a module providing the floating-point numbers used for the bounds of the intervals. Supports NaN and infinite values.