Skip to content
Snippets Groups Projects
index.html 42.3 KiB
Newer Older
Augustin Lemesle's avatar
Augustin Lemesle committed
<!DOCTYPE html>
Augustin Lemesle's avatar
Augustin Lemesle committed

Augustin Lemesle's avatar
Augustin Lemesle committed
<html lang="en-US" class="framac-site">
Augustin Lemesle's avatar
Augustin Lemesle committed
<head>
  <meta name="generator" content="HTML Tidy for HTML5 (experimental) for Windows https://github.com/w3c/tidy-html5/tree/c63cc39">
  <meta charset="UTF-8">
  <meta name="viewport" content="width=device-width,initial-scale=1,maximum-scale=1,user-sclable=no">

  <title>Frama-C</title>
  <link rel='dns-prefetch' href='http://s.w.org/'>
  <style type="text/css" id="wp-custom-css">
a.plain{color:#d6be98 !important;border:0 !important;border-radius:0 !important;border-bottom:1px solid !important;padding:0 !important;background-color:transparent !important;box-shadow:none !important;display:inline !important;margin-left:auto !important;margin-bottom:5px !important;-webkit-transition:all .35s !important;transition:all .35s !important}a.plain:hover{color:#f36521 !important}.defnitionList dd .contentTxt p a{color:#d6be98;border-bottom:1px solid;display:table;margin-left:auto;margin-bottom:5px;-webkit-transition:all .35s;transition:all .35s}.defnitionList dd .contentTxt p a:hover{color:#f36521}
  </style>
  <link rel="shortcut icon" href="app/themes/frama/assets/img/favicon.ico" type="image/x-icon">
</head>

<body class="home page-template-default page page-id-7 nonTouch">
  <div id="wrapper" class="hfeed">
    <header class="siteHeader" id="site_header">
      <div id="header_iv_point" class="inviewTop"></div><span class="brandLogo"><a href="index.html" rel="home" title=
      "Frama-C"><img src="app/themes/frama/assets/img/framac.gif" alt=""><span>Frama-C</span></a></span><a role="button" id=
      "menu_toggle" class="menuToggle"><span class="open"><i></i><i></i><i></i></span><span class="close"><i></i><i></i></span></a>

      <nav id="menu" role="navigation">
        <div class="menu-primary-meny-container">
          <ul id="menu-primary-meny" class="menu">
            <li id="menu-item-25" class="menu-item menu-item-type-post_type menu-item-object-page menu-item-25">
              <a href="using-frama-c/index.html">Using Frama C</a>
            </li>

            <li id="menu-item-26" class="menu-item menu-item-type-post_type menu-item-object-page menu-item-26">
              <a href="kernel-plugin/index.html">Kernel &amp; Plugins</a>
            </li>

            <li id="menu-item-27" class="menu-item menu-item-type-post_type menu-item-object-page menu-item-27">
              <a href="http://localhost:8000/contact/">Contact</a>
            </li>

            <li id="menu-item-28" class="menu-item menu-item-type-post_type menu-item-object-page menu-item-28">
              <a href="documentation/index.html">Documentation</a>
            </li>

            <li id="menu-item-29" class="menu-item menu-item-type-post_type menu-item-object-page menu-item-29">
              <a href="blog/index.html">Blog</a>
            </li>
          </ul>
        </div><a role="button" href="get-frama-c/index.html" id="header_download_link" class="btnDownload"><span><i class=
        "icon icon-curly-left"></i><i class="icon icon-download-arrow"></i><i class="icon icon-curly-right"></i></span></a>
      </nav>
    </header>

    <div id="container" class="mainContainer">
      <div class="pageContent" 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 code safer and more
            secure.</p><a class="btn cta-download" href="get-frama-c/index.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>
Augustin Lemesle's avatar
Augustin Lemesle committed
          </div>
Augustin Lemesle's avatar
Augustin Lemesle committed

          <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>Trying out Frama-C analyzing<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>
Augustin Lemesle's avatar
Augustin Lemesle committed
                    </div>
Augustin Lemesle's avatar
Augustin Lemesle committed
                  </div>

                  <div class="swiper-slide">
                    <div role="button" class="slideTxt" target="tab_1">
                      <span>Value Analysis</span>
Augustin Lemesle's avatar
Augustin Lemesle committed
                    </div>
Augustin Lemesle's avatar
Augustin Lemesle committed
                  </div>

                  <div class="swiper-slide">
                    <div role="button" class="slideTxt" target="tab_2">
                      <span>Effects Analysis</span>
Augustin Lemesle's avatar
Augustin Lemesle committed
                    </div>
Augustin Lemesle's avatar
Augustin Lemesle committed
                  </div>

                  <div class="swiper-slide">
                    <div role="button" class="slideTxt" target="tab_3">
                      <span>Dependency Analysis</span>
Augustin Lemesle's avatar
Augustin Lemesle committed
                    </div>
Augustin Lemesle's avatar
Augustin Lemesle committed
                  </div>

                  <div class="swiper-slide">
                    <div role="button" class="slideTxt" target="tab_4">
                      <span>Impact Analysis</span>
Augustin Lemesle's avatar
Augustin Lemesle committed
                    </div>
                  </div>
                </div>
Augustin Lemesle's avatar
Augustin Lemesle committed

                <div class="swiper-button-prev"></div>

                <div class="swiper-button-next"></div>
Augustin Lemesle's avatar
Augustin Lemesle committed
              </div>
Augustin Lemesle's avatar
Augustin Lemesle committed
            </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>
Augustin Lemesle's avatar
Augustin Lemesle committed
                      </div>

Augustin Lemesle's avatar
Augustin Lemesle committed
                      <div class="title">
                        <b>02</b><span>Option <samp>-val</samp> runs the Evolved Value Analysis plug-in and prepares its
                        results.</span>
                      </div>
Augustin Lemesle's avatar
Augustin Lemesle committed

Augustin Lemesle's avatar
Augustin Lemesle committed
                      <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%">
 <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>
 <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">&amp;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&lt;</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">-slevel</span> <span style="color: #3677a9">10<span class="tooltip">3</span></span> <span style="color: #d0d0d0">-val<span class="tooltip">2</span> <span style="color: #d0d0d0">first.c<span class="tooltip">1</span><span class="arrowTooltip right"><span><span class="title"><b>02</b><span>Option <samp>-val</samp> runs the Evolved Value Analysis plug-in and prepares its results.</span></span></span></span><u></u></span>
Augustin Lemesle's avatar
Augustin Lemesle committed
</span>
</pre>
                            </div>
                          </div>
                        </div>
                      </div>
                    </div>
Augustin Lemesle's avatar
Augustin Lemesle committed
                  </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>
Augustin Lemesle's avatar
Augustin Lemesle committed
                      </div>

Augustin Lemesle's avatar
Augustin Lemesle committed
                      <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%">
  <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">&lt;</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>
Augustin Lemesle's avatar
Augustin Lemesle committed
</pre>
                            </div>
                          </div>
                        </div>
                      </div>
                    </div>
Augustin Lemesle's avatar
Augustin Lemesle committed
                  </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>
Augustin Lemesle's avatar
Augustin Lemesle committed
                      </div>
Augustin Lemesle's avatar
Augustin Lemesle committed

                      <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%">
  <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">&lt;</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>
Augustin Lemesle's avatar
Augustin Lemesle committed
 
Augustin Lemesle's avatar
Augustin Lemesle committed
 <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>
Augustin Lemesle's avatar
Augustin Lemesle committed
</pre>
                            </div>
                          </div>
                        </div>
                      </div>
                    </div>
Augustin Lemesle's avatar
Augustin Lemesle committed
                  </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>
Augustin Lemesle's avatar
Augustin Lemesle committed
                      </div>
Augustin Lemesle's avatar
Augustin Lemesle committed

                      <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%">
<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>
Augustin Lemesle's avatar
Augustin Lemesle committed
<span style="color: #d0d0d0">{</span>
Augustin Lemesle's avatar
Augustin Lemesle committed
  <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">&lt;</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>
Augustin Lemesle's avatar
Augustin Lemesle committed
<span style="color: #d0d0d0">}</span>
</pre>
                            </div>
                          </div>
                        </div>
                      </div>
                    </div>
Augustin Lemesle's avatar
Augustin Lemesle committed
                  </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>
Augustin Lemesle's avatar
Augustin Lemesle committed
                      </div>
Augustin Lemesle's avatar
Augustin Lemesle committed

                      <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%">
<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>
Augustin Lemesle's avatar
Augustin Lemesle committed
<span style="color: #d0d0d0">{</span>
Augustin Lemesle's avatar
Augustin Lemesle committed
  <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">&lt;</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>
Augustin Lemesle's avatar
Augustin Lemesle committed
<span style="color: #d0d0d0">}</span>
</pre>
                            </div>
                          </div>
                        </div>
                      </div>
                    </div>
                  </div>
                </div>
              </div>
            </div>
Augustin Lemesle's avatar
Augustin Lemesle committed
          </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>How can<br>
              Frama-C<br>
              be used?</h2>

              <div class="circle robustness"></div>

              <div class="circle codeStandard"></div>

              <div class="circle security"></div><a href="using-frama-c/index.html#group_robustness" 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="using-frama-c/index.html#group_code_standards" 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="using-frama-c/index.html#group_security_defects" class="security" role=
              "button"><span class="icon"><i class=" icon-lock"></i></span> <span class="txt">Detect <b>security
              defects</b></span></a>
Augustin Lemesle's avatar
Augustin Lemesle committed
            </div>
Augustin Lemesle's avatar
Augustin Lemesle committed
          </div>

          <div id="about_iv_point" class="inviewCenter"></div>
        </section>

        <section id="latest_events" class="section calendarScreen fullScreen" data-title="FOLLOW">
          <div class="sectionContent">
            <h2>Frama-C Calendar</h2>

            <div id="event_detail_swiper" class="eventDetailsBlock swiper-container">
              <div class="swiper-wrapper">
                <div class="swiper-slide">
                  <div class="eventDetail" id="post_details_486">
                    <figure>
                      <span class="img" style=
                      "background-image: url(https://framac.s3.amazonaws.com/production/uploads/2017/07/PrtScr-capture_2686.jpg"></span>
                    </figure>

                    <div class="contentBlk">
                      <time><b>16</b><b>May</b><small>2017</small></time>

                      <div>
                        <h3>The first version of the Frama  C Plugins</h3>

                        <p>Lorem ipsum dolor sit amet, consectetur adipiscing elit, sed do eiusmod tempor incididunt ut labore et
                        dolore magna aliqua. Ut enim ad minim veniam, quis nostrud exercitation ullamco laboris nisi ut aliquip ex
                        ea commodo consequat. Duis aute irure dolor in reprehenderit...</p><a class="read-more link" href=
                        "http://www.gmail.com" target="_blank">Read More</a>
Augustin Lemesle's avatar
Augustin Lemesle committed
                      </div>
                    </div>
                  </div>
Augustin Lemesle's avatar
Augustin Lemesle committed
                </div>

                <div class="swiper-slide">
                  <div class="eventDetail" id="post_details_64">
                    <figure>
                      <span class="img" style=
                      "background-image: url(https://framac.s3.amazonaws.com/production/uploads/2017/07/01-1.jpg"></span>
                    </figure>

                    <div class="contentBlk">
                      <time><b>08</b><b>Jul</b><small>2017</small></time>

                      <div>
                        <h3>Lorem Ipsum</h3>

                        <p>It is a long established fact that a reader will be distracted by the readable content of a page when
                        looking at its layout. The point of using Lorem Ipsum is that it has a more-or-less normal distribution of
                        letters, as opposed...</p>
Augustin Lemesle's avatar
Augustin Lemesle committed
                      </div>
                    </div>
                  </div>
Augustin Lemesle's avatar
Augustin Lemesle committed
                </div>

                <div class="swiper-slide">
                  <div class="eventDetail" id="post_details_70">
                    <figure>
                      <span class="img" style=
                      "background-image: url(https://framac.s3.amazonaws.com/production/uploads/2017/07/01-1.jpg"></span>
                    </figure>

                    <div class="contentBlk">
                      <time><b>28</b><b>Jul</b><small>2017</small></time>

                      <div>
                        <h3>of letters, as opposed to using of letters, as opposed to using</h3>

                        <p>It is a long established fact that a reader will be distracted by the readable content of a page when
                        looking at its layout. The point of using Lorem Ipsum is that it has a more-or-less normal distribution of
                        letters, as opposed...</p><a class="read-more link" href="https://framac-dev.dev.kacdn.net/" target=
                        "_blank">Read More</a>
Augustin Lemesle's avatar
Augustin Lemesle committed
                      </div>
                    </div>
                  </div>
Augustin Lemesle's avatar
Augustin Lemesle committed
                </div>

                <div class="swiper-slide">
                  <div class="eventDetail" id="post_details_71">
                    <figure>
                      <span class="img" style=
                      "background-image: url(https://framac.s3.amazonaws.com/production/uploads/2017/07/01-1.jpg"></span>
                    </figure>

                    <div class="contentBlk">
                      <time><b>29</b><b>Jul</b><small>2017</small></time>

                      <div>
                        <h3>of letters, as opposed to using</h3>

                        <p>It is a long established fact that a reader will be distracted by the readable content of a page when
                        looking at its layout. The point of using Lorem Ipsum is that it has a more-or-less normal distribution of
                        letters, as opposed...</p>
Augustin Lemesle's avatar
Augustin Lemesle committed
                      </div>
                    </div>
                  </div>
Augustin Lemesle's avatar
Augustin Lemesle committed
                </div>

                <div class="swiper-slide">
                  <div class="eventDetail" id="post_details_525">
                    <figure>
                      <span class="img" style=
                      "background-image: url(https://framac.s3.amazonaws.com/production/uploads/2017/08/DragonFull.png"></span>
                    </figure>

                    <div class="contentBlk">
                      <time><b>02</b><b>Aug</b><small>2017</small></time>

                      <div>
                        <h3>frama-clang 0.0.3, compatible with Frama-C 15 is out.</h3>

                        <p>Frama-Clang is a plugin that allows Frama-C to take as input C++ programs. As its name implies, it is
                        based on the clang compiler, the C/C++/Objective-C front-end of the llvm platform. Changes Compatibility
                        with Frama-C 15 Phosphorus Improved handling of constructors and...</p><a class="read-more link" href=
                        "http://frama-c.com/frama-clang.html" target="_blank">Read More</a>
Augustin Lemesle's avatar
Augustin Lemesle committed
                      </div>
                    </div>
                  </div>
Augustin Lemesle's avatar
Augustin Lemesle committed
                </div>

                <div class="swiper-slide">
                  <div class="eventDetail" id="post_details_62">
                    <figure>
                      <span class="img" style=
                      "background-image: url(https://framac.s3.amazonaws.com/production/uploads/2017/07/1.jpg"></span>
                    </figure>

                    <div class="contentBlk">
                      <time><b>08</b><b>Aug</b><small>2017</small></time>

                      <div>
                        <h3>The First Version Of the frama-clang plugin</h3>

                        <p>The first version of the Frama-Clang plugin, an experimental C++ front-end for Frama-C, is available.
                        The first version of the Frama-Clang plugin, an experimental C++ front-end for Frama-C, is available. Nulla
                        quis lorem ut libero malesuada feugiat. Cras ultricies ligula sed magna...</p>
Augustin Lemesle's avatar
Augustin Lemesle committed
                      </div>
                    </div>
                  </div>
Augustin Lemesle's avatar
Augustin Lemesle committed
                </div>

                <div class="swiper-slide">
                  <div class="eventDetail" id="post_details_484">
                    <figure>
                      <span class="img" style=
                      "background-image: url(https://framac.s3.amazonaws.com/production/uploads/2017/07/slider-logation-img-desk-01.jpg">
                      </span>
                    </figure>

                    <div class="contentBlk">
                      <time><b>09</b><b>Aug</b><small>2017</small></time>

                      <div>
                        <h3>Event 1</h3>

                        <p>Lorem ipsum dolor sit amet, consectetur adipiscing elit, sed do eiusmod tempor incididunt ut labore et
                        dolore magna aliqua. Ut enim ad minim veniam, quis nostrud exercitation ullamco laboris nisi ut aliquip ex
                        ea commodo consequat. Duis aute irure dolor in reprehenderit...</p><a class="read-more link" href=
                        "http://www.gmail.com" target="_blank">Read More</a>
Augustin Lemesle's avatar
Augustin Lemesle committed
                      </div>
                    </div>
                  </div>
Augustin Lemesle's avatar
Augustin Lemesle committed
                </div>

                <div class="swiper-slide">
                  <div class="eventDetail" id="post_details_66">
                    <figure>
                      <span class="img" style=
                      "background-image: url(https://framac.s3.amazonaws.com/production/uploads/2017/07/3-1.jpg"></span>
                    </figure>

                    <div class="contentBlk">
                      <time><b>10</b><b>Aug</b><small>2017</small></time>

                      <div>
                        <h3>Lorem Ipsum</h3>

                        <p>It is a long established fact that a reader will be distracted by the readable content of a page when
                        looking at its layout. The point of using Lorem Ipsum is that it has a more-or-less normal distribution of
                        letters, as opposed...</p>
Augustin Lemesle's avatar
Augustin Lemesle committed
                      </div>
                    </div>
                  </div>
Augustin Lemesle's avatar
Augustin Lemesle committed
                </div>

                <div class="swiper-slide">
                  <div class="eventDetail" id="post_details_69">
                    <figure>
                      <span class="img" style=
                      "background-image: url(https://framac.s3.amazonaws.com/production/uploads/2017/07/3-1.jpg"></span>
                    </figure>

                    <div class="contentBlk">
                      <time><b>15</b><b>Aug</b><small>2017</small></time>

                      <div>
                        <h3>It is a long It is a long It is a long</h3>

                        <p>It is a long established fact that a reader will be distracted by the readable content of a page when
                        looking at its layout. The point of using Lorem Ipsum is that it has a more-or-less normal distribution of
                        letters, as opposed...</p>
Augustin Lemesle's avatar
Augustin Lemesle committed
                      </div>
                    </div>
                  </div>
Augustin Lemesle's avatar
Augustin Lemesle committed
                </div>

                <div class="swiper-slide">
                  <div class="eventDetail" id="post_details_485">
                    <figure>
                      <span class="img" style=
                      "background-image: url(https://framac.s3.amazonaws.com/production/uploads/2017/07/bolt.jpg"></span>
                    </figure>

                    <div class="contentBlk">
                      <time><b>15</b><b>Aug</b><small>2017</small></time>

                      <div>
                        <h3>Event 2</h3>

                        <p>Lorem ipsum dolor sit amet, consectetur adipiscing elit, sed do eiusmod tempor incididunt ut labore et
                        dolore magna aliqua. Ut enim ad minim veniam, quis nostrud exercitation ullamco laboris nisi ut aliquip ex
                        ea commodo consequat. Duis aute irure dolor in reprehenderit...</p><a class="read-more link" href=
                        "http://www.gmail.com" target="_blank">Read More</a>
Augustin Lemesle's avatar
Augustin Lemesle committed
                      </div>
                    </div>
                  </div>
                </div>
              </div>
            </div>
Augustin Lemesle's avatar
Augustin Lemesle committed
          </div>

          <div class="eventScaleBlock">
            <div class="scaleBg">
              <u></u>
            </div>

            <div id="event_calender_swiper" class="swiper-container">
              <div class="swiper-wrapper">
                <div class="swiper-slide">
                  <a role="button" class="eventLink"><time><b>16</b><small>May</small></time><span>The first version of the Frama 
                  C...</span></a>
                </div>

                <div class="swiper-slide">
                  <a role="button" class="eventLink"><time><b>08</b><small>Jul</small></time><span>Lorem Ipsum</span></a>
                </div>

                <div class="swiper-slide">
                  <a role="button" class="eventLink"><time><b>28</b><small>Jul</small></time><span>of letters, as opposed to using
                  of letters,...</span></a>
                </div>

                <div class="swiper-slide">
                  <a role="button" class="eventLink"><time><b>29</b><small>Jul</small></time><span>of letters, as opposed to
                  using</span></a>
                </div>

                <div class="swiper-slide">
                  <a role="button" class="eventLink"><time><b>02</b><small>Aug</small></time><span>frama-clang 0.0.3, compatible
                  with Frama-C 15 is out.</span></a>
                </div>

                <div class="swiper-slide">
                  <a role="button" class="eventLink"><time><b>08</b><small>Aug</small></time><span>The First Version Of the
                  frama-clang plugin</span></a>
                </div>

                <div class="swiper-slide">
                  <a role="button" class="eventLink"><time><b>09</b><small>Aug</small></time><span>Event 1</span></a>
                </div>

                <div class="swiper-slide">
                  <a role="button" class="eventLink"><time><b>10</b><small>Aug</small></time><span>Lorem Ipsum</span></a>
                </div>

                <div class="swiper-slide">
                  <a role="button" class="eventLink"><time><b>15</b><small>Aug</small></time><span>It is a long It is a
                  long...</span></a>
                </div>

                <div class="swiper-slide">
                  <a role="button" class="eventLink"><time><b>15</b><small>Aug</small></time><span>Event 2</span></a>
Augustin Lemesle's avatar
Augustin Lemesle committed
                </div>
              </div>
            </div>
Augustin Lemesle's avatar
Augustin Lemesle committed
          </div>

          <div id="events_iv_point" class="inviewCenter"></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="get-frama-c/index.html" class=
                "aluminiumVersion">Aluminum</a><a href="framac-versions/index.html" class="previousVersion">Previous Versions</a>
              </nav>
Augustin Lemesle's avatar
Augustin Lemesle committed
            </div>
Augustin Lemesle's avatar
Augustin Lemesle committed

            <div class="linkBlk">
              <p>Frama-C is only available for Desktop</p><a class="btn mobileLink" href="get-frama-c/index.html"><span>Discover
              more about <b>Frama-C</b></span></a> <a class="btn cta-download" href="get-frama-c/index.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>
Augustin Lemesle's avatar
Augustin Lemesle committed
            </div>
Augustin Lemesle's avatar
Augustin Lemesle committed
          </div>

          <div id="download_iv_point" class="inviewCenter"></div>
        </section>

        <footer id="footer" class="mainFooter">
          <a href="index.html" rel="home" class="footLogo" title="Frama-C"><img src="app/themes/frama/assets/img/framac.gif" alt=
          ""></a>

          <nav>
            <a href="https://twitter.com/frama_c" target="_blank" class="twitterLink"><i class="icon icon-twitter"></i></a>
          </nav>

          <div class="copyright">
            <span>Copyright © 2015-2018 Frama-C. All Rights Reserved.</span>

            <ul id="menu-footer-menu" class="footer-list-menu">
              <li id="menu-item-214" class="menu-item menu-item-type-post_type menu-item-object-page menu-item-214">
                <a href="terms-of-use/index.html">Terms Of Use</a>
              </li>

              <li id="menu-item-233" class="menu-item menu-item-type-post_type menu-item-object-page menu-item-233">
                <a href="authors/index.html">Authors</a>
              </li>
            </ul>
          </div>

          <div id="copyright" class="hide">
             2019 Frama-C. All Rights Reserved.
          </div>
        </footer>

        <section class="bgTitleBlk titleIn white">
          <div class="upperBlk">
            <div class="upperType">
              SECURE
Augustin Lemesle's avatar
Augustin Lemesle committed
            </div>
Augustin Lemesle's avatar
Augustin Lemesle committed
          </div>

          <div class="lowerBlk">
            <div class="lowerType">
              SECURE
Augustin Lemesle's avatar
Augustin Lemesle committed
            </div>
Augustin Lemesle's avatar
Augustin Lemesle committed
          </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>
Augustin Lemesle's avatar
Augustin Lemesle committed
    </div>
Augustin Lemesle's avatar
Augustin Lemesle committed
  </div><script type='text/javascript' src='app/themes/frama/build/js/manifest.7c8986b0ca7d8db7279d.js'>
</script><script type='text/javascript' src='app/themes/frama/build/js/lib.7c8986b0ca7d8db7279d.js'>
</script><script type='text/javascript'>
var ajax = {"url":"http:\/\/localhost:8000\/wp\/wp-admin\/admin-ajax.php","ajax_var":{"template_directory_uri":"http:\/\/localhost:8000\/app\/themes\/frama"},"apikey":"AIzaSyDwKjbfd43-rY5muMW76XUdAFMb7mL9kU8","nonce":"eb10361e5c"};
  </script><script type='text/javascript' src='app/themes/frama/build/js/main.7c8986b0ca7d8db7279d.js'>
Augustin Lemesle's avatar
Augustin Lemesle committed
</script>
Augustin Lemesle's avatar
Augustin Lemesle committed
</body>
Augustin Lemesle's avatar
Augustin Lemesle committed
</html>