---
css: documentation
layout: default
title: Documentation - Frama-C
---
<body class="page-template page-template-page-documentation page-template-page-documentation-php page page-id-20 nonTouch">
<div id="wrapper" class="hfeed">
{% include headers.html header=4 %}
<div id="container" class="mainContainer">
<div class="pageDocumentation pages">
<div class="bgTextbig">
Documentation
</div>
<div class="wrap">
<h1 class="pageTitle">Documentation</h1>
<div class="pageBanner" style=
"background-image:url('https://framac.s3.amazonaws.com/production/uploads/2017/07/banner.jpg');background-size:cover;">
<p>All the documentation<br>
you need !</p>
</div>
<div class="docListwrap">
<section>
<div class="docListTitle">
<span>PLUG-INS</span>
</div>
<div class="listItem">
<div>
<h4 class="listItemTitle" data-bgtext="Link Test"><span>Link Test</span></h4>
<p>This is a test to see if HTTP link is accepted instead of PDF</p><span class="docReadMore">Read
More</span><a class="linkReadmore" href="link-test/index.html"></a> <a class="btnPdfDownload" target="_blank"
href="http://www.dummies.com/"><i class="icon-download-arrow"></i></a>
</div>
</div>
<div class="listItem">
<div>
<h4 class="listItemTitle" data-bgtext="Studia"><span>Studia</span></h4>
<p>Studia helps with EVA case studies on the GUI.</p><a class="btnPdfDownload" target="_blank" href=
"https://framac.s3.amazonaws.com/production/uploads/2017/10/user-manual-Phosphorus-20170501.pdf"><i class=
"icon-download-arrow"></i></a>
</div>
</div>
<div class="listItem">
<div>
<h4 class="listItemTitle" data-bgtext="WP"><span>WP</span></h4>
<p>Deductive proofs of ACSL contracts</p><span class="docReadMore">Read More</span><a class="linkReadmore" href=
"wp/index.html"></a> <a class="btnPdfDownload" target="_blank" href=
"https://framac.s3.amazonaws.com/production/uploads/2017/10/wp-manual-Phosphorus-20170501.pdf"><i class=
"icon-download-arrow"></i></a>
</div>
</div>
<div class="listItem">
<div>
<h4 class="listItemTitle" data-bgtext="E-ACSL"><span>E-ACSL</span></h4>
<p>Runtime Verification Tool</p><span class="docReadMore">Read More</span><a class="linkReadmore" href=
"e-acsl/index.html"></a> <a class="btnPdfDownload" target="_blank" href=
"https://framac.s3.amazonaws.com/production/uploads/2017/10/e-acsl-manual.pdf"><i class=
"icon-download-arrow"></i></a>
</div>
</div>
<div class="listItem">
<div>
<h4 class="listItemTitle" data-bgtext="PathCrawler"><span>PathCrawler</span></h4>
<p>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...</p><span class="docReadMore">Read
More</span><a class="linkReadmore" href="pathcrawler/index.html"></a> <a class="btnPdfDownload" target="_blank"
href="http://www.google.fr"><i class="icon-download-arrow"></i></a>
</div>
</div>
<div class="listItem">
<div>
<h4 class="listItemTitle" data-bgtext="Mthread"><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><span class=
"docReadMore">Read More</span><a class="linkReadmore" href="mthread/index.html"></a> <a class="btnPdfDownload"
target="_blank" href=
"https://framac.s3.amazonaws.com/production/uploads/2017/10/frama-c-mthread-manual.pdf"><i class=
"icon-download-arrow"></i></a>
</div>
</div>
<div class="listItem">
<div>
<h4 class="listItemTitle" data-bgtext="Metrics calculation"><span>Metrics calculation</span></h4>
<p>Allows the user to compute various metrics from the source code.</p><span class="docReadMore">Read
More</span><a class="linkReadmore" href="metrics-calculation/index.html"></a> <a class="btnPdfDownload" target=
"_blank" href="https://framac.s3.amazonaws.com/production/uploads/2017/10/frama-c-metrics-manual.pdf"><i class=
"icon-download-arrow"></i></a>
</div>
</div>
<div class="listItem">
<div>
<h4 class="listItemTitle" data-bgtext="Variadic"><span>Variadic</span></h4>
<p>Variadic simplifies variadic functions for other plug-ins.</p><span class="docReadMore">Read
More</span><a class="linkReadmore" href="variadic/index.html"></a>
</div>
</div>
<div class="listItem">
<div>
<h4 class="listItemTitle" data-bgtext="Evolved Value Analysis (EVA)"><span>Evolved Value Analysis
(EVA)</span></h4>
<p>Automatically computes variation domains for the variables of the program.</p><span class="docReadMore">Read
More</span><a class="linkReadmore" href="/html/documentation/eva.html"></a> <a class="btnPdfDownload" target="_blank" href=
"https://framac.s3.amazonaws.com/production/uploads/2017/08/Form10C.pdf"><i class="icon-download-arrow"></i></a>
</div>
</div>
</section>
<section>
<div class="docListTitle">
<span>ACSL (ANSI/ISO-C Specification Language)</span>
</div>
<div class="listItem">
<div>
<h4 class="listItemTitle" data-bgtext="ACSL Reference Manual"><span>ACSL Reference Manual</span></h4>
<p>Lorem Ipsum is simply dummy text of the printing and typesetting industry. Lorem Ipsum has been the industrys
standard dummy text ever since the 1500s, when an unknown printer took...</p><a class="btnPdfDownload" target=
"_blank" href="https://framac.s3.amazonaws.com/production/uploads/2017/08/download.pdf"><i class=
"icon-download-arrow"></i></a>
</div>
</div>
</section>
</div>
</div>
</div>
{% include footer.html %}
<div class="clear"></div>
</div>
</div>
</body>