1extern int nondet_int(void);
2void __VERIFIER_assert(int cond) {
3 if (!(cond)) {
4 ERROR: goto ERROR;
5 }
6 return;
7}
8
9extern void __assert_fail (__const char *__assertion, __const char *__file,
10 unsigned int __line, __const char *__function)
11 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
12extern void __assert_perror_fail (int __errnum, __const char *__file,
13 unsigned int __line,
14 __const char *__function)
15 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
16extern void __assert (const char *__assertion, const char *__file, int __line)
17 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
18
19unsigned int mp_add(unsigned int a, unsigned int b)
20{
21 unsigned char a0, a1, a2, a3;
22 unsigned char b0, b1, b2, b3;
23 unsigned char r0, r1, r2, r3;
24 unsigned short carry;
25 unsigned short partial_sum;
26 unsigned int r;
27 unsigned char i;
28 unsigned char na, nb;
29 a0 = a;
30 a1 = a >> 8;
31 a2 = a >> 16U;
32 a3 = a >> 24U;
33 b0 = b;
34 b1 = b >> 8U;
35 b2 = b >> 16U;
36 b3 = b >> 24U;
37 na = (unsigned char)4;
38 if (a3 == (unsigned char)0) {
39 na = na - 1;
40 if (a2 == (unsigned char)0) {
41 na = na - 1;
42 if (a1 == (unsigned char)0) {
43 na = na - 1;
44 }
45 }
46 }
47 nb = (unsigned char)4;
48 if (b3 == (unsigned char)0) {
49 nb = nb - 1;
50 if (b2 == (unsigned char)0) {
51 nb = nb - 1;
52 if (b1 == (unsigned char)0) {
53 nb = nb - 1;
54 }
55 }
56 }
57 carry = (unsigned short)0;
58 i = (unsigned char)0;
59 while ((i < na) || (i < nb) || (carry != (unsigned short)0)) {
60 partial_sum = carry;
61 carry = (unsigned short)0;
62 if (i < na) {
63 if (i == (unsigned char)0) { partial_sum = partial_sum + a0; }
64 if (i == (unsigned char)1) { partial_sum = partial_sum + a1; }
65 if (i == (unsigned char)2) { partial_sum = partial_sum + a2; }
66 if (i == (unsigned char)3) { partial_sum = partial_sum + a3; }
67 }
68 if (i < nb) {
69 if (i == (unsigned char)0) { partial_sum = partial_sum + b0; }
70 if (i == (unsigned char)1) { partial_sum = partial_sum + b1; }
71 if (i == (unsigned char)2) { partial_sum = partial_sum + b2; }
72 if (i == (unsigned char)3) { partial_sum = partial_sum + b3; }
73 }
74 if (partial_sum > ((unsigned char)255)) {
75 partial_sum = partial_sum & ((unsigned char)255);
76 carry = (unsigned short)1;
77 }
78 if (i == (unsigned char)0) { r0 = (unsigned char)partial_sum; }
79 if (i == (unsigned char)1) { r1 = (unsigned char)partial_sum; }
80 if (i == (unsigned char)2) { r2 = (unsigned char)partial_sum; }
81 if (i == (unsigned char)3) { r3 = (unsigned char)partial_sum; }
82
83 i = i + (unsigned char)1;
84 }
85
86 while (i < (unsigned char)4) {
87 if (i == (unsigned char)0) { r0 = (unsigned char)0; }
88 if (i == (unsigned char)1) { r1 = (unsigned char)0; }
89 if (i == (unsigned char)2) { r2 = (unsigned char)0; }
90 if (i == (unsigned char)3) { r3 = (unsigned char)0; }
91
92 i = i + (unsigned char)1;
93 }
94
95 r = r0 | (r1 << 8U) | (r2 << 16U) | (r3 << 24U);
96
97 return r;
98}
99
100
101int main()
102{
103 unsigned int a, b, r;
104
105 a = 234770789;
106
107 r = mp_add(a, b);
108
109 __VERIFIER_assert(r == a + b);
110
111 return 0;
112}