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

Commit 3506183

Browse files
MartinSpiesslMartinSpiessl
committed
Include assert.h in .c files, add .i files
1 parent dfe8b22 commit 3506183

File tree

159 files changed

+1636
-424
lines changed

Some content is hidden

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

159 files changed

+1636
-424
lines changed

‎c/loop-zilu/benchmark01_conjunctive.c‎

Lines changed: 2 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,5 @@
1-
extern void __assert_fail (__const char *__assertion, __const char *__file,
2-
unsigned int __line, __const char *__function)
3-
__attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
4-
extern int __VERIFIER_nondet_int(void);
5-
extern _Bool __VERIFIER_nondet_bool(void);
6-
7-
void reach_error(void) {__assert_fail ("0", "benchmark01_conjunctive.c", 11, __PRETTY_FUNCTION__);}
1+
#include <assert.h>
2+
void reach_error(void) {assert(0);}
83

94
void __VERIFIER_assert(int cond) {
105
if (!cond) {

‎c/loop-zilu/benchmark01_conjunctive.i‎

Lines changed: 27 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,27 @@
1+
2+
extern void __assert_fail (const char *__assertion, const char *__file,
3+
unsigned int __line, const char *__function)
4+
__attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
5+
extern void __assert_perror_fail (int __errnum, const char *__file,
6+
unsigned int __line, const char *__function)
7+
__attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
8+
extern void __assert (const char *__assertion, const char *__file, int __line)
9+
__attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
10+
11+
void reach_error(void) {((void) sizeof ((0) ? 1 : 0), __extension__ ({ if (0) ; else __assert_fail ("0", "benchmark01_conjunctive.c", 2, __extension__ __PRETTY_FUNCTION__); }));}
12+
void __VERIFIER_assert(int cond) {
13+
if (!cond) {
14+
reach_error();
15+
}
16+
}
17+
int main() {
18+
int x = __VERIFIER_nondet_int();
19+
int y = __VERIFIER_nondet_int();
20+
if (!(x==1 && y==1)) return 0;
21+
while (__VERIFIER_nondet_bool()) {
22+
x=x+y;
23+
y=x;
24+
}
25+
__VERIFIER_assert(y>=1);
26+
return 0;
27+
}

‎c/loop-zilu/benchmark01_conjunctive.yml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
format_version: '2.0'
22

3-
input_files: 'benchmark01_conjunctive.c'
3+
input_files: 'benchmark01_conjunctive.i'
44

55
properties:
66
- property_file: ../properties/unreach-call.prp

‎c/loop-zilu/benchmark02_linear.c‎

Lines changed: 2 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,5 @@
1-
extern void __assert_fail (__const char *__assertion, __const char *__file,
2-
unsigned int __line, __const char *__function)
3-
__attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
4-
extern int __VERIFIER_nondet_int(void);
5-
extern _Bool __VERIFIER_nondet_bool(void);
6-
7-
void reach_error(void) {__assert_fail ("0", "benchmark02_linear.c", 11, __PRETTY_FUNCTION__);}
1+
#include <assert.h>
2+
void reach_error(void) {assert(0);}
83

94
void __VERIFIER_assert(int cond) {
105
if (!cond) {

‎c/loop-zilu/benchmark02_linear.i‎

Lines changed: 28 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,28 @@
1+
2+
extern void __assert_fail (const char *__assertion, const char *__file,
3+
unsigned int __line, const char *__function)
4+
__attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
5+
extern void __assert_perror_fail (int __errnum, const char *__file,
6+
unsigned int __line, const char *__function)
7+
__attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
8+
extern void __assert (const char *__assertion, const char *__file, int __line)
9+
__attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
10+
11+
void reach_error(void) {((void) sizeof ((0) ? 1 : 0), __extension__ ({ if (0) ; else __assert_fail ("0", "benchmark02_linear.c", 2, __extension__ __PRETTY_FUNCTION__); }));}
12+
void __VERIFIER_assert(int cond) {
13+
if (!cond) {
14+
reach_error();
15+
}
16+
}
17+
int main() {
18+
int n = __VERIFIER_nondet_int();
19+
int i = __VERIFIER_nondet_int();
20+
int l = __VERIFIER_nondet_int();
21+
i = l;
22+
if (!(l>0)) return 0;
23+
while (i < n) {
24+
i++;
25+
}
26+
__VERIFIER_assert(l>=1);
27+
return 0;
28+
}

‎c/loop-zilu/benchmark02_linear.yml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
format_version: '2.0'
22

3-
input_files: 'benchmark02_linear.c'
3+
input_files: 'benchmark02_linear.i'
44

55
properties:
66
- property_file: ../properties/unreach-call.prp

‎c/loop-zilu/benchmark03_linear.c‎

Lines changed: 2 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,5 @@
1-
extern void __assert_fail (__const char *__assertion, __const char *__file,
2-
unsigned int __line, __const char *__function)
3-
__attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
4-
extern int __VERIFIER_nondet_int(void);
5-
extern _Bool __VERIFIER_nondet_bool(void);
6-
7-
void reach_error(void) {__assert_fail ("0", "benchmark03_linear.c", 11, __PRETTY_FUNCTION__);}
1+
#include <assert.h>
2+
void reach_error(void) {assert(0);}
83

94
void __VERIFIER_assert(int cond) {
105
if (!cond) {

‎c/loop-zilu/benchmark03_linear.i‎

Lines changed: 34 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,34 @@
1+
2+
extern void __assert_fail (const char *__assertion, const char *__file,
3+
unsigned int __line, const char *__function)
4+
__attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
5+
extern void __assert_perror_fail (int __errnum, const char *__file,
6+
unsigned int __line, const char *__function)
7+
__attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
8+
extern void __assert (const char *__assertion, const char *__file, int __line)
9+
__attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
10+
11+
void reach_error(void) {((void) sizeof ((0) ? 1 : 0), __extension__ ({ if (0) ; else __assert_fail ("0", "benchmark03_linear.c", 2, __extension__ __PRETTY_FUNCTION__); }));}
12+
void __VERIFIER_assert(int cond) {
13+
if (!cond) {
14+
reach_error();
15+
}
16+
}
17+
int main() {
18+
int x = __VERIFIER_nondet_int();
19+
int y = __VERIFIER_nondet_int();
20+
int i = __VERIFIER_nondet_int();
21+
int j = __VERIFIER_nondet_int();
22+
_Bool flag = __VERIFIER_nondet_bool();
23+
x = 0; y = 0;
24+
if (!(i==0 && j==0)) return 0;
25+
while (__VERIFIER_nondet_bool()) {
26+
x++;
27+
y++;
28+
i+=x;
29+
j+=y;
30+
if (flag) j+=1;
31+
}
32+
__VERIFIER_assert(j>=i);
33+
return 0;
34+
}

‎c/loop-zilu/benchmark03_linear.yml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
format_version: '2.0'
22

3-
input_files: 'benchmark03_linear.c'
3+
input_files: 'benchmark03_linear.i'
44

55
properties:
66
- property_file: ../properties/unreach-call.prp

‎c/loop-zilu/benchmark04_conjunctive.c‎

Lines changed: 2 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,5 @@
1-
extern void __assert_fail (__const char *__assertion, __const char *__file,
2-
unsigned int __line, __const char *__function)
3-
__attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
4-
extern int __VERIFIER_nondet_int(void);
5-
extern _Bool __VERIFIER_nondet_bool(void);
6-
7-
void reach_error(void) {__assert_fail ("0", "benchmark04_conjunctive.c", 11, __PRETTY_FUNCTION__);}
1+
#include <assert.h>
2+
void reach_error(void) {assert(0);}
83

94
void __VERIFIER_assert(int cond) {
105
if (!cond) {

0 commit comments

Comments
 (0)