2011-09-16-Safe-donut.html

---
layout: post
author: Pascal Cuoq
date: 2011-09-16 22:57 +0200
categories: donut floating-point position value value-builtins
format: xhtml
title: "Safe donut"
summary: 
---
{% raw %}
<p>This post documents the steps I followed in order to finish verifying function <code>compute()</code>, picking up from <a href="/donut/facetious-colleagues/floating-point/value/value-builtins/2011/09/17/Probably-safe-donut">there</a>.</p> 
<h2>Previously on this blog</h2> 
<p>In last episode  we had found that some sub-cubes in the search space appeared to lead to dangerous value sets for variable <code>N</code>. These sets were:</p> 
<pre>        N ∈ {10; 11; 12} 
        N ∈ {6; 7; 8; 9; 10; 11; 12} 
        N ∈ {7; 8; 9; 10; 11; 12} 
        N ∈ {7; 8; 9; 10; 11; 12; 13} 
        N ∈ {8; 9; 10; 11; 12} 
        N ∈ {8; 9; 10; 11; 12; 13} 
        N ∈ {9; 10; 11; 12} 
        N ∈ {9; 10; 11; 12; 13} 
</pre> 
<p>There are only eight dangerous value sets for <code>N</code>  but these correspond to many values of input variables <code>An  Bn  in  jn</code> in the <a href="/assets/img/blog/imported-posts/an.c">analysis context</a> we wrote for the occasion. 
Grepping for each of these eight lines in the original logs allows to get the corresponding values of <code>An  Bn  in  jn</code>. These are the values for which we haven't concluded yet that <code>compute()</code> is safe:</p> 
<pre>for i in 1 2 3 4 
do 
    for line in \ 
	"N ∈ {10; 11; 12}" \ 
	"N ∈ {6; 7; 8; 9; 10; 11; 12}" \ 
	"N ∈ {7; 8; 9; 10; 11; 12}" \ 
	"N ∈ {7; 8; 9; 10; 11; 12; 13}" \ 
	"N ∈ {8; 9; 10; 11; 12}" \ 
	"N ∈ {8; 9; 10; 11; 12; 13}" \ 
	"N ∈ {9; 10; 11; 12}" \ 
	"N ∈ {9; 10; 11; 12; 13}"  
    do  
        grep "$line" log$i -A4 -B0 | grep -v "N " 
        echo -- 
    done &gt; pb$i 
done 
</pre> 
<p>The results are well distributed among the four quarters of the search space that I initially chose arbitrarily. That's good news  as it means things can be kept parallel by keeping these files separate. One file looks like:</p> 
<pre>        An ∈ {-26} 
        Bn ∈ {-15} 
        in ∈ {-26} 
        jn ∈ {18} 
-- 
        An ∈ {-26} 
        Bn ∈ {-15} 
        in ∈ {-26} 
        jn ∈ {19} 
-- 
        An ∈ {-26} 
        Bn ∈ {-15} 
        in ∈ {-3} 
        jn ∈ {6} 
-- 
... 
</pre> 
<h2>How to re-analyze the problematic subcubes more precisely</h2> 
<p>Each file pb1  ...  pb4 can be processed a little bit further to look like C code:</p> 
<pre>for i in 1 2 3 4 
do 
  sed -e s"/--/f();/" -e s"/∈ {/= /" -e s"/}/;/" &lt; pb$i &gt; pr$i.c 
done 
</pre> 
<p>The above commands transform the interesting values files into:</p> 
<pre>        An = -26; 
        Bn = -15; 
        in = -26; 
        jn = 18; 
f(); 
        An = -26; 
        Bn = -15; 
        in = -26; 
        jn = 19; 
f(); 
        An = -26; 
        Bn = -15; 
        in = -3; 
        jn = 6; 
