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

Commit d909d36

Browse files
lembergerthlembergerth
committed
Add benchmark tasks combined from bitvector/gcd_ and floats-cdfpl/newton_
Used in 'Dirk Beyer, Marie-Christine Jakobs, Thomas Lemberger: Difference Verification with Conditions, SEFM20'
1 parent c0fbe35 commit d909d36

File tree

192 files changed

+9768
-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.

192 files changed

+9768
-0
lines changed

‎c/combinations/gcd_1+newton_1_1.i‎

Lines changed: 93 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,93 @@
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+
extern void __assert_fail(const char *, const char *, unsigned int, const char *) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
10+
void reach_error() { __assert_fail("0", "gcd_1.c", 3, "reach_error"); }
11+
12+
extern char __VERIFIER_nondet_char(void);
13+
void __VERIFIER_assert(int cond) {
14+
if (!(cond)) {
15+
ERROR: {reach_error();abort();}
16+
}
17+
return;
18+
}
19+
signed char gcd_test(signed char a, signed char b)
20+
{
21+
signed char t;
22+
23+
if (a < 0) a = -a;
24+
if (b < 0) b = -b;
25+
26+
while (b != 0) {
27+
t = b;
28+
b = a % b;
29+
a = t;
30+
}
31+
return a;
32+
}
33+
34+
35+
int main1()
36+
{
37+
signed char x = __VERIFIER_nondet_char();
38+
signed char y = __VERIFIER_nondet_char();
39+
signed char g;
40+
41+
if (y > 0 && x % y == 0) {
42+
g = gcd_test(x, y);
43+
44+
__VERIFIER_assert(g == y);
45+
}
46+
47+
return 0;
48+
}
49+
50+
unsigned int __line, const char *__function)
51+
__attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
52+
unsigned int __line, const char *__function)
53+
__attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
54+
__attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
55+
56+
void assume_abort_if_not(int cond) {
57+
if(!cond) {abort();}
58+
}
59+
float f(float x)
60+
{
61+
return x - (x*x*x)/6.0f + (x*x*x*x*x)/120.0f + (x*x*x*x*x*x*x)/5040.0f;
62+
}
63+
64+
float fp(float x)
65+
{
66+
return 1 - (x*x)/2.0f + (x*x*x*x)/24.0f + (x*x*x*x*x*x)/720.0f;
67+
}
68+
69+
int main2()
70+
{
71+
float IN = __VERIFIER_nondet_float();
72+
assume_abort_if_not(IN > -0.2f && IN < 0.2f);
73+
74+
float x = IN - f(IN)/fp(IN);
75+
76+
77+
78+
79+
80+
81+
82+
if(!(x < 0.1))
83+
{reach_error();}
84+
85+
return 0;
86+
}
87+
int main()
88+
{
89+
if(__VERIFIER_nondet_int())
90+
main1();
91+
else
92+
main2();
93+
}

‎c/combinations/gcd_1+newton_1_1.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: 'gcd_1+newton_1_1.i'
4+
5+
properties:
6+
- property_file: ../properties/unreach-call.prp
7+
expected_verdict: True

‎c/combinations/gcd_1+newton_1_2.i‎

