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.
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.
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.
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.
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.
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.
Scope & Data-flow browsing
Allows the user to navigate the dataflow of the program, from definition to use or from use to definition.
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.
Studia
Studia helps with EVA case studies on the GUI.