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
No active development, limited support

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
Archived: no maintenance or support, incompatible with recent Frama-C versions

SecureFlow

Information flow analysis

Proprietary, contact us for more information
No active development, limited support

Jessie

A deductive verification plug-in.

Archived: no maintenance or support, incompatible with recent Frama-C versions

ACSL Importer

Import ACSL specifications from extern files

Included in main Frama-C distribution

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

Volatile

Instrument volatile accesses for verification

Included in main Frama-C distribution

CaFE

Verification of CaRet temporal logic properties

Distributed separately under open-source licence
Archived: no maintenance or support, incompatible with recent Frama-C versions

MetAcsl

Verification of high-level ACSL requirements

Distributed separately under open-source licence

Pilat

Loop numeric invariant generator

Distributed separately under open-source licence
Archived: no maintenance or support, incompatible with recent Frama-C versions

RPP

Verification of relational properties

Distributed separately under open-source licence
Early prototype, contact us for more information

Counter-Examples

Counter-example generation from failed proof attempts

Archived: no maintenance or support, incompatible with recent Frama-C versions

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
No active development, limited support

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
No active development, limited support

Spare code

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

Included in main Frama-C distribution
No active development, limited support

Variadic

Variadic simplifies variadic functions for other plug-ins.

Included in main Frama-C distribution

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
No active development, limited support

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

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

Proprietary, contact us for more information
Archived: no maintenance or support, incompatible with recent Frama-C versions

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.

Included in main Frama-C distribution

Conc2seq

Verification of concurrent programs

Distributed separately under open-source licence
Archived: no maintenance or support, incompatible with recent Frama-C versions

DeadlockF

Deadlock detection in multithreaded C programs with mutexes.

Distributed separately under open-source licence
Third-party plug-in