---
css: home
layout: default
title: Frama-C
---
<body class="home page-template-default page page-id-7 nonTouch">
<div id="wrapper" class="hfeed">
{% include headers.html %}
<div id="container" class="mainContainer">
<div class="pageContent titleIn secure" id="content" role="main">
<section class="section fullScreen verticalFlex">
<div class="sectionContent">
<h2 class="banner-title">A platform to make your C and C++ code safer and more secure</h2>
<p class="banner-desc">
Frama-C is an open-source extensible and collaborative platform dedicated to
source-code analysis of C and C++ software. The Frama-C analyzers assist you
in various source-code-related activities, from the navigation through
unfamiliar projects up to the certification of critical software.
</p>
<a class="btn cta-download" href="/html/get-frama-c.html"><span>Download <b>Frama-C</b><span><i class=
"icon icon-curly-left"></i><i class="icon icon-download-arrow"></i><i class=
"icon icon-curly-right"></i></span></span></a>
</div>
</section>
<section class="section fullScreen codeDemoScreen textCenter">
<div class="sectionContent">
<h3>Overview of a Frama-C analysis for<br>
a simple C program</h3>
<div class="slideHeader">
<h4>Browsing the analysis results with Frama-C</h4>
<div id="home_code_swiper" class="tabSlider swiper-container">
<div class="sliderWrapper swiper-wrapper">
<div class="swiper-slide">
<div role="button" class="slideTxt" target="tab_0">
<span>Interface Overview</span>
</div>
</div>
<div class="swiper-slide">
<div role="button" class="slideTxt" target="tab_1">
<span>Value Analysis</span>
</div>
</div>
<div class="swiper-slide">
<div role="button" class="slideTxt" target="tab_2">
<span>Effects Analysis</span>
</div>
</div>
<div class="swiper-slide">
<div role="button" class="slideTxt" target="tab_3">
<span>Dependency Analysis</span>
</div>
</div>
<div class="swiper-slide">
<div role="button" class="slideTxt" target="tab_4">
<span>Impact Analysis</span>
</div>
</div>
</div>
<div class="swiper-button-prev" style="color: #f7931c"></div>
<div class="swiper-button-next" style="color: #f7931c"></div>
</div>
</div>
<div class="codeDemoBlock">
<div id="home_code_detail_swiper" class="swiper-container">
<div class="swiper-wrapper">
<div class="swiper-slide">
<div class="sidetext">
<div>
<p>When invoked with the above command-line, Frama-C
creates an analysis project for the file first.c.
</p>
<p>The <tt>-val</tt> option on the command-line causes the value
analysis plug-in to run and have its results ready
before the interface appears.
</p>
<p>The <tt>-slevel</tt> option is one of several options that
influence the precision of the value analysis. The
actions of creating new analysis projects and
activating plug-ins can also be done interactively.
</p>
</div>
</div>
<img class="sideimg" src="/assets/img/home/gui-overview.png">
</div>
<div class="swiper-slide">
<div class="sidetext">
<div>
<p>The value analysis plug-in computes sets of possible
values for every variable at each point of the program.
When providing such results, Frama-C guarantees that the
variable does not take at that point any value other
than those listed.
</p>
<p>When the execution reaches this point inside the loop,
the variable <tt>S</tt> always contains either 0, 1, 3, or 6.
</p>
</div>
</div>
<img class="sideimg" src="/assets/img/home/value-analysis.png">
</div>
<div class="swiper-slide">
<div class="sidetext">
<div>
<p>For each statement, Frama-C can provide an exhaustive
list of the memory cells that may be modified by this
statement during the execution, even if the statement
uses pointers.
</p>
<p>Frama-C guarantees that anytime it is executed, the
statement <tt>*tmp = S;</tt> does not change any memory location
other than the cells of the array <tt>T</tt>.
</p>
</div>
</div>
<img class="sideimg" src="/assets/img/home/effect-analysis.png">
</div>
<div class="swiper-slide">
<div class="sidetext">
<div>
<p>The dependencies plug-in makes use of the results of
the value analysis plug-in to highlight the statements
that define the value of variable <tt>S</tt> at the selected
program point.
</p>
<p>The value contained in variable <tt>S</tt> at the statement
<tt>*tmp = S;</tt> was defined by the statement
<tt>S += i;</tt>.
</p>
</div>
</div>
<img class="sideimg" src="/assets/img/home/dep-analysis.png">
</div>
<div class="swiper-slide">
<div class="sidetext">
<div>
<p>This analysis highlights in green all the statements
impacted by the selected statement.
</p>
<p>The statement <tt>p = T;</tt> has repercussions on the statements
<tt>tmp = p; p++; *tmp = S;</tt>.
</p>
<p>It is guaranteed not to affect the statements <tt>S += i;</tt>
and <tt>i ++;</tt>.
</p>
</div>
</div>
<img class="sideimg" src="/assets/img/home/impact-analysis.png">
</div>
</div>
</div>
</div>
</div>
</section>
<section id="latest_events" class="section fullScreen calendarScreen" data-title="TIMELINE">
<div class="sectionContent">
<h3>Frama-C Timeline</h3>
<div class="eventScaleBlock">
<div class="scaleBg">
<u></u>
</div>
<div id="event_calender_swiper" class="swiper-container">
<div class="swiper-wrapper">
{% for event in site.events %}
<div class="swiper-slide"
{% if forloop.last %}
data-eventdate="latest"
{% endif %}
>
<a role="button" class="eventLink"><time>{{ event.date | date: "<b>%Y</b>" }}</time><span>{{ event.event }}</span></a>
</div>
{% endfor %}
</div>
</div>
</div>
<div id="events_iv_point" class="inviewCenter"></div>
<div id="event_detail_swiper" class="eventDetailsBlock swiper-container">
<div class="swiper-wrapper">
{% for event in site.events %}
<div class="swiper-slide">
<div class="eventDetail" id="post_details_486">
<div class="contentBlk">
<time>{{ event.date | date: "<b>%-d</b><b>%B</b><small>%Y</small>" }}</time>
<div>
<h3>{{ event.title }}</h3>
<p>{{ event.content }}</p>
</div>
</div>
</div>
</div>
{% endfor %}
</div>
</div>
</div>
</section>
<section class="section downloadSection fullScreen verticalFlex" data-title="DOWNLOAD">
<div class="sectionContent">
<div class="head">
<h3>Get Frama-C</h3>
<nav>
<span class="currentVersion">Latest Version</span><a role="button" href="/html/get-frama-c.html">{{ site.fc-versions.last.name }}</a><a href="/html/framac-versions.html" class="previousVersion">Previous Versions</a>
</nav>
</div>
<div class="linkBlk">
<p>Frama-C is only available for Desktop</p><a class="btn mobileLink" href="/html/get-frama-c.html"><span>Discover
more about <b>Frama-C</b></span></a> <a class="btn cta-download" href="/html/get-frama-c.html"><span>Download
<b>Frama-C</b><span><i class="icon icon-curly-left"></i><i class="icon icon-download-arrow"></i><i class=
"icon icon-curly-right"></i></span></span></a>
</div>
</div>
<div id="download_iv_point" class="inviewCenter"></div>
</section>
{% include footer.html %}
<div class="clear"></div>
</div>
</div>
<body>
<script type='text/javascript' src='/assets/js/swiper.js'></script>
<head><script type='text/javascript' src='/assets/js/main.js'></script></head>