Skip to content
This repository was archived by the owner on Oct 3, 2021. It is now read-only.

Commit 4911f5a

Browse files
lembergerthlembergerth
committed
Add benchmark tasks combined from floats-cdfpl/square and bitvector/soft_float_
Used in 'Dirk Beyer, Marie-Christine Jakobs, Thomas Lemberger: Difference Verification with Conditions, SEFM20'
1 parent b674661 commit 4911f5a

File tree

100 files changed

+16655
-0
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

100 files changed

+16655
-0
lines changed

‎c/combinations/square_1+soft_float_1-2a.c.cil.c‎

Lines changed: 389 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,389 @@
1+
extern unsigned int __VERIFIER_nondet_uint();
2+
extern char __VERIFIER_nondet_char();
3+
extern int __VERIFIER_nondet_int();
4+
extern long __VERIFIER_nondet_long();
5+
extern unsigned long __VERIFIER_nondet_ulong();
6+
extern float __VERIFIER_nondet_float();
7+
extern void exit(int);
8+
extern void abort(void);
9+
10+
extern void __assert_fail (const char *__assertion, const char *__file,
11+
unsigned int __line, const char *__function)
12+
__attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
13+
extern void __assert_perror_fail (int __errnum, const char *__file,
14+
unsigned int __line, const char *__function)
15+
__attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
16+
extern void __assert (const char *__assertion, const char *__file, int __line)
17+
__attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
18+
19+
void reach_error() { ((void) sizeof ((0) ? 1 : 0), __extension__ ({ if (0) ; else __assert_fail ("0", "square_1.c", 7, __extension__ __PRETTY_FUNCTION__); })); }
20+
extern void abort(void);
21+
void assume_abort_if_not(int cond) {
22+
if(!cond) {abort();}
23+
}
24+
extern float __VERIFIER_nondet_float(void);
25+
int main1()
26+
{
27+
float IN = __VERIFIER_nondet_float();
28+
assume_abort_if_not(IN >= 0.0f && IN < 1.0f);
29+
30+
float x = IN;
31+
32+
float result =
33+
1.0f + 0.5f*x - 0.125f*x*x + 0.0625f*x*x*x - 0.0390625f*x*x*x*x;
34+
35+
if(!(result >= 0.0f && result < 1.39f))
36+
{reach_error();}
37+
38+
return 0;
39+
}
40+
41+
void __VERIFIER_assert(int cond) {
42+
if (!(cond)) {
43+
ERROR: {reach_error();abort();}
44+
}
45+
return;
46+
}
47+
/* Generated by CIL v. 1.3.7 */
48+
/* print_CIL_Input is true */
49+
50+
unsigned int base2flt(unsigned int m , int e )
51+
{ unsigned int res ;
52+
unsigned int __retres4 ;
53+
54+
{
55+
if (! m) {
56+
__retres4 = 0U;
57+
goto return_label;
58+
} else {
59+
60+
}
61+
if (m < 1U << 24U) {
62+
{
63+
while (1) {
64+
while_0_continue: /* CIL Label */ ;
65+
if (e <= -128) {
66+
__retres4 = 0U;
67+
goto return_label;
68+
} else {
69+
70+
}
71+
e = e - 1;
72+
m = m << 1U;
73+
if (m < 1U << 24U) {
74+
75+
} else {
76+
goto while_0_break;
77+
}
78+
}
79+
while_0_break: /* CIL Label */ ;
80+
}
81+
} else {
82+
{
83+
while (1) {
84+
while_1_continue: /* CIL Label */ ;
85+
if (m >= 1U << 25U) {
86+
87+
} else {
88+
goto while_1_break;
89+
}
90+
if (e >= 127) {
91+
__retres4 = 4294967295U;
92+
goto return_label;
93+
} else {
94+
95+
}
96+
e = e + 1;
97+
m = m >> 1U;
98+
}
99+
while_1_break: /* CIL Label */ ;
100+
}
101+
}
102+
m = m & ~ (1U << 24U);
103+
res = m | ((unsigned int ) (e + 128) << 24U);
104+
__retres4 = res;
105+
return_label: /* CIL Label */
106+
return (__retres4);
107+
}
108+
}
109+
unsigned int addflt(unsigned int a , unsigned int b )
110+
{ unsigned int res ;
111+
unsigned int ma ;
112+
unsigned int mb ;
113+
unsigned int delta ;
114+
int ea ;
115+
int eb ;
116+
unsigned int tmp ;
117+
unsigned int __retres10 ;
118+
119+
{
120+
if (a < b) {
121+
tmp = a;
122+
a = b;
123+
b = tmp;
124+
} else {
125+
126+
}
127+
if (! b) {
128+
__retres10 = a;
129+
goto return_label;
130+
} else {
131+
132+
}
133+
{
134+
ma = a & ((1U << 24U) - 1U);
135+
ea = (int )(a >> 24U) - 128;
136+
ma = ma | (1U << 24U);
137+
mb = b & ((1U << 24U) - 1U);
138+
eb = (int )(b >> 24U) - 128;
139+
mb = mb | (1U << 24U);
140+
__VERIFIER_assert(ea >= eb);
141+
delta = ea - eb;
142+
if(!(delta < sizeof(mb) * 8)) {abort();}
143+
mb = mb >> delta;
144+
}
145+
if (! mb) {
146+
__retres10 = a;
147+
goto return_label;
148+
} else {
149+
150+
}
151+
ma = ma + mb;
152+
if (ma & (1U << 25U)) {
153+
if (ea == 127) {
154+
__retres10 = 4294967295U;
155+
goto return_label;
156+
} else {
157+
158+
}
159+
ea = ea + 1;
160+
ma = ma >> 1U;
161+
} else {
162+
163+
}
164+
{
165+
__VERIFIER_assert(ma < 1U << 25U);
166+
ma = ma & ((1U << 24U) - 1U);
167+
res = ma | ((unsigned int )(ea + 128) << 24U);
168+
}
169+
__retres10 = res;
170+
return_label: /* CIL Label */
171+
return (__retres10);
172+
}
173+
}
174+
unsigned int mulflt(unsigned int a , unsigned int b )
175+
{ unsigned int res ;
176+
unsigned int ma ;
177+
unsigned int mb ;
178+
unsigned long long accu ;
179+
int ea ;
180+
int eb ;
181+
unsigned int tmp ;
182+
unsigned int __retres10 ;
183+
184+
{
185+
if (a < b) {
186+
tmp = a;
187+
a = b;
188+
b = tmp;
189+
} else {
190+
191+
}
192+
if (! b) {
193+
__retres10 = 0U;
194+
goto return_label;
195+
} else {
196+
197+
}
198+
ma = a & ((1U << 24U) - 1U);
199+
ea = (int )(a >> 24U) - 128;
200+
ma = ma | (1U << 24U);
201+
mb = b & ((1U << 24U) - 1U);
202+
eb = (int )(b >> 24U) - 128;
203+
mb = mb | (1U << 24U);
204+
ea = ea + eb;
205+
ea = ea + 24;
206+
if (ea > 127) {
207+
__retres10 = 4294967295U;
208+
goto return_label;
209+
} else {
210+
211+
}
212+
if (ea < -128) {
213+
__retres10 = 0U;
214+
goto return_label;
215+
} else {
216+
217+
}
218+
accu = ma;
219+
accu = accu * (unsigned long long )mb;
220+
accu = accu >> 24U;
221+
if (accu >= (unsigned long long )(1U << 25U)) {
222+
if (ea == 127) {
223+
__retres10 = 4294967295U;
224+
goto return_label;
225+
} else {
226+
227+
}
228+
ea = ea + 1;
229+
accu = accu >> 1U;
230+
if (accu >= (unsigned long long )(1U << 25U)) {
231+
__retres10 = 4294967295U;
232+
goto return_label;
233+
} else {
234+
235+
}
236+
} else {
237+
238+
}
239+
{
240+
__VERIFIER_assert(accu < (unsigned long long )(1U << 25U));
241+
__VERIFIER_assert(accu & (unsigned long long )(1U << 24U));
242+
ma = accu;
243+
ma = ma & ~ (1U << 24U);
244+
res = ma | (unsigned int )((ea + 128) << 24U);
245+
}
246+
__retres10 = res;
247+
return_label: /* CIL Label */
248+
return (__retres10);
249+
}
250+
}
251+
int main2(void)
252+
{ unsigned int a ;
253+
unsigned int ma = __VERIFIER_nondet_uint();
254+
signed char ea = __VERIFIER_nondet_char();
255+
unsigned int b ;
256+
unsigned int mb = __VERIFIER_nondet_uint();
257+
signed char eb = __VERIFIER_nondet_char();
258+
unsigned int r_add ;
259+
unsigned int zero ;
260+
int sa ;
261+
int sb ;
262+
int tmp ;
263+
int tmp___0 ;
264+
int tmp___1 ;
265+
int tmp___2 ;
266+
int tmp___3 ;
267+
int tmp___4 ;
268+
int tmp___5 ;
269+
int tmp___6 ;
270+
int tmp___7 ;
271+
int tmp___8 ;
272+
int tmp___9 ;
273+
int __retres23 ;
274+
275+
{
276+
{
277+
zero = base2flt(0, 0);
278+
a = base2flt(ma, ea);
279+
b = base2flt(mb, eb);
280+
}
281+
if (a < zero) {
282+
sa = -1;
283+
} else {
284+
if (a > zero) {
285+
tmp = 1;
286+
} else {
287+
tmp = 0;
288+
}
289+
sa = tmp;
290+
}
291+
if (b < zero) {
292+
sb = -1;
293+
} else {
294+
if (b > zero) {
295+
tmp___0 = 1;
296+
} else {
297+
tmp___0 = 0;
298+
}
299+
sb = tmp___0;
300+
}
301+
{
302+
r_add = addflt(a, b);
303+
}
304+
if (sa > 0) {
305+
if (sb > 0) {
306+
if (r_add < a) {
307+
tmp___2 = -1;
308+
} else {
309+
if (r_add > a) {
310+
tmp___1 = 1;
311+
} else {
312+
tmp___1 = 0;
313+
}
314+
tmp___2 = tmp___1;
315+
}
316+
{
317+
__VERIFIER_assert(tmp___2 >= 0);
318+
}
319+
if (r_add < b) {
320+
tmp___4 = -1;
321+
} else {
322+
if (r_add > b) {
323+
tmp___3 = 1;
324+
} else {
325+
tmp___3 = 0;
326+
}
327+
tmp___4 = tmp___3;
328+
}
329+
{
330+
__VERIFIER_assert(tmp___4 >= 0);
331+
}
332+
} else {
333+
334+
}
335+
} else {
336+
337+
}
338+
if (sa == 0) {
339+
goto _L;
340+
} else {
341+
if (sb == 0) {
342+
_L: /* CIL Label */
343+
if (r_add < a) {
344+
tmp___6 = -1;
345+
} else {
346+
if (r_add > a) {
347+
tmp___5 = 1;
348+
} else {
349+
tmp___5 = 0;
350+
}
351+
tmp___6 = tmp___5;
352+
}
353+
if (tmp___6 == 0) {
354+
tmp___9 = 1;
355+
} else {
356+
if (r_add < b) {
357+
tmp___8 = -1;
358+
} else {
359+
if (r_add > b) {
360+
tmp___7 = 1;
361+
} else {
362+
tmp___7 = 0;
363+
}
364+
tmp___8 = tmp___7;
365+
}
366+
if (tmp___8 == 0) {
367+
tmp___9 = 1;
368+
} else {
369+
tmp___9 = 0;
370+
}
371+
}
372+
{
373+
__VERIFIER_assert(tmp___9);
374+
}
375+
} else {
376+
377+
}
378+
}
379+
__retres23 = 0;
380+
return (__retres23);
381+
}
382+
}
383+
int main()
384+
{
385+
if(__VERIFIER_nondet_int())
386+
main1();
387+
else
388+
main2();
389+
}

‎c/combinations/square_1+soft_float_1-2a.c.cil.yml‎

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
format_version: '1.0'
2+
3+
input_files: 'square_1+soft_float_1-2a.c.cil.c'
4+
5+
properties:
6+
- property_file: ../properties/unreach-call.prp
7+
expected_verdict: False

0 commit comments

Comments
 (0)