package frama-c

  1. Overview
  2. No Docs

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.

Dependencies (16)

  1. why3 >= "1.3.1" & < "1.4~"
  2. yojson
  3. conf-graphviz post
  4. alt-ergo
  5. alt-ergo-free
  6. conf-gtksourceview3
  7. lablgtk3-sourceview3
  8. lablgtk3 >= "3.0.beta4" & os != "macos"
  9. conf-gtksourceview
  10. conf-gnomecanvas
  11. lablgtk >= "2.18.2"
  12. conf-autoconf build
  13. zarith
  14. ocamlfind
  15. ocamlgraph >= "1.8.8" & < "1.9~"
  16. ocaml >= "4.05.0" & (< "4.08.0~" | >= "4.08.1")

Dev Dependencies

None

Used by (2)

  1. pilat < "1.2"
  2. why < "2.32"
OCaml

Innovation. Community. Security.