f(); 
... 
</pre> 
<p>Each of the four pieces of program weights in at a bit less than 7 MB of C code. I plan to make good use of this information tidbit the next time someone asks me <a href="/index.php?post/2011/07/16/Formal-verification-and-SLOC">what project sizes Frama-C's value analysis can handle</a>.</p> 
<pre>$ ls -l pr?.c 
-rw-r--r-- 1 cuoq cuoq 6788869 2011-09-17 18:52 pr1.c 
-rw-r--r-- 1 cuoq cuoq 6551620 2011-09-17 18:52 pr2.c 
-rw-r--r-- 1 cuoq cuoq 6655238 2011-09-17 18:52 pr3.c 
-rw-r--r-- 1 cuoq cuoq 6486765 2011-09-17 18:52 pr4.c 
</pre> 
<p>The files pr1.c  ...  pr4.c are not complete C programs  but they work well with the following prolog (<a href="/assets/img/blog/imported-posts/prolog.c">download</a>):</p> 
<pre>... 
int An  Bn  in  jn; 
void f(void) 
{ 
  int Ans  Bns  ins  jns; 
  float A  B  i  j; 
  for (Ans=4*An; Ans&lt;4*(An+1); Ans++) 
    { 
      A = Frama_C_float_interval(Ans / 32.  (Ans + 1) / 32.); 
      for (Bns=4*Bn; Bns&lt;4*(Bn+1); Bns++) 
        { 
          B = Frama_C_float_interval(Bns / 32.  (Bns + 1) / 32.); 
          for (ins=4*in; ins&lt;4*(in+1); ins++) 
            { 
              i = Frama_C_float_interval(ins / 32.  (ins + 1) / 32.); 
              for (jns=4*jn; jns&lt;4*(jn+1); jns++) 
                { 
                  j = Frama_C_float_interval(jns / 32.  (jns + 1) / 32.); 
                  compute(A  B  i  j); 
                } 
            } 
        } 
    } 
} 
main(){ 
</pre> 
<p>A closing bracket <code>}</code> is also needed to make the whole thing a syntactically correct C program.</p> 
<p>Alas  a regrettable performance bug in Frama-C's front end prevents from analyzing such huge generated C functions. We are a bit too close to the Nitrogen release to change data structures for representing the AST  so this bug will probably remain for at least one release cycle. To circumvent the issue  I simply split the files into 182 reasonably-sized chunks (reasonably-sized here meaning 10000 lines  a more usual size for a function).</p> 
<pre>split -l 10000 pr1.c pr1.c. 
</pre> 
<p>182 C files to analyze and 4 cores to analyze them with: this is an undreamed-of opportunity to make use of the <code>xargs -n 1 -P 4</code> command.</p> 
<pre>ls pr?.c.* | xargs -n 1 -P 4 ./do.sh 
</pre> 
<p>Here is the script <code>do.sh</code> for handling one program. It first catenates the prolog  
the chunk  and a closing bracket  and then it launches the value analysis on the 
resulting C program:</p> 
<pre>#!/bin/sh 
( cat prolog.c ; cat $1 ; echo "}" ) &gt; t_$1.c 
frama-c -val share/builtin.c t_$1.c -obviously-terminates \ 
  -no-val-show-progress -all-rounding-modes &gt; log_pass2_$1 2&gt;&amp;1 
