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 Edit opam file Versions (36)

Authors

Maintainers

F

francois.bobot@cea.fr

Sources

frama-c-24.0-Chromium.tar.gz

sha256=4eeaf1321780a8d88f492fb50a83859a229585e33fa7a5e10dbf49506e7c3d74

Description

Frama-C gathers several analysis techniques in a single collaborative framework, based on analyzers (called "plug-ins") that can build upon the results computed by other analyzers in the framework. Thanks to this approach, Frama-C provides sophisticated tools, including:

an analyzer based on abstract interpretation (Eva plug-in);
a program proof framework based on weakest precondition calculus (WP plug-in);
a program slicer (Slicing plug-in);
a tool for verification of temporal (LTL) properties (Aoraï plug-in);
a runtime verification tool (E-ACSL plug-in);
several tools for code base exploration and dependency analysis (plug-ins From, Impact, Metrics, Occurrence, Scope, etc.). These plug-ins communicate between each other via the Frama-C API and via ACSL (ANSI/ISO C Specification Language) properties.

Published: 02 Dec 2021

Dependencies (17)

zarith >= "1.5"
why3 >= "1.4.0" & < "1.5~"
ocamlgraph >= "1.8.8"
ocamlfind
ocaml >= "4.08.1"
conf-graphviz post
alt-ergo
alt-ergo-free
conf-gtksourceview3
lablgtk3-sourceview3
lablgtk3 >= "3.1.0" & os != "macos"
ocamlgraph_gtk
ocamlgraph < "2.0"
conf-gtksourceview
conf-gnomecanvas
lablgtk >= "2.18.8"
conf-autoconf build

Dev Dependencies (3)

yojson >= "1.6.0" & < "2.1.0" & (< "2.0.0" | !with-test)
ocamlgraph with-test & < "2.1.0"
conf-time with-test

Used by (6)

deadlock
frama-c-lannotate < "0.2"
frama-c-luncov < "0.2"
frama-c-metacsl = "0.2"
pilat < "1.2" | >= "1.6"
why < "2.32"

Conflicts

None

On This Page

Description
Dependencies (17)
Dev Dependencies (3)
Used by (6)
Conflicts