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
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
|
/* run.config*
STDOPT: #"-slevel-function pgcd1:100,pgcd2:100,pgcd3:100"
*/
int A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R;
volatile v;
void main2 ()
{ int i = v;
A = (4 * i) % 4;
B = (4 * i + 1) % 4;
i = v; //@ assert ((i>=-100) && (i<=100)) ;
E = (3*i + 1) % 12;
i = v; //@ assert ((i>=0) && (i<=100)) ;
C = (4 * i + 1) % 4;
D = (3*i + 1) % 12;
F = (24*i + 5) % 12;
G = (24*i + 5) % 13;
H = i % 1000;
I = (2 * i+1101) % 1000;
J = (5 * i - 201) % 1000;
K = (5 * i - 201) % 10;
L = K % J;
M = K % D;
N = J % I;
O = I % G;
P = A % J;
Q = J % L;
}
extern int a, b;
/*@ requires -10<=x<=10 && -10<=y<=10; */
int pgcd1(int x, int y) {
int a = x, b = y;
/*@ loop invariant -10<=b<0||b==0||0<b<=10;
loop invariant -10<=a<0||a==0||0<a<=10; */
while(b!=0) {
int tmp = a % b;
Frama_C_show_each_1(a,b,tmp);
a = b; b = tmp;
}
return a;
}
/*@ requires -10<=x<=10 && -10<=y<=10; */
int pgcd2(int x, int y) {
int a = x, b = y;
/*@ loop invariant -10<=b<0||b==0||0<b<=10; */
while(b!=0) {
int tmp = a % b;
Frama_C_show_each_2(a,b,tmp);
a = b; b = tmp;
}
return a;
}
/*@ requires -10<=x<=10 && -10<=y<=10; */
int pgcd3(int x, int y) {
int a = x, b = y;
while(b!=0) {
int tmp = a % b;
Frama_C_show_each_3(a,b,tmp);
a = b; b = tmp;
}
return a;
}
void simultaneous_congruences(void)
{
/* Different tests for x congruent to r1 mod m1 and to r2 mod m2. */
/* Test with pgcd(m1,m2) = 1, r2-r1 = 1: a solution. */
extern int i2;
/*@ assert 0<= i2 <= 0x02000000 ; */
int n1 = i2 * 13 + 7;
int n2 = i2 * 15 + 8;
int n3;
if(n1 == n2) { n3 = n1;} else { while(1);}
/* Test with pgcd(m1,m2) != 1, r2-r1 !=1, pgcd(m1,m2) does not
* divide r2 -r1: no solution. */
int m1 = i2 * 4 + 7;
int m2 = i2 * 6 + 10;
if(m1 == m2) { /*@ assert \false; */ }
/* Test with pgcd != 1, r2-r1 !=1, pgcd(m1,m2) divides (r2-r1): a
* solution. */
int o1 = i2* 8 + 3;
int o2 = i2* 12 + 11;
int o3;
if(o1 == o2) { o3 = o1;} else { while(1);}
}
void shift_modulo(void)
{ int i = v;
/*@ assert 0 <= i <= 10; */
int r = (i * 12 + 5) << 2;
int s = ((i * 12 + 5) << 24)>>24;
int q = ((i * 12 + 5) << 25)>>25;
int t = ((i * 13 + 7) << 25)>>25;
}
void extract_bits_modulo(void)
{ int i = v;
/*@ assert 0 <= i <= 10; */
int aa1 = (i * 12 + 5) * 256 + 11;
unsigned char *ptr1 = (unsigned char *)&aa1;
int m1 = ptr1[0]; /* Ideally: congruent to 11 modulo 256; equal to 11. */
int n1 = ptr1[1]; /* Ideally: congruent to 5 modulo 12. */
int aa2 = (i * 12 + 5) * 256 + (i * 11 + 14);
unsigned char *ptr2 = (unsigned char *)&aa2;
int m2 = ptr2[0]; /* Ideally: congruent to 3 modulo 11. */
int n2 = ptr2[1]; /* Ideally: congruent to 5 modulo 12. */
int aa3 = (i * 12 + 5) * 256 + (i * 11 + 16);
unsigned char *ptr3 = (unsigned char *)&aa3;
int m3 = ptr3[0]; /* Ideally: congruent to 5 modulo 11. */
int n3 = ptr3[1]; /* Ideally: congruent to 5 modulo 12. */
int aa4 = (i * 11 + 16);
unsigned char *ptr4 = (unsigned char *)&aa4;
int m4 = ptr4[0]; /* Ideally: congruent to 5 modulo 11. */
int n4 = ptr4[1]; /* Ideally: equal to zero. */
}
//volatile int v;
// Test extraction of modulo with 'positive' semantics (ie. not nearest
// to zero in absolute value, which is the one '%' would have used).
void pos_rem(void) {
int n = v;
//@ assert -1 <= n <= 255;
int j = (int)*(signed char*)&n;
n = v;
//@ assert 0 <= n <= 135;
int k = (int)*(unsigned char*)&n;
n = v;
//@ assert -1 <= n <= 72;
int l = (int)*(signed char*)&n; // Best rem is ([0..72] \cup {255})%255, we approximate by [-128..127]
}
void main() {
if (v) { pgcd1(a, b); }
if (v) { pgcd2(a, b); }
if (v) { pgcd3(a, b); }
main2();
simultaneous_congruences();
shift_modulo();
extract_bits_modulo();
pos_rem();
}
|
