---
layout: default
css: plugin
title: Kernel & Plugins - Frama-C
---
<body class="page-template page-template-page-kernel_plugins page-template-page-kernel_plugins-php page page-id-16 nonTouch">
<div id="wrapper" class="hfeed">
{% include headers.html header=2 %}
<div id="container" class="mainContainer">
<div class="tabs">
<div class="wrap">
<a class="active tabLink" href="kernel-plugin.html">Plugins</a> <em></em> <a class="tabLink" href=
"/html/kernel.html">Kernel</a> <em></em> <a class="tabLink" href="/html/gui.html">GUI</a>
<div class="tabOptions">
<div class="pluginSearch">
<form class="searchForm" method="get" action="kernel-plugin.html" data-parsley-validate="">
<button type="submit" class="submit searchLink" title="Search"><i class="icon icon-search"></i></button>
<input type="text" name="plugin" placeholder="Search for the plugins here" data-parsley-required="">
<div class="error" id="top_search_error" style="display: none;" role="alert"></div>
</form><a class="btn" target="_blank" href=
"https://framac.s3.amazonaws.com/production/uploads/2017/08/frama-c-plugin-development-guide.pdf.pdf"><span>Write
Your Own Plugin</span></a>
</div>
</div>
</div>
</div>
<div class="pluginSliderWrapper">
<div class="pluginSwiper swiper-container">
<div class="swiper-wrapper">
<div class="swiper-slide" id="post_details" style="background-image: url(kernel-plugin.html);background-size:cover;">
<div>
<h3>WP<i class="icon-arrow-thin-rgt"></i></h3>
<p>Deductive proofs of ACSL contracts</p>
<p><a class="readMore" href="../documentation/wp/index.html">Read More</a></p>
</div>
</div>
<div class="swiper-slide" id="post_details" style="background-image: url(kernel-plugin.html);background-size:cover;">
<div>
<h3>E-ACSL<i class="icon-arrow-thin-rgt"></i></h3>
<p>Runtime Verification Tool</p>
<p><a class="readMore" href="../documentation/e-acsl/index.html">Read More</a></p>
</div>
</div>
<div class="swiper-slide" id="post_details" style=
"background-image: url(https://framac.s3.amazonaws.com/production/uploads/2017/08/eva2-2.jpg);background-size:cover;">
<div>
<h3>Evolved Value Analysis (EVA)<i class="icon-arrow-thin-rgt"></i></h3>
<p>Automatically computes variation domains for the variables of the program.</p>
<p><a class="readMore" href="../documentation/eva/index.html">Read More</a></p>
</div>
</div>
</div>
<div class="swiper-pagination"></div>
</div>
<div class="nextPrev">
<div class="swiper-button-prev"></div>
<div class="swiper-button-next"></div>
</div>
</div>
<div class="pagePlugin pages">
<div class="bgTextbig">
Plugin
</div>
<div class="wrap">
<div class="docListwrap">
<section>
<div class="docListTitle">
<span>Main analyzers</span>
</div><a role="link" href="../documentation/jessie/index.html" class="listItem">
<div>
<h4 class="listItemTitle" data-bgtext="Jessie"><span>Jessie</span></h4>
<p>A deductive verification plug-in.</p>
</div></a> <a role="link" href="../documentation/wp/index.html" class="listItem">
<div>
<h4 class="listItemTitle" data-bgtext="WP"><span>WP</span></h4>
<p>Deductive proofs of ACSL contracts</p>
</div></a> <a role="link" href="../documentation/e-acsl/index.html" class="listItem">
<div>
<h4 class="listItemTitle" data-bgtext="E-ACSL"><span>E-ACSL</span></h4>
<p>Runtime Verification Tool</p>
</div></a> <a role="link" href="../documentation/eva/index.html" 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>
</div></a>
</section>
<section>
<div class="docListTitle">
<span>For test-case generation</span>
</div><a role="link" href="../documentation/pathcrawler/index.html" 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>
</div></a>
</section>
<section>
<div class="docListTitle">
<span>For concurrent programs</span>
</div><a role="link" href="../documentation/mthread/index.html" 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>
</div></a>
</section>
<section>
<div class="docListTitle">
<span>For code transformation</span>
</div><a role="link" href="../documentation/semantic-constant-folding/index.html" class="listItem">
<div>
<h4 class="listItemTitle" data-bgtext="Semantic constant folding"><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>
</div></a> <a role="link" href="../documentation/spare-code/index.html" class="listItem">
<div>
<h4 class="listItemTitle" data-bgtext="Spare code"><span>Spare code</span></h4>
<p>Removes "spare code", code that does not contribute to the final results of the program.</p>
</div></a> <a role="link" href="../documentation/variadic/index.html" class="listItem">
<div>
<h4 class="listItemTitle" data-bgtext="Variadic"><span>Variadic</span></h4>
<p>Variadic simplifies variadic functions for other plug-ins.</p>
</div></a>
</section>
<section>
<div class="docListTitle">
<span>For browsing unfamiliar code</span>
</div><a role="link" href="../documentation/studia/index.html" class="listItem">
<div>
<h4 class="listItemTitle" data-bgtext="Studia"><span>Studia</span></h4>
<p>Studia helps with EVA case studies on the GUI.</p>
</div></a> <a role="link" href="../documentation/metrics-calculation/index.html" 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>
</div></a> <a role="link" href="../documentation/sparecode/index.html" class="listItem">
<div>
<h4 class="listItemTitle" data-bgtext="Occurrence analysis plug-in"><span>Occurrence analysis plug-in</span></h4>
<p>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.</p>
</div></a> <a role="link" href="../documentation/impact/index.html" class="listItem">
<div>
<h4 class="listItemTitle" data-bgtext="Impact analysis"><span>Impact analysis</span></h4>
<p>Highlights the locations in the source code that are impacted by a modification.</p>
</div></a> <a role="link" href="../documentation/scope/index.html" class="listItem">
<div>
<h4 class="listItemTitle" data-bgtext="Scope & Data-flow browsing"><span>Scope & Data-flow
browsing</span></h4>
<p>Allows the user to navigate the dataflow of the program, from definition to use or from use to definition.</p>
</div></a>
</section>
</div>
</div>
</div>
{% include footer.html %}
<div class="clear"></div>
</div>
</div>
</body>