E-ACSL

Runtime Verification Tool

Read More

Evolved Value Analysis (EVA)

Automatically computes variation domains for the variables of the program.

Read More

WP

Deductive proofs of ACSL contracts.

Read More

Plugin
Main analyzers

E-ACSL

Runtime Verification Tool

Evolved Value Analysis (EVA)

Automatically computes variation domains for the variables of the program.

Jessie

A deductive verification plug-in.

WP

Deductive proofs of ACSL contracts.

For test-case generation

PathCrawler

PathCrawler automatically finds test-case inputs to ensure coverage of a C function. It can be used for structural unit testing, as a complement to static analysis or to study the feasible execution paths of the function.

For concurrent programs

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.

For verifying functional specifications

Aoraï

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

For code transformation

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.

Slicing

This plug-in slices the code according to a user-provided criterion.

Spare code

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

Variadic

Variadic simplifies variadic functions for other plug-ins.

For browsing unfamiliar code

Impact analysis

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

Metrics calculation

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

Occurrence analysis plug-in

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

Scope & Data-flow browsing

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

Studia

Studia helps with EVA case studies on the GUI.

Front-end for other languages

Frama-Clang

This plug-in provides a C++ front-end to Frama-C, based on the clang compiler.