1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
|
int A, B, C;
int u, v, w;
/*@ requires u == argf && v == 0;
assigns u, v, w \from u;
ensures u != \result;
*/
int main(int argf, int en1, int en2, int en3, int en4, unsigned int uc, int m, int n)
{
int x,y,z,t;
x = 1;
/*@ assert x == 1+u; */
Frama_C_show_each_diff(x - u);
/*@ requires y != 2;
@ ensures y == 2;
*/
y = 2;
/*@ assert y == 2; */
z = 3;
A = en1 ? 0 : 1;
B = en2 ? 0 : 2;
if (en3)
{
//@ assert A == 0 <==> A != 0 ;
Frama_C_show_each_then_A_B(A,B);
}
else if (en4)
{
//@ assert ! (A == 0 <==> B == A) ;
Frama_C_show_each_elseif_A_B(A,B);
}
else
{
//@ assert A == 0 <==> B == A ;
Frama_C_show_each_else_A_B(A,B);
}
//@ assert 0 <= m <= n <= 9;
Frama_C_show_each_mn(m, n);
int a = 0, b = 1;
/*@ assert (a || b) == b; */
/*@ assert (a && a) == a; */
int tt[3];
tt[0] = 1;
//@ assert (uc > 0 || tt[uc] == 1) == \true;
/*@ assert y == z; */
return z;
}
|
