PV1 ⊧ Frama-Cframework providing abstractions for C code analysis

Platform/framework for the analysis of C code

Application domain/field

• Software verification
• Runtime verification
• Deductive verification
• Abstract interpretation

Type of tool

Framework

Expected input

• C program
• Specifications (as ACSL annotations)

Format:

.c file with ACSL annotations.

Expected output

Depends on the plugin that is used.

Internals

It has many different types of plugins that do different kind of analyses such as WP (deductive verification), E-ACSL (runtime verification), PathCrawler (test case generator) and EVA (value analysis based on abstract interpretation). It uses the specification language ACSL. Some plugins support a subset of ACSL.

Comments

It can be run from the command-line or via its graphical user interface. Some plugins are meant to be used via the command-line, not via the GUI.