---
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 siteIntro fullScreen verticalFlex" id="intro_screen" data-title="SECURE">
<div class="sectionContent">
<h2 class="banner-title">Securing the future of your critical activities</h2>
<p class="banner-desc">The Frama-C source code analysis platform provides tools to make your C/C++ code safer and more
secure.</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>
<div id="siteIntro_iv_point" class="inviewCenter"></div><a class="goDown" data-target="code_demo_screen" role=
"button"><span>Get Started</span><i class="icon icon-arrow-thin-dwn"></i></a>
</section>
<section class="section codeDemoScreen textCenter" id="code_demo_screen" data-title="ERROR!">
<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"></div>
<div class="swiper-button-next"></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="codeTips">
<div class="title">
<b>01</b><span>This command-line creates an analysis project for file <samp>first.c</samp>.</span>
</div>
<div class="title">
<b>02</b><span>Option <samp>-eva</samp> runs the Eva plug-in and prepares its
results.</span>
</div>
<div class="title">
<b>03</b><span>Option <tt>-slevel 10</tt> is one of several options that influence the precision of the
value analysis.</span>
</div>
</div>
<div class="notebook code">
<div>
<div class="codeScreen">
<div class="codeTab tab-demo">
<div style="background: #202020; overflow:auto;width:auto;border:solid transparent;">
<pre style="margin: 0; line-height: 125%; background: #202020;">
<span style="color: #6ab825; font-weight: bold">int</span> <span style="color: #d0d0d0">S=</span><span style=
"color: #3677a9">0</span><span style="color: #d0d0d0">;</span>
<span style="color: #6ab825; font-weight: bold">int</span> <span style="color: #d0d0d0">T[</span><span style=
"color: #3677a9">5</span><span style="color: #d0d0d0">];</span>
<span style="color: #6ab825; font-weight: bold">int</span> <span style="color: #447fcf">main</span><span style=
"color: #d0d0d0">(</span><span style="color: #6ab825; font-weight: bold">void</span><span style="color: #d0d0d0">)<span class="arrowTooltip right"><span><span class="title"><b>03</b><span>Option <tt>-slevel 10</tt> is one of several options that influence the precision of the
value analysis.</span></span></span></span></span>
<span style="color: #d0d0d0">{</span>
<span class="highlight">int i;</span>
<span style="color: #6ab825; font-weight: bold">int</span> <span style="color: #d0d0d0">*p</span> <span style=
"color: #d0d0d0">=</span> <span style="color: #d0d0d0">&T[</span><span style="color: #3677a9">0</span><span style=
"color: #d0d0d0">]</span> <span style="color: #d0d0d0">;</span>
<span style="color: #6ab825; font-weight: bold">for</span> <span style="color: #d0d0d0">(i=</span><span style=
"color: #3677a9">0</span><span style="color: #d0d0d0">;</span> <span style="color: #d0d0d0">i<</span><span style=
"color: #3677a9">5</span><span style="color: #d0d0d0">;</span> <span style="color: #d0d0d0">i++)</span>
<span style="color: #d0d0d0">{</span> <span style="color: #d0d0d0">S</span> <span style="color: #d0d0d0">=</span> <span style=
"color: #d0d0d0">S+i;</span> <span style="color: #d0d0d0">*p++</span> <span style="color: #d0d0d0">=</span> <span style=
"color: #d0d0d0">S;</span> <span style="color: #d0d0d0">}</span>
<span style="color: #6ab825; font-weight: bold">return</span> <span style="color: #d0d0d0">S;</span>
<span style="color: #d0d0d0">}</span>
<span style="color: #d0d0d0"><span class="arrowTooltip left"><span><span class=
"title"><b>01</b><span>This command-line creates an analysis project for file <samp>first.c</samp>.</span></span></span></span><u></u>frama-c-gui</span> <span style="color: #d0d0d0">-eva</span><span class="tooltip">2</span> <span style="color: #d0d0d0">-slevel</span> <span style="color: #3677a9">10<span class="tooltip">3</span></span> <span style="color: #d0d0d0">first.c</span><span class="tooltip">1</span><span class="arrowTooltip right"><span><span class="title"><b>02</b><span>Option <samp>-eva</samp> runs the Eva plug-in and prepares its results.</span></span></span></span><u></u>
</pre>
</div>
</div>
</div>
</div>
</div>
</div>
<div class="swiper-slide">
<div class="codeTips">
<div class="title">
<b>01</b><span>The Evolved Value Analysis (EVA) plug-in computes sets of possible values for every variable
at each point of the program.</span>
</div>
<div class="title">
<b>02</b><span>When the execution reaches the highlighted point inside the loop, the variable
<samp>S</samp> always contains either 0, 1, 3, or 6. Frama-C guarantees that it does not take any other
values at that point.</span>
</div>
</div>
<div class="notebook code">
<div>
<div class="codeScreen">
<div class="codeTab tab-demo">
<div style="background: #202020; overflow:auto;width:auto;border:solid transparent;">
<pre style="margin: 0; line-height: 125%; background: #202020;">
<span style="color: #d0d0d0">i</span> <span style="color: #d0d0d0">=</span> <span style="color: #3677a9">0</span><span style=
"color: #d0d0d0">;</span>
<span style="color: #6ab825; font-weight: bold">while</span> <span style="color: #d0d0d0">(i</span> <span style=
"color: #d0d0d0"><</span> <span style="color: #3677a9">5</span><span style="color: #d0d0d0">)</span> <span style=
"color: #d0d0d0">{</span>
<span style="color: #d0d0d0">{</span>
<span style="color: #6ab825; font-weight: bold">int</span> <span style="color: #d0d0d0">*tmp;</span>
<span class="arrowTooltip left"><span><span class=
"title"><b>01</b><span>The Evolved Value Analysis (EVA) plug-in computes sets of possible values for every variable at each point of the program.</span></span></span></span><u></u><span style="color: #d0d0d0"><span class="highlight">S<span class="tooltip">1</span></span></span> <span style="color: #d0d0d0">+=</span> <span style="color: #d0d0d0">i;</span>
<span style="color: #d0d0d0">{</span> <span style="color: #999999; font-style: italic">/* sequence */</span>
<span style="color: #d0d0d0">tmp</span> <span style="color: #d0d0d0">=</span> <span style="color: #d0d0d0">p;</span>
<span style="color: #d0d0d0">p</span> <span style="color: #d0d0d0">++;</span>
<span style="color: #d0d0d0">*tmp</span> <span style="color: #d0d0d0">=</span> <span style="color: #d0d0d0">S;</span>
<span style="color: #d0d0d0">}</span>
<span style="color: #d0d0d0">}</span>
<span style="color: #d0d0d0">i++;</span>
<span style="color: #d0d0d0">}</span>
<span style="color: #6ab825; font-weight: bold">return</span> <span style="color: #d0d0d0">S;</span>
<span style="color: #d0d0d0">}</span>
<span style="color: #d0d0d0">S</span> <span style="color: #a61717; background-color: #e3d2d2">∈</span> <span style=
"color: #d0d0d0">{</span><span style="color: #3677a9">0</span><span style="color: #d0d0d0">;</span> <span style=
"color: #3677a9">1</span><span style="color: #d0d0d0">;</span> <span style="color: #3677a9">3</span><span style=
"color: #d0d0d0">;</span> <span style="color: #3677a9">6</span><span style="color: #d0d0d0">}</span><span class=
"tooltip">2</span><span class="arrowTooltip right"><span><span class=
"title"><b>02</b><span>When the execution reaches the highlighted point inside the loop, the variable <samp>S</samp> always contains either 0, 1, 3, or 6. Frama-C guarantees that it does not take any other values at that point.</span></span></span></span><u></u>
<span style="color: #d0d0d0">S</span> <span style="color: #d0d0d0">(after)</span> <span style=
"color: #a61717; background-color: #e3d2d2">∈</span> <span style="color: #d0d0d0">{</span><span style=
"color: #3677a9">0</span><span style="color: #d0d0d0">;</span> <span style="color: #3677a9">1</span><span style=
"color: #d0d0d0">;</span> <span style="color: #3677a9">3</span><span style="color: #d0d0d0">;</span> <span style=
"color: #3677a9">6</span><span style="color: #d0d0d0">;</span> <span style="color: #3677a9">10</span><span style=
"color: #d0d0d0">}</span>
</pre>
</div>
</div>
</div>
</div>
</div>
</div>
<div class="swiper-slide">
<div class="codeTips">
<div class="title">
<b>01</b><span>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.</span>
</div>
<div class="title">
<b>02</b><span>Frama-C guarantees that anytime it is executed, the statement <samp>*tmp = S;</samp> does
not change any memory location other than the cells of the array <samp>T</samp>.</span>
</div>
</div>
<div class="notebook code">
<div>
<div class="codeScreen">
<div class="codeTab tab-demo">
<div style="background: #202020; overflow:auto;width:auto;border:solid transparent;">
<pre style="margin: 0; line-height: 125%; background: #202020;">
<span style="color: #d0d0d0">p</span> <span style="color: #d0d0d0">=</span> <span style="color: #d0d0d0">T;</span>
<span style="color: #d0d0d0">i</span> <span style="color: #d0d0d0">=</span> <span style="color: #3677a9">0</span><span style=
"color: #d0d0d0">;</span>
<span style="color: #6ab825; font-weight: bold">while</span> <span style="color: #d0d0d0">(i</span> <span style=
"color: #d0d0d0"><</span> <span style="color: #3677a9">5</span><span style="color: #d0d0d0">)</span> <span style=
"color: #d0d0d0">{</span>
<span style="color: #d0d0d0">{</span>
<span style="color: #6ab825; font-weight: bold">int</span> <span style="color: #d0d0d0">*tmp;</span>
<span style="color: #d0d0d0">S</span> <span style="color: #d0d0d0">+=</span> <span style="color: #d0d0d0">i;</span>
<span style="color: #d0d0d0">{</span> <span style="color: #999999; font-style: italic">/* sequence */</span>
<span style="color: #d0d0d0">tmp</span> <span style="color: #d0d0d0">=</span> <span style="color: #d0d0d0">p;</span>
<span style="color: #d0d0d0">p</span> <span style="color: #d0d0d0">++;</span>
<span class="arrowTooltip left"><span><span class=
"title"><b>01</b><span>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.</span></span></span></span><u></u><span class="highlight">*tmp = S;<span class="tooltip">1</span></span>
<span style="color: #d0d0d0">}</span>
<span style="color: #d0d0d0">}</span>
<span style="color: #d0d0d0">i++;</span>
<span style="color: #d0d0d0">}</span>
<span style="color: #6ab825; font-weight: bold">return</span> <span style="color: #d0d0d0">S;</span>
<span style="color: #d0d0d0">}</span>
<span class="highlight">*tmp = S;</span> <span style="color: #d0d0d0">modifies</span> <span style=
"color: #d0d0d0">T[</span><span style="color: #3677a9">0..4</span><span style="color: #d0d0d0">]</span><span class=
"arrowTooltip right"><span><span class=
"title"><b>02</b><span>Frama-C guarantees that anytime it is executed, the statement <samp>*tmp = S;</samp> does not change any memory location other than the cells of the array <samp>T</samp>.</span></span></span></span><u></u><span class="tooltip">2</span>
</pre>
</div>
</div>
</div>
</div>
</div>
</div>
<div class="swiper-slide">
<div class="codeTips">
<div class="title">
<b>01</b><span>The dependencies plug-in highlights the statements that define the value of variable
<samp>S</samp> at this point.</span>
</div>
<div class="title">
<b>02</b><span>The value contained in variable <samp>S</samp> at the statement <samp>*tmp = S;</samp> was
defined by the statement <samp>S += i;</samp></span>
</div>
</div>
<div class="notebook code">
<div>
<div class="codeScreen">
<div class="codeTab tab-demo">
<div style="background: #202020; overflow:auto;width:auto;border:solid transparent;">
<pre style="margin: 0; line-height: 125%; background: #202020;">
<span style="color: #6ab825; font-weight: bold">int</span> <span style="color: #447fcf">main</span><span style=
"color: #d0d0d0">(</span><span style="color: #6ab825; font-weight: bold">void</span><span style="color: #d0d0d0">)</span>
<span style="color: #d0d0d0">{</span>
<span style="color: #6ab825; font-weight: bold">int</span> <span style="color: #d0d0d0">i;</span>
<span style="color: #6ab825; font-weight: bold">int</span> <span style="color: #d0d0d0">*p;</span>
<span style="color: #d0d0d0">p</span> <span style="color: #d0d0d0">=</span> <span style="color: #d0d0d0">T;</span>
<span style="color: #d0d0d0">i</span> <span style="color: #d0d0d0">=</span> <span style="color: #3677a9">0</span><span style=
"color: #d0d0d0">;</span>
<span style="color: #6ab825; font-weight: bold">while</span> <span style="color: #d0d0d0">(i</span> <span style=
"color: #d0d0d0"><</span> <span style="color: #3677a9">5</span><span style="color: #d0d0d0">)</span> <span style=
"color: #d0d0d0">{</span>
<span style="color: #d0d0d0">{</span>
<span style="color: #6ab825; font-weight: bold">int</span> <span style="color: #d0d0d0">*tmp;</span>
<span class="highlight2">S += i;</span><span class="tooltip">2</span><span class="arrowTooltip right"><span><span class=
"title"><b>02</b><span>The value contained in variable <samp>S</samp> at the statement <samp>*tmp = S;</samp> was defined by the statement <samp>S += i;</samp></span></span></span></span><u></u>
<span style="color: #d0d0d0">{</span> <span style="color: #999999; font-style: italic">/* sequence */</span>
<span style="color: #d0d0d0">tmp</span> <span style="color: #d0d0d0">=</span> <span style="color: #d0d0d0">p;</span>
<span style="color: #d0d0d0">p</span> <span style="color: #d0d0d0">++;</span>
<span class="arrowTooltip left"><span><span class=
"title"><b>01</b><span>The dependencies plug-in highlights the statements that define the value of variable <samp>S</samp> at this point.</span></span></span></span><u></u><span style="color: #d0d0d0">*tmp</span> <span style="color: #d0d0d0">=</span> <span class="highlight">S<span class="tooltip">1</span></span><span style="color: #d0d0d0">;</span>
<span style="color: #d0d0d0">}</span>
<span style="color: #d0d0d0">}</span>
<span style="color: #d0d0d0">i++;</span>
<span style="color: #d0d0d0">}</span>
<span style="color: #6ab825; font-weight: bold">return</span> <span style="color: #d0d0d0">S;</span>
<span style="color: #d0d0d0">}</span>
</pre>
</div>
</div>
</div>
</div>
</div>
</div>
<div class="swiper-slide">
<div class="codeTips">
<div class="title">
<b>01</b><span>This analysis highlights all the statements impacted by the selected statement.</span>
</div>
<div class="title">
<b>02</b><span>This statement has repercussions on the statements <samp>tmp = p; p++; *tmp = S;</samp>. It
is guaranteed not to affect the statements <samp>S += i;</samp> and <samp>i ++;</samp></span>
</div>
</div>
<div class="notebook code">
<div>
<div class="codeScreen">
<div class="codeTab tab-demo">
<div style="background: #202020; overflow:auto;width:auto;border:solid transparent;">
<pre style="margin: 0; line-height: 125%; background: #202020;">
<span style="color: #6ab825; font-weight: bold">int</span> <span style="color: #447fcf">main</span><span style=
"color: #d0d0d0">(</span><span style="color: #6ab825; font-weight: bold">void</span><span style="color: #d0d0d0">)</span>
<span style="color: #d0d0d0">{</span>
<span style="color: #6ab825; font-weight: bold">int</span> <span style="color: #d0d0d0">i;</span>
<span style="color: #6ab825; font-weight: bold">int</span> <span style="color: #d0d0d0">*p;</span>
<span class="arrowTooltip left"><span><span class=
"title"><b>01</b><span>This analysis highlights all the statements impacted by the selected statement.</span></span></span></span><u></u><span class="highlight">p = T;</span><span class="tooltip">1</span>
<span style="color: #d0d0d0">i</span> <span style="color: #d0d0d0">=</span> <span style="color: #3677a9">0</span><span style=
"color: #d0d0d0">;</span>
<span style="color: #6ab825; font-weight: bold">while</span> <span style="color: #d0d0d0">(i</span> <span style=
"color: #d0d0d0"><</span> <span style="color: #3677a9">5</span><span style="color: #d0d0d0">)</span> <span style=
"color: #d0d0d0">{</span>
<span style="color: #d0d0d0">{</span>
<span style="color: #6ab825; font-weight: bold">int</span> <span style="color: #d0d0d0">*tmp;</span>
<span style="color: #d0d0d0">S</span> <span style="color: #d0d0d0">+=</span> <span style="color: #d0d0d0">i;</span>
<span style="color: #d0d0d0">{</span> <span style="color: #999999; font-style: italic">/* sequence */</span>
<span class="highlight2">tmp = p;</span>
<span class="highlight2">p++;</span>
<span class="highlight2">*tmp = S;</span><span class="tooltip">2</span><span class="arrowTooltip right"><span><span class=
"title"><b>02</b><span>This statement has repercussions on the statements <samp>tmp = p; p++; *tmp = S;</samp>. It is guaranteed not to affect the statements <samp>S += i;</samp> and <samp>i ++;</samp></span></span></span></span><u></u>
<span style="color: #d0d0d0">}</span>
<span style="color: #d0d0d0">}</span>
<span style="color: #d0d0d0">i++;</span>
<span style="color: #d0d0d0">}</span>
<span style="color: #6ab825; font-weight: bold">return</span> <span style="color: #d0d0d0">S;</span>
<span style="color: #d0d0d0">}</span>
</pre>
</div>
</div>
</div>
</div>
</div>
</div>
</div>
</div>
</div>
</div>
<div id="code_demo_iv_point" class="inviewCenter"></div>
</section>
<section class="section aboutScreen fullScreen verticalFlex" id="about_screen" data-title="ABOUT">
<div class="sectionContent">
<div class="circleBlock">
<h2>What is<br>
Frama-C<br>
used for?</h2>
<div class="circle robustness"></div>
<div class="circle codeStandard"></div>
<div class="circle security"></div><a href="/html/using-frama-c.html" class="robustness" role=
"button"><span class="icon"><i class=" icon-thumb"></i></span> <span class="txt">Test your software's
<b>robustness</b></span></a><a href="/html/using-frama-c.html" class="codeStandard" role=
"button"><span class="icon"><i class=" icon-code"></i></span> <span class="txt">Enforce <b>code
requirements</b></span></a><a href="/html/using-frama-c.html" class="security" role=
"button"><span class="icon"><i class=" icon-lock"></i></span> <span class="txt">Detect <b>security
defects</b></span></a>
</div>
</div>
<div id="about_iv_point" class="inviewCenter"></div>
</section>
<section id="latest_events" class="section calendarScreen fullScreen" data-title="TIMELINE">
<div class="sectionContent">
<h2>Frama-C Timeline</h2>
<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" id="download_screen" 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 %}
<section class="bgTitleBlk titleIn white">
<div class="upperBlk">
<div class="upperType">
SECURE
</div>
</div>
<div class="lowerBlk">
<div class="lowerType">
SECURE
</div>
</div>
</section>
</div>
<script>
var homeLabels = {secure_label : 'Secure',error_label : 'Error',about_label : 'About',follow_label : 'Follow',footer_label : 'Get Frama-C',};
</script>
<div class="clear"></div>
</div>
</div>
<body>