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
Jessie
A deductive verification plug-in.
Old plug-in, not necessarily compatible with recent Frama-C versions
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
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
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
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
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
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
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