Skip to content
Snippets Groups Projects
Normal view Permalink
index.html 26.7 KiB
Newer Older
Augustin Lemesle's avatar
Change to jekyll  
Augustin Lemesle committed
1 2 3 4 5 
---
css: home
layout: default
title: Frama-C
---
Augustin Lemesle's avatar
tidy better  
Augustin Lemesle committed
6 7 8 

<body class="home page-template-default page page-id-7 nonTouch">
  <div id="wrapper" class="hfeed">
Yaelle Vincont's avatar
[refactor] remove trailing whitespaces  
Yaelle Vincont committed
9
Augustin Lemesle's avatar
Change to jekyll  
Augustin Lemesle committed
10 
	{% include headers.html %}
Augustin Lemesle's avatar
tidy better  
Augustin Lemesle committed
11 12 

    <div id="container" class="mainContainer">
Augustin Lemesle's avatar
Change to jekyll  
Augustin Lemesle committed
13 
      <div class="pageContent titleIn secure" id="content" role="main">
Augustin Lemesle's avatar
tidy better  
Augustin Lemesle committed
14 15 16 17 
        <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>
Augustin Lemesle's avatar
malberti fixes  
Augustin Lemesle committed
18 
            <p class="banner-desc">The Frama-C source code analysis platform provides tools to make your C/C++ code safer and more
Augustin Lemesle's avatar
Change to jekyll  
Augustin Lemesle committed
19 
            secure.</p><a class="btn cta-download" href="/html/get-frama-c.html"><span>Download <b>Frama-C</b><span><i class=
Augustin Lemesle's avatar
tidy better  
Augustin Lemesle committed
20 21 
            "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
Initial commit
Augustin Lemesle committed
22 
          </div>
Augustin Lemesle's avatar
tidy better  
Augustin Lemesle committed
23 24 25 26 27 28 29 

          <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">
Augustin Lemesle's avatar
malberti fixes  
Augustin Lemesle committed
30 
            <h3>Overview of a Frama-C analysis for<br>
Augustin Lemesle's avatar
tidy better  
Augustin Lemesle committed
31 32 33 34 35 36 37 38 39 40 
            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
Initial commit
Augustin Lemesle committed
41 
                    </div>
Augustin Lemesle's avatar
tidy better  
Augustin Lemesle committed
42 43 44 45 46 
                  </div>

                  <div class="swiper-slide">
                    <div role="button" class="slideTxt" target="tab_1">
                      <span>Value Analysis</span>
Augustin Lemesle's avatar
Initial commit
Augustin Lemesle committed
47 
                    </div>
Augustin Lemesle's avatar
tidy better  
Augustin Lemesle committed
48 49 50 51 52 
                  </div>

                  <div class="swiper-slide">
                    <div role="button" class="slideTxt" target="tab_2">
                      <span>Effects Analysis</span>
Augustin Lemesle's avatar
Initial commit
Augustin Lemesle committed
53 
                    </div>
Augustin Lemesle's avatar
tidy better  
Augustin Lemesle committed
54 55 56 57 58 
                  </div>

                  <div class="swiper-slide">
                    <div role="button" class="slideTxt" target="tab_3">
                      <span>Dependency Analysis</span>
Augustin Lemesle's avatar
Initial commit
Augustin Lemesle committed
59 
                    </div>
Augustin Lemesle's avatar
tidy better  
Augustin Lemesle committed
60 61 62 63 64 
                  </div>

                  <div class="swiper-slide">
                    <div role="button" class="slideTxt" target="tab_4">
                      <span>Impact Analysis</span>
Augustin Lemesle's avatar
Initial commit
Augustin Lemesle committed
65 66 67 
                    </div>
                  </div>
                </div>
Augustin Lemesle's avatar
tidy better  
Augustin Lemesle committed
68 69 70 71 

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

                <div class="swiper-button-next"></div>
Augustin Lemesle's avatar
Initial commit
Augustin Lemesle committed
72 
              </div>
Augustin Lemesle's avatar
tidy better  
Augustin Lemesle committed
73 74 75 76 77 78 79 80 81 
            </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
Initial commit
Augustin Lemesle committed
82 83 
                      </div>
Augustin Lemesle's avatar
tidy better  
Augustin Lemesle committed
84 
                      <div class="title">
Yaelle Vincont's avatar
[ref/index] rename Eva  
Yaelle Vincont committed
85 
                        <b>02</b><span>Option <samp>-eva</samp> runs the Eva plug-in and prepares its