Lines changed: 93 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,93 @@
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+
extern void __assert_fail(const char *, const char *, unsigned int, const char *) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
10+
void reach_error() { __assert_fail("0", "gcd_1.c", 3, "reach_error"); }
11+
12+
extern char __VERIFIER_nondet_char(void);
13+
void __VERIFIER_assert(int cond) {
14+
if (!(cond)) {
15+
ERROR: {reach_error();abort();}
16+
}
17+
return;
18+
}
19+
signed char gcd_test(signed char a, signed char b)
20+
{
21+
signed char t;
22+
23+
if (a < 0) a = -a;
24+
if (b < 0) b = -b;
25+
26+
while (b != 0) {
27+
t = b;
28+
b = a % b;
29+
a = t;
30+
}
31+
return a;
32+
}
33+
34+
35+
int main1()
36+
{
37+
signed char x = __VERIFIER_nondet_char();
38+
signed char y = __VERIFIER_nondet_char();
39+
signed char g;
40+
41+
if (y > 0 && x % y == 0) {
42+
g = gcd_test(x, y);
43+
44+
__VERIFIER_assert(g == y);
45+
}
46+
47+
return 0;
48+
}
49+
50+
unsigned int __line, const char *__function)
51+
__attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
52+
unsigned int __line, const char *__function)
53+
__attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
54+
__attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
55+
56+
void assume_abort_if_not(int cond) {
57+
if(!cond) {abort();}
58+
}
59+
float f(float x)
60+
{
61+
return x - (x*x*x)/6.0f + (x*x*x*x*x)/120.0f + (x*x*x*x*x*x*x)/5040.0f;
62+
}
63+
64+
float fp(float x)
65+
{
66+
return 1 - (x*x)/2.0f + (x*x*x*x)/24.0f + (x*x*x*x*x*x)/720.0f;
67+
}
68+
69+
int main2()
70+
{
71+
float IN = __VERIFIER_nondet_float();
72+
assume_abort_if_not(IN > -0.4f && IN < 0.4f);
73+
74+
float x = IN - f(IN)/fp(IN);
75+
76+
77+
78+
79+
80+
81+
82+
if(!(x < 0.1))
83+
{reach_error();}
84+
85+
return 0;
86+
}
87+
int main()
88+
{
89+
if(__VERIFIER_nondet_int())
90+
main1();
91+
else
92+
main2();
93+
}

‎c/combinations/gcd_1+newton_1_2.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: 'gcd_1+newton_1_2.i'
4+
5+
properties:
6+
- property_file: ../properties/unreach-call.prp
7+
expected_verdict: True

‎c/combinations/gcd_1+newton_1_3.i‎

Lines changed: 93 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,93 @@
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+
extern void __assert_fail(const char *, const char *, unsigned int, const char *) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
10+
void reach_error() { __assert_fail("0", "gcd_1.c", 3, "reach_error"); }
11+
12+
extern char __VERIFIER_nondet_char(void);
13+
void __VERIFIER_assert(int cond) {
14+
if (!(cond)) {
15+
ERROR: {reach_error();abort();}
16+
}
17+
return;
18+
}
19+
signed char gcd_test(signed char a, signed char b)
20+
{
21+
signed char t;
22+
23+
if (a < 0) a = -a;
24+
if (b < 0) b = -b;
25+
26+
while (b != 0) {
27+
t = b;
28+
b = a % b;
29+
a = t;
30+
}
31+
return a;
32+
}
33+
34+
35+
int main1()
36+
{
37+
signed char x = __VERIFIER_nondet_char();
38+
signed char y = __VERIFIER_nondet_char();
39+
signed char g;
40+
41+
if (y > 0 && x % y == 0) {
42+
g = gcd_test(x, y);
43+
44+
__VERIFIER_assert(g == y);
45+
}
46+
47+
return 0;
48+
}
49+
50+
unsigned int __line, const char *__function)
51+
__attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
52+
unsigned int __line, const char *__function)
53+
__attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
54+
__attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
55+
56+
void assume_abort_if_not(int cond) {
57+
if(!cond) {abort();}
58+
}
59+
float f(float x)
60+
{
61+
return x - (x*x*x)/6.0f + (x*x*x*x*x)/120.0f + (x*x*x*x*x*x*x)/5040.0f;
62+
}
63+
64+
float fp(float x)
65+
{
66+
return 1 - (x*x)/2.0f + (x*x*x*x)/24.0f + (x*x*x*x*x*x)/720.0f;
67+
}
68+
69+
int main2()
70+
{
71+
float IN = __VERIFIER_nondet_float();
72+
assume_abort_if_not(IN > -0.6f && IN < 0.6f);
73+
74+
float x = IN - f(IN)/fp(IN);
75+
76+
77+
78+
79+
80+
81+
82+
if(!(x < 0.1))
83+
{reach_error();}
84+
85+
return 0;
86+
}
87+
int main()
88+
{
89+
if(__VERIFIER_nondet_int())
90+
main1();
91+
else
92+
main2();
93+
}

‎c/combinations/gcd_1+newton_1_3.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: 'gcd_1+newton_1_3.i'
4+
5+
properties:
6+
- property_file: ../properties/unreach-call.prp
7+
expected_verdict: True

0 commit comments

Comments
 (0)