Plugins Kernel Specification GUI Ivette
Write Your Own Plugin
Main analyzers

Eva

Automatically computes variation domains for the variables of the program.

Included in main Frama-C distribution

WP

Deductive proofs of ACSL contracts.

Included in main Frama-C distribution

E-ACSL

Runtime Verification Tool.

Included in main Frama-C distribution

PathCrawler

White-box test cases generator.

Proprietary, contact us for more information
Specialized analyses

Alias

Efficient alias and points-to analysis

Included in main Frama-C distribution

StaDy

Generation of test inputs confirming alarms generated by static analysis

Distributed separately under open-source licence

SecureFlow

Information flow analysis

Proprietary, contact us for more information

Jessie

A deductive verification plug-in.

Old plug-in, not necessarily compatible with recent Frama-C versions
Specification of code properties

Aoraï

Verify specifications expressed as LTL (Linear Temporal Logic) formulas.

Included in main Frama-C distribution

RTE

Generates annotations for possible runtime errors and other properties.

Included in main Frama-C distribution

CaFE

Verification of CaRet temporal logic properties

Distributed separately under open-source licence

MetAcsl

Verification of high-level ACSL requirements

Distributed separately under open-source licence

Pilat

Loop numeric invariant generator

Distributed separately under open-source licence

ACSL Importer

Import ACSL specifications from extern files

Proprietary, contact us for more information

Counter-Examples

Counter-example generation from failed proof attempts

Proprietary, contact us for more information

RPP

Verification of relational properties

Early prototype, contact us for more information
Reporting

MdR

Markdown and SARIF reports on status of ACSL annotations

Included in main Frama-C distribution

Metrics

Allows the user to compute various metrics from the source code.

Included in main Frama-C distribution

Report

Report on status of ACSL annotations

Included in main Frama-C distribution

Server

Frama-C Server Protocol

Included in main Frama-C distribution

LTest

Set of utilities for test coverage

Distributed separately under open-source licence
Code transformation

Instantiate

Creates function specializations for other plugins.

Included in main Frama-C distribution

Semantic constant folding

Makes use of the results of the EVA plug-in to replace, in the source code, the constant expressions by their values.

Included in main Frama-C distribution

Slicing

Slices the code according to user-provided criteria.

Included in main Frama-C distribution

Spare code

Removes "spare code", code that does not contribute to the final results of the program.

Included in main Frama-C distribution

Variadic

Variadic simplifies variadic functions for other plug-ins.

Included in main Frama-C distribution
Browsing unfamiliar code

Dive

Dive provides dataflow visualization (from Eva) in Ivette.

Included in main Frama-C distribution

Impact

Highlights the locations in the source code that are impacted by a modification.

Included in main Frama-C distribution

Occurrence

Allows the user to reach the statements where a given variable is used. Also provided as a simple example for new plug-in development.

Included in main Frama-C distribution

Scope

Allows the user to navigate the dataflow of the program, from definition to use or from use to definition.

Included in main Frama-C distribution

Studia

Studia helps with Eva case studies on the GUI.

Included in main Frama-C distribution
Front-ends for other languages

Frama-Clang

C++ front-end to Frama-C, based on the clang compiler.

Distributed separately under open-source licence

Frama-PLC

Analyses of Software Application for Programmable Logic Controllers

Proprietary, contact us for more information

JCard

JavaCard Front-End for Frama-C

Old plug-in, not necessarily compatible with recent Frama-C versions
Concurrent/multi-threaded programs

Conc2seq

Verification of concurrent programs

Distributed separately under open-source licence

DeadlockF

Deadlock detection in multithreaded C programs with mutexes.

Distributed separately under open-source licence

Mthread

Analyzes concurrent C programs, taking into account all possible thread interactions. Provides precise information about shared variables, which mutex protects a part of the code, etc.

Proprietary, contact us for more information