Augustin Lemesle's avatar
tidy better  
Augustin Lemesle committed
86 87 
                        results.</span>
                      </div>
Augustin Lemesle's avatar
Initial commit
Augustin Lemesle committed
88
Augustin Lemesle's avatar
tidy better  
Augustin Lemesle committed
89 90 91 92 93 94 95 96 97 98 99 
                      <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;">
Yaelle Vincont's avatar
[index] fix Value to Eva  
Yaelle Vincont committed
100
Augustin Lemesle's avatar
minor fixes  
Augustin Lemesle committed
101 
                              <pre style="margin: 0; line-height: 125%; background: #202020;">
Augustin Lemesle's avatar
tidy better  
Augustin Lemesle committed
102 103 104 105 106 
 <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=
Augustin Lemesle's avatar
Add number 3 on front page  
Augustin Lemesle committed
107 108 
"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>
Augustin Lemesle's avatar
tidy better  
Augustin Lemesle committed
109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 
 <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=
Augustin Lemesle's avatar
malberti fixes  
Augustin Lemesle committed
124 125 
"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>
Augustin Lemesle's avatar
Initial commit
Augustin Lemesle committed
126 127 128 129 130 131 
</pre>
                            </div>
                          </div>
                        </div>
                      </div>
                    </div>
Augustin Lemesle's avatar
tidy better  
Augustin Lemesle committed
132 133 134 135 136 137 138 
                  </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
Initial commit
Augustin Lemesle committed
139 140 
                      </div>
Augustin Lemesle's avatar
tidy better  
Augustin Lemesle committed
141 142 143 144 145 146 147 148 149 150 151 152 
                      <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;">
Augustin Lemesle's avatar
minor fixes  
Augustin Lemesle committed
153 
                              <pre style="margin: 0; line-height: 125%; background: #202020;">
Augustin Lemesle's avatar
tidy better  
Augustin Lemesle committed
154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 
  <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
Initial commit
Augustin Lemesle committed
186 187 188 189 190 191 
</pre>
                            </div>
                          </div>
                        </div>
                      </div>
                    </div>
Augustin Lemesle's avatar
tidy better  
Augustin Lemesle committed
192 193 194 195 196 197 198 
                  </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
Initial commit
Augustin Lemesle committed
199 
                      </div>
Augustin Lemesle's avatar
tidy better  
Augustin Lemesle committed
200 201 202 203 204 205 206 207 208 209 210 211 

                      <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;">
Augustin Lemesle's avatar
minor fixes  
Augustin Lemesle committed
212 
                              <pre style="margin: 0; line-height: 125%; background: #202020;">
Augustin Lemesle's avatar
tidy better  
Augustin Lemesle committed
213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 
  <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>
Yaelle Vincont's avatar
[refactor] remove trailing whitespaces  
Yaelle Vincont committed
233
Augustin Lemesle's avatar
tidy better  
Augustin Lemesle committed
234 235 236 237 
 <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
Initial commit
Augustin Lemesle committed
238 239 240 241 242 243 
</pre>
                            </div>
                          </div>
                        </div>
                      </div>
                    </div>
Augustin Lemesle's avatar
tidy better  
Augustin Lemesle committed
244 245 246 247 248 249 250 
                  </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
Initial commit
Augustin Lemesle committed
251 
                      </div>
Augustin Lemesle's avatar
tidy better  
Augustin Lemesle committed
252 253 254 255 256 257 258 259 260 261 262 263 

                      <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;">
Augustin Lemesle's avatar
minor fixes  
Augustin Lemesle committed
264 
                              <pre style="margin: 0; line-height: 125%; background: #202020;">
Augustin Lemesle's avatar
tidy better  
Augustin Lemesle committed
265 266 
<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
Initial commit
Augustin Lemesle committed
267 
<span style="color: #d0d0d0">{</span>
Augustin Lemesle's avatar
tidy better  
Augustin Lemesle committed
268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 
  <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
Initial commit
Augustin Lemesle committed
290 291 292 293 294 295 296 
<span style="color: #d0d0d0">}</span>
</pre>
                            </div>
                          </div>
                        </div>
                      </div>
                    </div>
Augustin Lemesle's avatar
tidy better  
Augustin Lemesle committed
297 298 299 300 301 302 
                  </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
Initial commit
Augustin Lemesle committed
303 
                      </div>
Augustin Lemesle's avatar
tidy better  
Augustin Lemesle committed
304 305 306 307 308 309 310 311 312 313 314 315 

                      <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;">
Augustin Lemesle's avatar
minor fixes  
Augustin Lemesle committed
316 
                              <pre style="margin: 0; line-height: 125%; background: #202020;">
