package frama-c
- Overview
- No Docs
You can search for identifiers within the package.
in-package search v0.2.0
Platform dedicated to the static analysis of source code written in C
Install
Dune Dependency
Authors
-
PPatrick Baudin
-
FFrançois Bobot
-
RRichard Bonichon
-
DDavid Bühler
-
LLoïc Correnson
-
PPascal Cuoq
-
ZZaynah Dargaye
-
JJean-Christophe Filliâtre
-
PPhilippe Herrmann
-
FFlorent Kirchner
-
MMatthieu Lemerre
-
CClaude Marché
-
AAndré Maroneze
-
BBenjamin Monate
-
YYannick Moy
-
AAnne Pacalet
-
VValentin Perrelle
-
GGuillaume Petiot
-
VVirgile Prevosto
-
AArmand Puccetti
-
MMuriel Roger
-
JJulien Signoles
-
BBoris Yakobowski
Maintainers
Description
Frama-C is a suite of tools dedicated to the analysis of the source code of software written in C. Magnesium version.
Frama-C gathers several static analysis techniques in a single collaborative framework. The collaborative approach of Frama-C allows static analyzers to build upon the results already computed by other analyzers in the framework. Thanks to this approach, Frama-C provides sophisticated tools, such as a slicer and dependency analysis.
This virtual package forces the installation of frama-C with its IDE.
Tags
deductive program verification formal specification automated theorem prover interactive theorem prover C plugins abstract interpretation slicing weakest precondition ACSL dataflow analysisPublished: 30 Oct 2018
Dependencies (6)
- conf-gnomecanvas
- conf-gtksourceview
-
lablgtk
>= "2.18.2"
- zarith
-
frama-c-base
= "12.1"
-
ocaml
>= "3.12" & != "4.02.0"
Dev Dependencies
None
Conflicts
None
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>
On This Page