</pre> 
<h2>Results</h2> 
<p>The above  yada yada yada  produces one log file for each of the 182 chunks:</p> 
<pre>$ ls -l log_pass2_pr* 
-rw-r--r-- 1 cuoq cuoq 500913957 2011-09-17 20:50 log_pass2_pr1.c.aa 
-rw-r--r-- 1 cuoq cuoq 502329593 2011-09-17 20:49 log_pass2_pr1.c.ab 
-rw-r--r-- 1 cuoq cuoq 503146982 2011-09-17 20:51 log_pass2_pr1.c.ac 
... 
-rw-r--r-- 1 cuoq cuoq 502560543 2011-09-18 01:22 log_pass2_pr1.c.ay 
-rw-r--r-- 1 cuoq cuoq 502283181 2011-09-18 01:23 log_pass2_pr1.c.az 
-rw-r--r-- 1 cuoq cuoq 503974409 2011-09-18 01:30 log_pass2_pr1.c.ba 
-rw-r--r-- 1 cuoq cuoq 501308298 2011-09-18 01:29 log_pass2_pr1.c.bb 
... 
-rw-r--r-- 1 cuoq cuoq 502932885 2011-09-18 05:20 log_pass2_pr1.c.bs 
-rw-r--r-- 1 cuoq cuoq 422006804 2011-09-18 05:03 log_pass2_pr1.c.bt 
-rw-r--r-- 1 cuoq cuoq 502353901 2011-09-18 05:19 log_pass2_pr2.c.aa 
-rw-r--r-- 1 cuoq cuoq 502485241 2011-09-18 05:23 log_pass2_pr2.c.ab 
-rw-r--r-- 1 cuoq cuoq 503562848 2011-09-18 05:57 log_pass2_pr2.c.ac 
... 
-rw-r--r-- 1 cuoq cuoq 184986900 2011-09-18 12:28 log_pass2_pr2.c.bs 
-rw-r--r-- 1 cuoq cuoq 498627515 2011-09-18 13:11 log_pass2_pr3.c.aa 
... 
-rw-r--r-- 1 cuoq cuoq 263096852 2011-09-19 05:27 log_pass2_pr4.c.bs 
</pre> 
<p>Incidentally  it appears from the above listing that the second 
pass took about 36 hours (two nights and one day). 
The inside of one log file looks like:</p> 
<pre>[value] DUMPING STATE of file t_pr1.c.aa.c line 24 
... 
        N ∈ {10; 11} 
        An ∈ {-26} 
        Bn ∈ {-15} 
        in ∈ {-26} 
        jn ∈ {18} 
        Ans ∈ {-104} 
        Bns ∈ {-60} 
        ins ∈ {-104} 
        jns ∈ {72} 
        A ∈ [-3.25 .. -3.21875] 
        B ∈ [-1.875 .. -1.84375] 
        i ∈ [-3.25 .. -3.21875] 
        j ∈ [2.25 .. 2.28125] 
        =END OF DUMP== 
t_pr1.c.aa.c:15:[value] Function compute: postcondition got status valid. 
[value] DUMPING STATE of file t_pr1.c.aa.c line 24 
... 
        N ∈ {10; 11} 
        An ∈ {-26} 
        Bn ∈ {-15} 
        in ∈ {-26} 
        jn ∈ {18} 
        Ans ∈ {-104} 
        Bns ∈ {-60} 
        ins ∈ {-104} 
        jns ∈ {73} 
        A ∈ [-3.25 .. -3.21875] 
        B ∈ [-1.875 .. -1.84375] 
        i ∈ [-3.25 .. -3.21875] 
        j ∈ [2.28125 .. 2.3125] 
        =END OF DUMP== 
... 
</pre> 
<p>Each value set for variable <code>N</code> is computed more precisely than in the first pass  because the values for floating-point variables <code>A  B  i  j</code> are known more precisely. Above  <code>N</code> is determined to be either 10 or 11 (both safe values) for two of the subsubcubes under examination. Below is the complete list of sets of values computed for <code>N</code>:</p> 
<pre>$ for i in log_pass2_pr* ; do grep "N " $i | sort -u ; done | sort -u 
        N ∈ {10} 
        N ∈ {10; 11} 
        N ∈ {11} 
        N ∈ {7; 8; 9} 
        N ∈ {8; 9} 
        N ∈ {8; 9; 10} 
        N ∈ {9} 
        N ∈ {9; 10} 
        N ∈ {9; 10; 11} 