Augustin Lemesle's avatar
tidy better  
Augustin Lemesle committed
317 318 
<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
Initial commit
Augustin Lemesle committed
319 
<span style="color: #d0d0d0">{</span>
Augustin Lemesle's avatar
tidy better  
Augustin Lemesle committed
320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 
  <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
Initial commit
Augustin Lemesle committed
342 343 344 345 346 347 348 349 350 351 352 
<span style="color: #d0d0d0">}</span>
</pre>
                            </div>
                          </div>
                        </div>
                      </div>
                    </div>
                  </div>
                </div>
              </div>
            </div>
Augustin Lemesle's avatar
tidy better  
Augustin Lemesle committed
353 354 355 356 357 358 359 360 
          </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">
Augustin Lemesle's avatar
malberti fixes  
Augustin Lemesle committed
361 
              <h2>What is<br>
Augustin Lemesle's avatar
tidy better  
Augustin Lemesle committed
362 
              Frama-C<br>
Augustin Lemesle's avatar
malberti fixes  
Augustin Lemesle committed
363 
              used for?</h2>
Augustin Lemesle's avatar
tidy better  
Augustin Lemesle committed
364 365 366 367 368 

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

              <div class="circle codeStandard"></div>
Augustin Lemesle's avatar
add ack  
Augustin Lemesle committed
369 
              <div class="circle security"></div><a href="/html/using-frama-c.html" class="robustness" role=
Augustin Lemesle's avatar
tidy better  
Augustin Lemesle committed
370 
              "button"><span class="icon"><i class=" icon-thumb"></i></span> <span class="txt">Test your software's
Augustin Lemesle's avatar
add ack  
Augustin Lemesle committed
371 
              <b>robustness</b></span></a><a href="/html/using-frama-c.html" class="codeStandard" role=
Augustin Lemesle's avatar
tidy better  
Augustin Lemesle committed
372 
              "button"><span class="icon"><i class=" icon-code"></i></span> <span class="txt">Enforce <b>code
Augustin Lemesle's avatar
add ack  
Augustin Lemesle committed
373 
              requirements</b></span></a><a href="/html/using-frama-c.html" class="security" role=
Augustin Lemesle's avatar
tidy better  
Augustin Lemesle committed
374 375 
              "button"><span class="icon"><i class=" icon-lock"></i></span> <span class="txt">Detect <b>security
              defects</b></span></a>
Augustin Lemesle's avatar
Initial commit
Augustin Lemesle committed
376 
            </div>
Augustin Lemesle's avatar
tidy better  
Augustin Lemesle committed
377 378 379 380 381 
          </div>

          <div id="about_iv_point" class="inviewCenter"></div>
        </section>
David Bühler's avatar
Timeline: renames calendar into timeline.  
David Bühler committed
382 
        <section id="latest_events" class="section calendarScreen fullScreen" data-title="TIMELINE">
Augustin Lemesle's avatar
tidy better  
Augustin Lemesle committed
383 
          <div class="sectionContent">
David Bühler's avatar
Timeline: renames calendar into timeline.  
David Bühler committed
384 
            <h2>Frama-C Timeline</h2>
Augustin Lemesle's avatar
tidy better  
Augustin Lemesle committed
385 386 387 

            <div id="event_detail_swiper" class="eventDetailsBlock swiper-container">
              <div class="swiper-wrapper">
Marc Coudriau's avatar
Timeline in the correct order  
Marc Coudriau committed
388 
			    {% for event in site.events %}
Augustin Lemesle's avatar
tidy better  
Augustin Lemesle committed
389 390 391 392 
                <div class="swiper-slide">
                  <div class="eventDetail" id="post_details_486">
                    <figure>
                      <span class="img" style=
Augustin Lemesle's avatar
Add authors  
Augustin Lemesle committed
393 
                      "background-image: url({{ event.image }})"></span>
Augustin Lemesle's avatar
tidy better  
Augustin Lemesle committed
394 395 396 
                    </figure>

                    <div class="contentBlk">
Augustin Lemesle's avatar
Add authors  
Augustin Lemesle committed
397 398 399 
					  <time>{{ event.date | date: "<b>%-d</b><b>%B</b><small>%Y</small>" }}</time>
					  <div>
                        <h3>{{ event.title }}</h3>
Augustin Lemesle's avatar
tidy better  
Augustin Lemesle committed
400
David Bühler's avatar
Calendar: sorts events by reversed date and do not strip nor truncate the description.  
David Bühler committed
401 
                        <p>{{ event.content }}</p>
