Here's a cool obfuscated C program by Andy Sloane that draws a revolving donut.

You know where this is heading... I am going to suggest that someone should verify it. I will get us started.

1. Download the code

2. Determine what library functions it needs:

```\$ frama-c -metrics donut.c
[kernel] preprocessing with "gcc -C -E -I.  donut.c"
donut.c:1:[kernel] user error: syntax error
```

Oops. The donut is a little bit too obfuscated for our front-end, it seems. The problem here is the idiom `k;` to declare an `int` variable `k`. Let's change this:

```int          k;double sin()
,cos();main(){float A=
0,B=0,i,j,z[1760];char b[
1760];printf("\x1b[2J");for(;;
){memset(b,32,1760);memset(z,0,7040)
;for(j=0;6.28>j;j+=0.07)for(i=0;6.28
>i;i+=0.02){float c=sin(i),d=cos(j),e=
sin(A),f=sin(j),g=cos(A),h=d+2,D=1/(c*
h*e+f*g+5),l=cos      (i),m=cos(B),n=s\
in(B),t=c*h*g-f*        e;int x=40+30*D*
(l*h*m-t*n),y=            12+15*D*(l*h*n
+t*m),o=x+80*y,          N=8*((f*e-c*d*g
)*m-c*d*e-f*g-l        *d*n);if(22>y&&
y>0&&x>0&&80>x&&D>z[o]){z[o]=D;;;b[o]=
".,-~:;=!*#\$@"[N>0?N:0];}}/*#****!!-*/
printf("\x1b[H");for(k=0;1761>k;k++)
putchar(k%80?b[k]:10);A+=0.04;B+=
0.02;}}/*****####*******!!=;:~
~::==!!!**********!!!==::-
.,~~;;;========;;;:~-.
..,--------,*/
```
```\$ frama-c -metrics donut.c
[kernel] preprocessing with "gcc -C -E -I.  donut.c"
[metrics] Syntactic metrics
Defined function (1):
main  (0 call);
Undefined functions (5):
putchar  (1 call); sin  (4 calls); cos  (4 calls); printf  (2 calls);
memset  (2 calls);
```

Functions `putchar()` and `printf()` do not influence the rest of the execution, so we can postpone finding a good modelization for them until the very end. We have a `memset()` implementation leftover from the Skein tutorial. Math functions `cos()` and `sin()` can in a first step be specified as returning `[-1.0 .. 1.0]`. The value analysis has for a long time had a `Frama_C_cos()` built-in that does a little better than that, and the next release will have a `Frama_C_sin()`, but these are not necessary yet.

Let's use a file sincos.c such as:

```#include "share/builtin.h"

double sin(double x)
{
return Frama_C_double_interval(-1.0, 1.0);
}

double cos(double x)
{
return Frama_C_double_interval(-1.0, 1.0);
}
```

3. Launch an imprecise analysis:

```\$ bin/toplevel.opt -val share/builtin.c sincos.c donut.c share/libc.c | grep assert
```

We use the command above and get the results below. There are 9 alarms and 2 of them are redundant with the other 7 (these two would be removed in the GUI).

```share/libc.c:51:[kernel] warning: out of bounds write. assert \valid(tmp);
donut.c:14:[kernel] warning: accessing out of bounds index [-7610..9610]. assert 0 ≤ o ∧ o < 1760;
donut.c:14:[kernel] warning: accessing uninitialized left-value: assert \initialized(z[o]);
donut.c:14:[kernel] warning: accessing out of bounds index [-7610..9610]. assert 0 ≤ o ∧ o < 1760;
donut.c:15:[kernel] warning: out of bounds read. assert \valid(".,-~:;=!*#\$@"+tmp_7);
donut.c:15:[kernel] warning: accessing out of bounds index [-7610..9610]. assert 0 ≤ o ∧ o < 1760;
donut.c:17:[kernel] warning: accessing uninitialized left-value: assert \initialized(b[k]);
donut.c:17:[kernel] warning: accessing out of bounds index [0..1760]. assert 0 ≤ k ∧ k < 1760;
donut.c:14:[value] warning: overflow in float: [--..--] -> [-3.40282346639e+38 .. 3.40282346639e+38]. assert(Ook)
[scope] [rm_asserts] removing 2 assertion(s)
```

4. The imprecise analysis was fast. Let us launch a more precise analysis:

```\$ bin/toplevel.opt -val share/builtin.c sincos.c donut.c share/libc.c -slevel 200 | grep assert
share/libc.c:51:[kernel] warning: out of bounds write. assert \valid(tmp);
donut.c:14:[kernel] warning: accessing out of bounds index [-7610..9610]. assert 0 ≤ o ∧ o < 1760;
donut.c:14:[kernel] warning: accessing uninitialized left-value: assert \initialized(z[o]);
donut.c:14:[kernel] warning: accessing out of bounds index [-7610..9610]. assert 0 ≤ o ∧ o < 1760;
donut.c:15:[kernel] warning: accessing out of bounds index [-7610..9610]. assert 0 ≤ o ∧ o < 1760;
donut.c:15:[kernel] warning: out of bounds read. assert \valid(".,-~:;=!*#\$@"+tmp_7);
donut.c:17:[kernel] warning: accessing uninitialized left-value: assert \initialized(b[k]);
donut.c:17:[kernel] warning: accessing out of bounds index [200..1760]. assert 0 ≤ k ∧ k < 1760;
donut.c:14:[value] warning: overflow in float: [--..--] -> [-3.40282346639e+38 .. 3.40282346639e+38]. assert(Ook)
[scope] [rm_asserts] removing 2 assertion(s)
```

It's still the same assertions. The development version of Frama-C shows the range of the index `k` (that is, `[200..1760]`) when it prints the assertion `assert 0 ≤ k ∧ k < 1760;`. That suggests that pushing the value of `-slevel` to more than `1760` may eliminate this alarm.

I will let someone else continue from here if they want. This program could be very rewarding to verify (a little birdie tells me that there is at least one true alarm to be found, using the value analysis or any other techniquesI have completely lost faith in that little birdie. There may or may not be a bug, we will know for sure when we are done, but don't stay awake all night looking for one), so I recommended as a fun exercise for those who are bored from sandy holiday beaches.