|
/html/kernel-plugin.html
|
Features
|
|
|
/html/documentation.html
|
Documentation
|
|
|
/html/publications.html
|
Publications
|
|
|
/blog/index.html
|
Blog
|
|
|
/html/jobs.html
|
Jobs
|
|
|
/html/contact.html
|
Contact
|
|
|
/html/get-frama-c.html
|
Download
|
|
|
/html/get-frama-c.html
|
<span><i class="icon icon-curly-left"></i><i class="icon icon-download-arrow"></i><i class="icon icon-curly-right"></i></span>
|
|
|
/html/kernel-plugin.html
|
Plugins
|
|
|
/html/kernel.html
|
Kernel
|
|
|
/html/acsl.html
|
Specification
|
|
|
/html/ivette.html
|
Ivette (GUI)
|
|
|
/download/frama-c-plugin-development-guide.pdf
|
<span>Write Your Own Plugin</span>
|
|
|
/fc-plugins/eva.html
|
<h4 class="tileTitle"><span>Eva</span></h4> <p>Automatically computes variation domains for the variables of the program.</p> <p> <i>Included in main Frama-C distribution</i> </p>
|
|
|
/fc-plugins/wp.html
|
<h4 class="tileTitle"><span>WP</span></h4> <p>Deductive proofs of ACSL contracts.</p> <p> <i>Included in main Frama-C distribution</i> </p>
|
|
|
/fc-plugins/e-acsl.html
|
<h4 class="tileTitle"><span>E-ACSL</span></h4> <p>Runtime Verification Tool.</p> <p> <i>Included in main Frama-C distribution</i> </p>
|
|
|
/fc-plugins/pathcrawler.html
|
<h4 class="tileTitle"><span>PathCrawler</span></h4> <p>White-box test cases generator.</p> <p> <i>Proprietary, contact us for more information</i> <br> <i>No active development, limited support</i> </p>
|
|
|
/fc-plugins/alias.html
|
<h4 class="tileTitle"><span>Alias</span></h4> <p>Efficient alias and points-to analysis</p> <p> <i>Included in main Frama-C distribution</i> </p>
|
|
|
/fc-plugins/stady.html
|
<h4 class="tileTitle"><span>StaDy</span></h4> <p>Generation of test inputs confirming alarms generated by static analysis</p> <p> <i>Distributed separately under open-source licence</i> <br> <i>Archived: no maintenance or support, incompatible with recent Frama-C versions</i> </p>
|
|
|
/fc-plugins/secureflow.html
|
<h4 class="tileTitle"><span>SecureFlow</span></h4> <p>Information flow analysis</p> <p> <i>Proprietary, contact us for more information</i> <br> <i>No active development, limited support</i> </p>
|
|
|
/fc-plugins/jessie.html
|
<h4 class="tileTitle"><span>Jessie</span></h4> <p>A deductive verification plug-in.</p> <p> <i>Archived: no maintenance or support, incompatible with recent Frama-C versions</i> </p>
|
|
|
/fc-plugins/acsl-importer.html
|
<h4 class="tileTitle"><span>ACSL Importer</span></h4> <p>Import ACSL specifications from extern files</p> <p> <i>Included in main Frama-C distribution</i> </p>
|
|
|
/fc-plugins/aorai.html
|
<h4 class="tileTitle"><span>Aoraï</span></h4> <p>Verify specifications expressed as LTL (Linear Temporal Logic) formulas.</p> <p> <i>Included in main Frama-C distribution</i> </p>
|
|
|
/fc-plugins/rte.html
|
<h4 class="tileTitle"><span>RTE</span></h4> <p>Generates annotations for possible runtime errors and other properties.</p> <p> <i>Included in main Frama-C distribution</i> </p>
|
|
|
/fc-plugins/volatile.html
|
<h4 class="tileTitle"><span>Volatile</span></h4> <p>Instrument volatile accesses for verification</p> <p> <i>Included in main Frama-C distribution</i> </p>
|
|
|
/fc-plugins/cafe.html
|
<h4 class="tileTitle"><span>CaFE</span></h4> <p>Verification of CaRet temporal logic properties</p> <p> <i>Distributed separately under open-source licence</i> <br> <i>Archived: no maintenance or support, incompatible with recent Frama-C versions</i> </p>
|
|
|
/fc-plugins/metacsl.html
|
<h4 class="tileTitle"><span>MetAcsl</span></h4> <p>Verification of high-level ACSL requirements</p> <p> <i>Distributed separately under open-source licence</i> </p>
|
|
|
/fc-plugins/pilat.html
|
<h4 class="tileTitle"><span>Pilat</span></h4> <p>Loop numeric invariant generator</p> <p> <i>Distributed separately under open-source licence</i> <br> <i>Archived: no maintenance or support, incompatible with recent Frama-C versions</i> </p>
|
|
|
/fc-plugins/rpp.html
|
<h4 class="tileTitle"><span>RPP</span></h4> <p>Verification of relational properties</p> <p> <i>Distributed separately under open-source licence</i> <br> <i>Early prototype, contact us for more information</i> </p>
|
|
|
/fc-plugins/counter-examples.html
|
<h4 class="tileTitle"><span>Counter-Examples</span></h4> <p>Counter-example generation from failed proof attempts</p> <p> <i>Archived: no maintenance or support, incompatible with recent Frama-C versions</i> </p>
|
|
|
/fc-plugins/markdown-report.html
|
<h4 class="tileTitle"><span>MdR</span></h4> <p>Markdown and SARIF reports on status of ACSL annotations</p> <p> <i>Included in main Frama-C distribution</i> </p>
|
|
|
/fc-plugins/metrics-calculation.html
|
<h4 class="tileTitle"><span>Metrics</span></h4> <p>Allows the user to compute various metrics from the source code.</p> <p> <i>Included in main Frama-C distribution</i> </p>
|
|
|
/fc-plugins/report.html
|
<h4 class="tileTitle"><span>Report</span></h4> <p>Report on status of ACSL annotations</p> <p> <i>Included in main Frama-C distribution</i> </p>
|
|
|
/fc-plugins/server.html
|
<h4 class="tileTitle"><span>Server</span></h4> <p>Frama-C Server Protocol</p> <p> <i>Included in main Frama-C distribution</i> </p>
|
|
|
/fc-plugins/ltest.html
|
<h4 class="tileTitle"><span>LTest</span></h4> <p>Set of utilities for test coverage</p> <p> <i>Distributed separately under open-source licence</i> <br> <i>No active development, limited support</i> </p>
|
|
|
/fc-plugins/instantiate.html
|
<h4 class="tileTitle"><span>Instantiate</span></h4> <p>Creates function specializations for other plugins.</p> <p> <i>Included in main Frama-C distribution</i> </p>
|
|
|
/fc-plugins/semantic-constant-folding.html
|
<h4 class="tileTitle"><span>Semantic constant folding</span></h4> <p>Makes use of the results of the EVA plug-in to replace, in the source code, the constant expressions by their values.</p> <p> <i>Included in main Frama-C distribution</i> </p>
|
|
|
/fc-plugins/slicing.html
|
<h4 class="tileTitle"><span>Slicing</span></h4> <p>Slices the code according to user-provided criteria.</p> <p> <i>Included in main Frama-C distribution</i> <br> <i>No active development, limited support</i> </p>
|
|
|
/fc-plugins/spare-code.html
|
<h4 class="tileTitle"><span>Spare code</span></h4> <p>Removes "spare code", code that does not contribute to the final results of the program.</p> <p> <i>Included in main Frama-C distribution</i> <br> <i>No active development, limited support</i> </p>
|
|
|
/fc-plugins/variadic.html
|
<h4 class="tileTitle"><span>Variadic</span></h4> <p>Variadic simplifies variadic functions for other plug-ins.</p> <p> <i>Included in main Frama-C distribution</i> </p>
|
|
|
/fc-plugins/dive.html
|
<h4 class="tileTitle"><span>Dive</span></h4> <p>Dive provides dataflow visualization (from Eva) in Ivette.</p> <p> <i>Included in main Frama-C distribution</i> </p>
|
|
|
/fc-plugins/impact.html
|
<h4 class="tileTitle"><span>Impact</span></h4> <p>Highlights the locations in the source code that are impacted by a modification.</p> <p> <i>Included in main Frama-C distribution</i> <br> <i>No active development, limited support</i> </p>
|
|
|
/fc-plugins/occurrence.html
|
<h4 class="tileTitle"><span>Occurrence</span></h4> <p>Allows the user to reach the statements where a given variable is used. Also provided as a simple example for new plug-in development.</p> <p> <i>Included in main Frama-C distribution</i> </p>
|
|
|
/fc-plugins/scope.html
|
<h4 class="tileTitle"><span>Scope</span></h4> <p>Allows the user to navigate the dataflow of the program, from definition to use or from use to definition.</p> <p> <i>Included in main Frama-C distribution</i> </p>
|
|
|
/fc-plugins/studia.html
|
<h4 class="tileTitle"><span>Studia</span></h4> <p>Studia helps with Eva case studies on the GUI.</p> <p> <i>Included in main Frama-C distribution</i> </p>
|
|
|
/fc-plugins/frama-clang.html
|
<h4 class="tileTitle"><span>Frama-Clang</span></h4> <p>C++ front-end to Frama-C, based on the clang compiler.</p> <p> <i>Distributed separately under open-source licence</i> </p>
|
|
|
/fc-plugins/frama-plc.html
|
<h4 class="tileTitle"><span>Frama-PLC</span></h4> <p>Analyses of Software Application for Programmable Logic Controllers</p> <p> <i>Proprietary, contact us for more information</i> </p>
|
|
|
/fc-plugins/jcard.html
|
<h4 class="tileTitle"><span>JCard</span></h4> <p>JavaCard Front-End for Frama-C</p> <p> <i>Proprietary, contact us for more information</i> <br> <i>Archived: no maintenance or support, incompatible with recent Frama-C versions</i> </p>
|
|
|
/fc-plugins/mthread.html
|
<h4 class="tileTitle"><span>Mthread</span></h4> <p>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.</p> <p> <i>Included in main Frama-C distribution</i> </p>
|
|
|
/fc-plugins/conc2seq.html
|
<h4 class="tileTitle"><span>Conc2seq</span></h4> <p>Verification of concurrent programs</p> <p> <i>Distributed separately under open-source licence</i> <br> <i>Archived: no maintenance or support, incompatible with recent Frama-C versions</i> </p>
|
|
|
/fc-plugins/deadlockf.html
|
<h4 class="tileTitle"><span>DeadlockF</span></h4> <p>Deadlock detection in multithreaded C programs with mutexes.</p> <p> <i>Distributed separately under open-source licence</i> <br> <i>Third-party plug-in</i> </p>
|
|
|
/html/terms-of-use.html
|
Terms Of Use
|
|
|
/html/authors.html
|
Authors
|
|
|
/html/acknowledgement.html
|
Acknowledgements
|
|
nginx