Augustin Lemesle's avatar
Initial commit
Augustin Lemesle committed
402 403 404 405 
                      </div>
                    </div>
                  </div>
                </div>
Augustin Lemesle's avatar
Add authors  
Augustin Lemesle committed
406 
				{% endfor %}
Augustin Lemesle's avatar
Initial commit
Augustin Lemesle committed
407 408 
              </div>
            </div>
Augustin Lemesle's avatar
tidy better  
Augustin Lemesle committed
409 410 411 412 413 414 415 416 417 
          </div>

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

            <div id="event_calender_swiper" class="swiper-container">
              <div class="swiper-wrapper">
Marc Coudriau's avatar
Timeline in the correct order  
Marc Coudriau committed
418 419 
			    {% for event in site.events %}
                  <div class="swiper-slide"
Augustin Lemesle's avatar
malberti fixes  
Augustin Lemesle committed
420 
                       {% if forloop.last %}
Marc Coudriau's avatar
Timeline in the correct order  
Marc Coudriau committed
421 422 423 
                       data-eventdate="latest"
                       {% endif %}
                  >
David Bühler's avatar
Timeline: show the year instead of day/month in the bubble.  
David Bühler committed
424 
                  <a role="button" class="eventLink"><time>{{ event.date | date: "<b>%Y</b>" }}</time><span>{{ event.title }}</span></a>
Augustin Lemesle's avatar
Initial commit
Augustin Lemesle committed
425 
                </div>
Augustin Lemesle's avatar
Add authors  
Augustin Lemesle committed
426 
				{% endfor %}
Augustin Lemesle's avatar
Initial commit
Augustin Lemesle committed
427 428 
              </div>
            </div>
Augustin Lemesle's avatar
tidy better  
Augustin Lemesle committed
429 430 431 432 433 434 435 436 437 438 439 
          </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>
Augustin Lemesle's avatar
Added missing plugins  
Augustin Lemesle committed
440 
                <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>
Augustin Lemesle's avatar
tidy better  
Augustin Lemesle committed
441 
              </nav>
Augustin Lemesle's avatar
Initial commit
Augustin Lemesle committed
442 
            </div>
Augustin Lemesle's avatar
tidy better  
Augustin Lemesle committed
443 444 

            <div class="linkBlk">
Augustin Lemesle's avatar
Change to jekyll  
Augustin Lemesle committed
445 446 
              <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
Augustin Lemesle's avatar
tidy better  
Augustin Lemesle committed
447 448 
              <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
Initial commit
Augustin Lemesle committed
449 
            </div>
Augustin Lemesle's avatar
tidy better  
Augustin Lemesle committed
450 451 452 453 
          </div>

          <div id="download_iv_point" class="inviewCenter"></div>
        </section>
Yaelle Vincont's avatar
[refactor] remove trailing whitespaces  
Yaelle Vincont committed
454
Augustin Lemesle's avatar
Change to jekyll  
Augustin Lemesle committed
455 
      {% include footer.html %}
Augustin Lemesle's avatar
tidy better  
Augustin Lemesle committed
456 457 458 459 460 

        <section class="bgTitleBlk titleIn white">
          <div class="upperBlk">
            <div class="upperType">
              SECURE
Augustin Lemesle's avatar
Initial commit
Augustin Lemesle committed
461 
            </div>
Augustin Lemesle's avatar
tidy better  
Augustin Lemesle committed
462 463 464 465 466 
          </div>

          <div class="lowerBlk">
            <div class="lowerType">
              SECURE
Augustin Lemesle's avatar
Initial commit
Augustin Lemesle committed
467 
            </div>
Augustin Lemesle's avatar
tidy better  
Augustin Lemesle committed
468 469 
          </div>
        </section>
Augustin Lemesle's avatar
Change to jekyll  
Augustin Lemesle committed
470 471 472 
      </div>
	  <script>
		var homeLabels = {secure_label    : 'Secure',error_label     : 'Error',about_label     : 'About',follow_label    : 'Follow',footer_label    : 'Get Frama-C',};
Augustin Lemesle's avatar
tidy better  
Augustin Lemesle committed
473 474 475 
      </script>

      <div class="clear"></div>
Augustin Lemesle's avatar
Initial commit
Augustin Lemesle committed
476 
    </div>
Augustin Lemesle's avatar
Change to jekyll  
Augustin Lemesle committed
477 
  </div>
David Bühler's avatar
Calendar: sorts events by reversed date and do not strip nor truncate the description.  
David Bühler committed
478 
<body>