This repository has been archived by the owner on Oct 3, 2021. It is now read-only.
/
byte_add_1_true-unreach-call_true-no-overflow_true-termination.i
116 lines (101 loc) · 3.53 KB
/
byte_add_1_true-unreach-call_true-no-overflow_true-termination.i
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
extern void __VERIFIER_error() __attribute__ ((__noreturn__));
extern unsigned int __VERIFIER_nondet_uint(void);
void __VERIFIER_assert(int cond) {
if (!(cond)) {
ERROR: __VERIFIER_error();
}
return;
}
extern void __assert_fail (__const char *__assertion, __const char *__file,
unsigned int __line, __const char *__function)
__attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
extern void __assert_perror_fail (int __errnum, __const char *__file,
unsigned int __line,
__const char *__function)
__attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
extern void __assert (const char *__assertion, const char *__file, int __line)
__attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
unsigned int mp_add(unsigned int a, unsigned int b)
{
unsigned char a0, a1, a2, a3;
unsigned char b0, b1, b2, b3;
unsigned char r0, r1, r2, r3;
unsigned short carry;
unsigned short partial_sum;
unsigned int r;
unsigned char i;
unsigned char na, nb;
a0 = a;
a1 = a >> 8;
a2 = a >> 16U;
a3 = a >> 24U;
b0 = b;
b1 = b >> 8U;
b2 = b >> 16U;
b3 = b >> 24U;
na = (unsigned char)4;
if (a3 == (unsigned char)0) {
na = na - 1;
if (a2 == (unsigned char)0) {
na = na - 1;
if (a1 == (unsigned char)0) {
na = na - 1;
}
}
}
nb = (unsigned char)4;
if (b3 == (unsigned char)0) {
nb = nb - 1;
if (b2 == (unsigned char)0) {
nb = nb - 1;
if (b1 == (unsigned char)0) {
nb = nb - 1;
}
}
}
carry = (unsigned short)0;
i = (unsigned char)0;
while ((i < na) || (i < nb) || (carry != (unsigned short)0)) {
partial_sum = carry;
carry = (unsigned short)0;
if (i < na) {
if (i == (unsigned char)0) { partial_sum = partial_sum + a0; }
if (i == (unsigned char)1) { partial_sum = partial_sum + a1; }
if (i == (unsigned char)2) { partial_sum = partial_sum + a2; }
if (i == (unsigned char)3) { partial_sum = partial_sum + a3; }
}
if (i < nb) {
if (i == (unsigned char)0) { partial_sum = partial_sum + b0; }
if (i == (unsigned char)1) { partial_sum = partial_sum + b1; }
if (i == (unsigned char)2) { partial_sum = partial_sum + b2; }
if (i == (unsigned char)3) { partial_sum = partial_sum + b3; }
}
if (partial_sum > ((unsigned char)255)) {
partial_sum = partial_sum & ((unsigned char)255);
carry = (unsigned short)1;
}
if (i == (unsigned char)0) { r0 = (unsigned char)partial_sum; }
if (i == (unsigned char)1) { r1 = (unsigned char)partial_sum; }
if (i == (unsigned char)2) { r2 = (unsigned char)partial_sum; }
if (i == (unsigned char)3) { r3 = (unsigned char)partial_sum; }
i = i + (unsigned char)1;
}
while (i < (unsigned char)4) {
if (i == (unsigned char)0) { r0 = (unsigned char)0; }
if (i == (unsigned char)1) { r1 = (unsigned char)0; }
if (i == (unsigned char)2) { r2 = (unsigned char)0; }
if (i == (unsigned char)3) { r3 = (unsigned char)0; }
i = i + (unsigned char)1;
}
r = r0 | (r1 << 8U) | (r2 << 16U) | ((unsigned int)r3 << 24U);
return r;
}
int main()
{
unsigned int a, b, r;
b = __VERIFIER_nondet_uint();
a = 234770789;
r = mp_add(a, b);
__VERIFIER_assert(r == a + b);
return 0;
}