</pre> 
<h2>Conclusion</h2> 
<p>I have already provided the "the function being analyzed is safe after all" conclusion in the previous post. This post is only for showing the "how"  so that you can judge for yourself  for instance  how much cheating there was. There was quite a bit of C code written for the purpose of the verification: this code could itself have bugs. And there was a good amount of logs processing with shell scripts. There could be bugs there too. Stéphane Duprat would however point out that if we had done the verification with tests  there would have been <a href="http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2011-February/002461.html">testing code and logs-processing-scripts too</a>. The difference between the two approaches is that we used <code>Frama_C_float_interval()</code> in the places where we might have used a random number generator. It does not feel like a large conceptual leap  and we obtained deeper properties in exchange (would you trust the function not to return <code>12</code> if  like me  you didn't understand what it computes at all and had only tested it a million times? A billion times? How many tests would be enough for you to <a href="http://blog.regehr.org/archives/364">sit under a piano</a>?)</p> 
<p>The possibility that variable <code>N</code> in function <code>compute()</code> held a number larger than 11 was related to the <a href="/index.php?post/2011/08/07/.%2C-%7E%3A%3B%21%2A%24%40%5BN0N%3A0%5D">last and most difficult of a series of alarms</a> that we found in a <a href="/donut/value/2011/07/22/Animated-donut-verification">mostly unmodified piece of obfuscated C code</a>. Some of the <a href="/index.php?post/2011/08/01/Animated-donut">other alarms</a> disappeared simply by playing with the <code>-slevel</code> setting  which is the setting to think of immediately when the analysis is fast enough and some alarms remain. I explained where the other alarms came from (a call to <code>memset()</code> was not handled precisely enough  etc.) but in actual use  you don't need to: just increase the argument to <code>-slevel</code> and see if the alarms go away  even before starting to think.</p> 
<p>The method I have shown here is a little bit laborious  but one reason for us Frama-C developers to do these case studies is to find out about possible uses and make them more comfortable in future releases. This series of posts shows how to do this kind of verification now (well... it describes how to do them soon; the method shown will work with the Nitrogen release). This is absolutely not definitive. A plug-in could automate a lot of what we have done by hand here.</p> 
<p>This post was improved by insights from Florent Kirchner.</p>
 <p>This post documents the steps I followed in order to finish verifying function <code>compute()</code>, picking up from <a href="/donut/facetious-colleagues/floating-point/value/value-builtins/2011/09/17/Probably-safe-donut">there</a>.</p> 
<h2>Previously on this blog</h2> 
<p>In last episode  we had found that some sub-cubes in the search space appeared to lead to dangerous value sets for variable <code>N</code>. These sets were:</p> 
<pre>        N ∈ {10; 11; 12} 
        N ∈ {6; 7; 8; 9; 10; 11; 12} 
        N ∈ {7; 8; 9; 10; 11; 12} 
        N ∈ {7; 8; 9; 10; 11; 12; 13} 
        N ∈ {8; 9; 10; 11; 12} 
        N ∈ {8; 9; 10; 11; 12; 13} 
        N ∈ {9; 10; 11; 12} 
        N ∈ {9; 10; 11; 12; 13} 
</pre> 
<p>There are only eight dangerous value sets for <code>N</code>  but these correspond to many values of input variables <code>An  Bn  in  jn</code> in the <a href="/assets/img/blog/imported-posts/an.c">analysis context</a> we wrote for the occasion. 
Grepping for each of these eight lines in the original logs allows to get the corresponding values of <code>An  Bn  in  jn</code>. These are the values for which we haven't concluded yet that <code>compute()</code> is safe:</p> 
<pre>for i in 1 2 3 4 
do 
    for line in \ 
	"N ∈ {10; 11; 12}" \ 
	"N ∈ {6; 7; 8; 9; 10; 11; 12}" \ 
	"N ∈ {7; 8; 9; 10; 11; 12}" \ 
	"N ∈ {7; 8; 9; 10; 11; 12; 13}" \ 
	"N ∈ {8; 9; 10; 11; 12}" \ 
	"N ∈ {8; 9; 10; 11; 12; 13}" \ 
	"N ∈ {9; 10; 11; 12}" \ 
	"N ∈ {9; 10; 11; 12; 13}"  
    do  
        grep "$line" log$i -A4 -B0 | grep -v "N " 
        echo -- 
    done &gt; pb$i 
done 
</pre> 
<p>The results are well distributed among the four quarters of the search space that I initially chose arbitrarily. That's good news  as it means things can be kept parallel by keeping these files separate. One file looks like:</p> 
<pre>        An ∈ {-26} 
        Bn ∈ {-15} 
        in ∈ {-26} 
        jn ∈ {18} 
-- 
        An ∈ {-26} 
        Bn ∈ {-15} 
        in ∈ {-26} 
        jn ∈ {19} 
-- 
        An ∈ {-26} 
        Bn ∈ {-15} 
        in ∈ {-3} 
        jn ∈ {6} 
-- 
... 
</pre> 
<h2>How to re-analyze the problematic subcubes more precisely</h2> 
<p>Each file pb1  ...  pb4 can be processed a little bit further to look like C code:</p> 
<pre>for i in 1 2 3 4 
do 
  sed -e s"/--/f();/" -e s"/∈ {/= /" -e s"/}/;/" &lt; pb$i &gt; pr$i.c 
done 
</pre> 
<p>The above commands transform the interesting values files into:</p> 
<pre>        An = -26; 
        Bn = -15; 
        in = -26; 
        jn = 18; 
f(); 
        An = -26; 
        Bn = -15; 
        in = -26; 
        jn = 19; 
f(); 
        An = -26; 
        Bn = -15; 
        in = -3; 
        jn = 6; 
f(); 
... 
</pre> 
<p>Each of the four pieces of program weights in at a bit less than 7 MB of C code. I plan to make good use of this information tidbit the next time someone asks me <a href="/index.php?post/2011/07/16/Formal-verification-and-SLOC">what project sizes Frama-C's value analysis can handle</a>.</p> 
<pre>$ ls -l pr?.c 
-rw-r--r-- 1 cuoq cuoq 6788869 2011-09-17 18:52 pr1.c 
-rw-r--r-- 1 cuoq cuoq 6551620 2011-09-17 18:52 pr2.c 
-rw-r--r-- 1 cuoq cuoq 6655238 2011-09-17 18:52 pr3.c 
-rw-r--r-- 1 cuoq cuoq 6486765 2011-09-17 18:52 pr4.c 
</pre> 
<p>The files pr1.c  ...  pr4.c are not complete C programs  but they work well with the following prolog (<a href="/assets/img/blog/imported-posts/prolog.c">download</a>):</p> 
<pre>... 
int An  Bn  in  jn; 
void f(void) 
{ 
  int Ans  Bns  ins  jns; 
  float A  B  i  j; 
  for (Ans=4*An; Ans&lt;4*(An+1); Ans++) 
    { 
      A = Frama_C_float_interval(Ans / 32.  (Ans + 1) / 32.); 
      for (Bns=4*Bn; Bns&lt;4*(Bn+1); Bns++) 
        { 
          B = Frama_C_float_interval(Bns / 32.  (Bns + 1) / 32.); 
          for (ins=4*in; ins&lt;4*(in+1); ins++) 
            { 
              i = Frama_C_float_interval(ins / 32.  (ins + 1) / 32.); 
              for (jns=4*jn; jns&lt;4*(jn+1); jns++) 
                { 
                  j = Frama_C_float_interval(jns / 32.  (jns + 1) / 32.); 
                  compute(A  B  i  j); 
                } 
            } 
        } 
    } 
} 
main(){ 
</pre> 
<p>A closing bracket <code>}</code> is also needed to make the whole thing a syntactically correct C program.</p> 
<p>Alas  a regrettable performance bug in Frama-C's front end prevents from analyzing such huge generated C functions. We are a bit too close to the Nitrogen release to change data structures for representing the AST  so this bug will probably remain for at least one release cycle. To circumvent the issue  I simply split the files into 182 reasonably-sized chunks (reasonably-sized here meaning 10000 lines  a more usual size for a function).</p> 
<pre>split -l 10000 pr1.c pr1.c. 
</pre> 
<p>182 C files to analyze and 4 cores to analyze them with: this is an undreamed-of opportunity to make use of the <code>xargs -n 1 -P 4</code> command.</p> 
<pre>ls pr?.c.* | xargs -n 1 -P 4 ./do.sh 
</pre> 
<p>Here is the script <code>do.sh</code> for handling one program. It first catenates the prolog  
the chunk  and a closing bracket  and then it launches the value analysis on the 
resulting C program:</p> 
<pre>#!/bin/sh 
( cat prolog.c ; cat $1 ; echo "}" ) &gt; t_$1.c 
frama-c -val share/builtin.c t_$1.c -obviously-terminates \ 
  -no-val-show-progress -all-rounding-modes &gt; log_pass2_$1 2&gt;&amp;1 
</pre> 
<h2>Results</h2> 
<p>The above  yada yada yada  produces one log file for each of the 182 chunks:</p> 
<pre>$ ls -l log_pass2_pr* 
-rw-r--r-- 1 cuoq cuoq 500913957 2011-09-17 20:50 log_pass2_pr1.c.aa 
-rw-r--r-- 1 cuoq cuoq 502329593 2011-09-17 20:49 log_pass2_pr1.c.ab 
-rw-r--r-- 1 cuoq cuoq 503146982 2011-09-17 20:51 log_pass2_pr1.c.ac 
... 
-rw-r--r-- 1 cuoq cuoq 502560543 2011-09-18 01:22 log_pass2_pr1.c.ay 
-rw-r--r-- 1 cuoq cuoq 502283181 2011-09-18 01:23 log_pass2_pr1.c.az 
-rw-r--r-- 1 cuoq cuoq 503974409 2011-09-18 01:30 log_pass2_pr1.c.ba 
-rw-r--r-- 1 cuoq cuoq 501308298 2011-09-18 01:29 log_pass2_pr1.c.bb 
... 
-rw-r--r-- 1 cuoq cuoq 502932885 2011-09-18 05:20 log_pass2_pr1.c.bs 
-rw-r--r-- 1 cuoq cuoq 422006804 2011-09-18 05:03 log_pass2_pr1.c.bt 
-rw-r--r-- 1 cuoq cuoq 502353901 2011-09-18 05:19 log_pass2_pr2.c.aa 
-rw-r--r-- 1 cuoq cuoq 502485241 2011-09-18 05:23 log_pass2_pr2.c.ab 
-rw-r--r-- 1 cuoq cuoq 503562848 2011-09-18 05:57 log_pass2_pr2.c.ac 
... 
-rw-r--r-- 1 cuoq cuoq 184986900 2011-09-18 12:28 log_pass2_pr2.c.bs 
-rw-r--r-- 1 cuoq cuoq 498627515 2011-09-18 13:11 log_pass2_pr3.c.aa 
... 
-rw-r--r-- 1 cuoq cuoq 263096852 2011-09-19 05:27 log_pass2_pr4.c.bs 
</pre> 
<p>Incidentally  it appears from the above listing that the second 
pass took about 36 hours (two nights and one day). 
The inside of one log file looks like:</p> 
<pre>[value] DUMPING STATE of file t_pr1.c.aa.c line 24 
... 
        N ∈ {10; 11} 
        An ∈ {-26} 
        Bn ∈ {-15} 
        in ∈ {-26} 
        jn ∈ {18} 
        Ans ∈ {-104} 
        Bns ∈ {-60} 
        ins ∈ {-104} 
        jns ∈ {72} 
        A ∈ [-3.25 .. -3.21875] 
        B ∈ [-1.875 .. -1.84375] 
        i ∈ [-3.25 .. -3.21875] 
        j ∈ [2.25 .. 2.28125] 
        =END OF DUMP== 
t_pr1.c.aa.c:15:[value] Function compute: postcondition got status valid. 
[value] DUMPING STATE of file t_pr1.c.aa.c line 24 
... 
        N ∈ {10; 11} 
        An ∈ {-26} 
        Bn ∈ {-15} 
        in ∈ {-26} 
        jn ∈ {18} 
        Ans ∈ {-104} 
        Bns ∈ {-60} 
        ins ∈ {-104} 
        jns ∈ {73} 
        A ∈ [-3.25 .. -3.21875] 
        B ∈ [-1.875 .. -1.84375] 
        i ∈ [-3.25 .. -3.21875] 
        j ∈ [2.28125 .. 2.3125] 
        =END OF DUMP== 
... 
</pre> 
<p>Each value set for variable <code>N</code> is computed more precisely than in the first pass  because the values for floating-point variables <code>A  B  i  j</code> are known more precisely. Above  <code>N</code> is determined to be either 10 or 11 (both safe values) for two of the subsubcubes under examination. Below is the complete list of sets of values computed for <code>N</code>:</p> 
<pre>$ for i in log_pass2_pr* ; do grep "N " $i | sort -u ; done | sort -u 
        N ∈ {10} 
        N ∈ {10; 11} 
        N ∈ {11} 
        N ∈ {7; 8; 9} 
        N ∈ {8; 9} 
        N ∈ {8; 9; 10} 
        N ∈ {9} 
        N ∈ {9; 10} 
        N ∈ {9; 10; 11} 
</pre> 
<h2>Conclusion</h2> 
<p>I have already provided the "the function being analyzed is safe after all" conclusion in the previous post. This post is only for showing the "how"  so that you can judge for yourself  for instance  how much cheating there was. There was quite a bit of C code written for the purpose of the verification: this code could itself have bugs. And there was a good amount of logs processing with shell scripts. There could be bugs there too. Stéphane Duprat would however point out that if we had done the verification with tests  there would have been <a href="http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2011-February/002461.html">testing code and logs-processing-scripts too</a>. The difference between the two approaches is that we used <code>Frama_C_float_interval()</code> in the places where we might have used a random number generator. It does not feel like a large conceptual leap  and we obtained deeper properties in exchange (would you trust the function not to return <code>12</code> if  like me  you didn't understand what it computes at all and had only tested it a million times? A billion times? How many tests would be enough for you to <a href="http://blog.regehr.org/archives/364">sit under a piano</a>?)</p> 
<p>The possibility that variable <code>N</code> in function <code>compute()</code> held a number larger than 11 was related to the <a href="/index.php?post/2011/08/07/.%2C-%7E%3A%3B%21%2A%24%40%5BN0N%3A0%5D">last and most difficult of a series of alarms</a> that we found in a <a href="/donut/value/2011/07/22/Animated-donut-verification">mostly unmodified piece of obfuscated C code</a>. Some of the <a href="/index.php?post/2011/08/01/Animated-donut">other alarms</a> disappeared simply by playing with the <code>-slevel</code> setting  which is the setting to think of immediately when the analysis is fast enough and some alarms remain. I explained where the other alarms came from (a call to <code>memset()</code> was not handled precisely enough  etc.) but in actual use  you don't need to: just increase the argument to <code>-slevel</code> and see if the alarms go away  even before starting to think.</p> 
<p>The method I have shown here is a little bit laborious  but one reason for us Frama-C developers to do these case studies is to find out about possible uses and make them more comfortable in future releases. This series of posts shows how to do this kind of verification now (well... it describes how to do them soon; the method shown will work with the Nitrogen release). This is absolutely not definitive. A plug-in could automate a lot of what we have done by hand here.</p> 
<p>This post was improved by insights from Florent Kirchner.</p>
{% endraw %}