Newer
Older
title: Frama-C - Framework for Modular Analysis of C programs
description: "Frama-C - An open-source extensible and collaborative platform
dedicated to source-code analysis of C software."
<link rel="stylesheet" href="/assets/css/swiper.css">
<body class="home page-template-default page page-id-7 nonTouch">
<div id="wrapper" class="hfeed">
<div class="pageContent titleIn secure" id="content" role="main">
<section class="section verticalFlex fullScreen">
<h2 class="banner-title">A platform to make your 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 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.
<h3><a href="html/overview.html">Read More</a></h3>
<br/>
</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 class="goDown">
<div class="downlink">
<a href="#frama-c-overview" role="button">
Overview<br>
<i class="icon icon-arrow-thin-dwn"></i>
</a>
</div>
<div class="downlink">
<a href="#latest_events" role="button">
Latest News<br>
<i class="icon icon-arrow-thin-dwn"></i>
</a>
</div>
<section class="section normal codeDemoScreen textCenter" style="margin-top: 0">
<h3 tabindex="0" id="frama-c-overview" class="anchor">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 tabindex="0" role="button" class="slideTxt" target="0">
<div tabindex="0" role="button" class="slideTxt" target="1">
<div tabindex="0" role="button" class="slideTxt" target="2">
<div tabindex="0" role="button" class="slideTxt" target="3">
<div tabindex="0" role="button" class="slideTxt" target="4">
<div class="swiper-button-prev" style="color: #f7931c"></div>
<div class="swiper-button-next" style="color: #f7931c"></div>
</div>
<div class="codeDemoBlock">
<div id="home_code_detail_swiper" class="swiper-container">
<div class="swiper-wrapper">
<div class="swiper-slide">
<p>When invoked with the command-line: </p>
<pre>frama-c -eva -eva-precision 1 first.c</pre>
creates an analysis project for the file first.c.
</p>
<p>The <tt>-eva</tt> option on the command-line causes
the Eva plug-in to run and have its results ready
before the interface appears.
<p>The <tt>-eva-precision</tt> option is one of several
options that influence the precision of the Eva
plug-in. 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">
<p>The Eva 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">
<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">
<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">
<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">
<section id="latest_events" class="section normal calendarScreen" data-title="TIMELINE">
<h3 tabindex="0">Frama-C Timeline</h3>
{% assign all_events = site.events | concat: site.jobs | sort: 'date' %}
<div class="eventScaleBlock">
<div class="scaleBg">
<u></u>
</div>
<div id="event_calender_swiper" class="swiper-container">
<div class="swiper-wrapper">
<a role="button" class="eventLink"><time>{{ event.date | date: "<b>%Y</b>" }}</time>
</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">
<div class="eventDetail">
<time>{{ event.date | date: "<b>%B </b><b>%-d</b><small> %Y</small>" }}</time>
{% if event.layout == "job" %}
<p>{% if event.filled == true %}<b>[FILLED] </b>{% endif %}
{{ event.short }} [<a href="{{ event.url }}">More details</a>]
</p>
{% else %}
<p>{{ event.content }}</p>
{% endif %}
{% if event.keywords %}
<p>Keywords: <i>{{ event.keywords }}</i></p>
{% endif %}
<section class="section downloadSection normal verticalFlex" data-title="DOWNLOAD">
<h3 tabindex="0">Get Frama-C</h3>
{% assign versions = site.fc-versions | reverse %}
{% if versions[0].beta %}
{% assign beta = versions[0] %}
{% assign latest = versions[1] %}
{% else %}
{% assign latest = versions[0] %}
<span class="currentVersion">Latest Version</span><a role="button" href="/html/get-frama-c.html">{{ latest.name }}</a>
{% if beta %}<br><span class="currentVersion">Next Version</span><a role="button" href="{{ beta.url }}">{{ beta.name }}-β</a>{% endif %}
<br><a href="/html/framac-versions.html" class="previousVersion">All Versions</a>
<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 id="download_iv_point" class="inviewCenter"></div>
</section>
David Bühler
committed
<body>
<script type='text/javascript' src='/assets/js/swiper.js'></script>
<head><script type='text/javascript' src='/assets/js/main.js'></script></head>