Skip to content

Commit c379f9c

Browse files
peterschrammelpeterschrammel
authored
Merge pull request diffblue#5 from thk123/c-test-gen-no-prune
First pass on the C Test Generation
2 parents 4a883d0 + d68f1c8 commit c379f9c

Some content is hidden

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

66 files changed

+4703
-229
lines changed

‎regression/.gitignore

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
tests.log

‎regression/ansi-c/function_return1/main.c

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,4 @@
1+
void fun()
2+
{
3+
return 5;
4+
}

‎regression/ansi-c/function_return1/test.desc

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
CORE
2+
main.c
3+
--verbosity 2
4+
^Function fun has return void but a return statement returning signedbv was found on line.*$
5+
^SIGNAL=0$
6+
7+
--
8+
^warning: ignoring
9+
^CONVERSION ERROR$

‎regression/test-c-gen/Makefile

Lines changed: 25 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,25 @@
1+
default: tests.log
2+
3+
test:
4+
@if ! ../test.pl -c ../../../src/cbmc/cbmc ; then \
5+
../failed-tests-printer.pl ; \
6+
exit 1 ; \
7+
fi
8+
9+
tests.log: ../test.pl
10+
@if ! ../test.pl -c ../../../src/cbmc/cbmc ; then \
11+
../failed-tests-printer.pl ; \
12+
exit 1 ; \
13+
fi
14+
15+
show:
16+
@for dir in *; do \
17+
if [ -d "$$dir" ]; then \
18+
vim -o "$$dir/*.c" "$$dir/*.out"; \
19+
fi; \
20+
done;
21+
22+
clean:
23+
rm tests.log
24+
$(MAKE)
25+

‎regression/test-c-gen/array1/main.c

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,5 @@
1+
2+
int fun(int array[5])
3+
{
4+
return array[1] + array[4];
5+
}

‎regression/test-c-gen/array1/test.desc

Lines changed: 28 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,28 @@
1+
CORE
2+
main.c
3+
--function fun --cover branch --gen-c-test-case
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^#include <assert\.h>$
7+
^#include <stdio\.h>$
8+
^#include <stdlib\.h>$
9+
10+
^#include "main\.c"$
11+
^int test_main(int argc, char\* argv)$
12+
^\{$
13+
^ signed int \* arg_fun_array = ((signed int \*)NULL);$
14+
15+
^ signed int arg_fun_array\[\] = {1, 2, 3, 4, 5};$
16+
17+
^ signed int ret_fun;$
18+
^ ret_fun = fun();$
19+
20+
^ assert(ret_fun == 7);$
21+
^ exit(0);$
22+
^\}$
23+
^ return 0;$
24+
^\}$
25+
26+
27+
--
28+
^warning: ignoring

‎regression/test-c-gen/array2/main.c

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,4 @@
1+
int fun(int array[])
2+
{
3+
return array[1] + array[4];
4+
}

‎regression/test-c-gen/array2/test.desc

Lines changed: 28 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,28 @@
1+
CORE
2+
main.c
3+
--function fun --cover branch --gen-c-test-case
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^#include <assert\.h>$
7+
^#include <stdio\.h>$
8+
^#include <stdlib\.h>$
9+
10+
^#include "main\.c"$
11+
^int test_main(int argc, char\* argv)$
12+
^\{$
13+
^ signed int \* arg_fun_array = ((signed int \*)NULL);$
14+
15+
^ signed int arg_fun_array\[\] = {1, 2, 3, 4, 5};$
16+
17+
^ signed int ret_fun;$
18+
^ ret_fun = fun();$
19+
20+
^ assert(ret_fun == 7);$
21+
^ exit(0);$
22+
^\}$
23+
^ return 0;$
24+
^\}$
25+
26+
27+
--
28+
^warning: ignoring

‎regression/test-c-gen/cover1/main.c

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
void fun(int a)
2+
{
3+
if(a > 0)
4+
{
5+
a++;
6+
}
7+
else
8+
{
9+
a--;
10+
}
11+
}

‎regression/test-c-gen/cover1/test.desc

Lines changed: 20 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,20 @@
1+
CORE
2+
main.c
3+
--function fun --cover branch --gen-c-test-case
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^#include <assert\.h>$
7+
^#include <stdio\.h>$
8+
^#include <stdlib\.h>$
9+
10+
^#include "main\.c"$
11+
^int test_main(int argc, char\* argv)$
12+
^\{$
13+
^ signed int arg_fun_a = 1;$
14+
^ signed int arg_fun_a = -2147483648;$
15+
^ fun(arg_fun_a);$
16+
^ exit(0);$
17+
^ return 0;$
18+
^\}$
19+
--
20+
^warning: ignoring

‎regression/test-c-gen/function_call1/main.c

Lines changed: 19 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,19 @@
1+
int bar()
2+
{
3+
return 3;
4+
}
5+
6+
int fun()
7+
{
8+
int a = bar();
9+
if(a > 0)
10+
{
11+
a++;
12+
}
13+
else
14+
{
15+
a--;
16+
}
17+
18+
return a;
19+
}

‎regression/test-c-gen/function_call1/test.desc

Lines changed: 20 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,20 @@
1+
CORE
2+
main.c
3+
--function fun --cover branch --gen-c-test-case
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^#include <assert\.h>$
7+
^#include <stdio\.h>$
8+
^#include <stdlib\.h>$
9+
10+
^#include "main\.c"$
11+
^int test_main(int argc, char\* argv)$
12+
^\{$
13+
^ signed int ret_fun;$
14+
^ ret_fun = fun();$
15+
^ assert(ret_fun == 4)
16+
^ exit(0);$
17+
^ return 0;$
18+
^\}$
19+
--
20+
^warning: ignoring

‎regression/test-c-gen/function_call2/main.c

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
#include <math.h>
2+
3+
int fun()
4+
{
5+
double rem = fmod(4.0, 3.0);
6+
if(rem == 0.0)
7+
{
8+
return 1;
9+
}
10+
else
11+
{
12+
return -1;
13+
}
14+
}

‎regression/test-c-gen/function_call2/test.desc

Lines changed: 21 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,21 @@
1+
CORE
2+
main.c
3+
--function fun --cover branch --gen-c-test-case
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^#include <assert\.h>$
7+
^#include <stdio\.h>$
8+
^#include <stdlib\.h>$
9+
10+
^#include "main\.c"$
11+
^int test_main(int argc, char\* argv)$
12+
^\{$
13+
^ signed int ret_fun;$
14+
^ ret_fun = fun();$
15+
^ assert(ret_fun == 1);$
16+
^ assert(ret_fun == -1);$
17+
^ exit(0);$
18+
^ return 0;$
19+
^\}$
20+
--
21+
^warning: ignoring

‎regression/test-c-gen/local_variable1/main.c

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
#include <stdbool.h>
2+
3+
void fun()
4+
{
5+
int x = 0;
6+
if(x > 0)
7+
{
8+
9+
}
10+
else
11+
{
12+
13+
}
14+
}

‎regression/test-c-gen/local_variable1/test.desc

Lines changed: 20 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,20 @@
1+
CORE
2+
main.c
3+
--function fun --cover branch --gen-c-test-case
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^#include <assert\.h>$
7+
^#include <stdio\.h>$
8+
^#include <stdlib\.h>$
9+
10+
^#include "main\.c"$
11+
^int test_main(int argc, char\* argv)$
12+
^\{$
13+
^ fun();$
14+
^ exit(0);$
15+
^ return 0;$
16+
^\}$
17+
18+
19+
--
20+
^warning: ignoring

‎regression/test-c-gen/main_call1/main.c

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
//int fun(int* array[])
2+
int main(int argc, char* params[])
3+
{
4+
//return (*array[1]) + (*array[4]);
5+
return 45;
6+
}

‎regression/test-c-gen/main_call1/test.desc

Lines changed: 26 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,26 @@
1+
CORE
2+
main.c
3+
--function main --cover branch --gen-c-test-case
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^#include <assert\.h>$
7+
^#include <stdio\.h>$
8+
^#include <stdlib\.h>$
9+
10+
^#include "main\.c"$
11+
^int test_main(int argc, char\* argv)$
12+
^\{$
13+
^ signed int arg_main_argc = 4098;$
14+
^ char \*\*arg_main_params = ((char \*\*)NULL);$
15+
^ signed int ret_main;$
16+
^ ret_main = main(arg_main_argc, arg_main_params);$
17+
18+
^ assert(ret_main == 45);$
19+
^ exit(0);$
20+
^\}$
21+
^ return 0;$
22+
^\}$
23+
24+
25+
--
26+
^warning: ignoring

‎regression/test-c-gen/pointer1/main.c

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,18 @@
1+
#include <stdbool.h>
2+
3+
4+
int fun(int* ptr_x)
5+
{
6+
int y = 0;
7+
if(ptr_x)
8+
{
9+
int y = *ptr_x;
10+
y += 1;
11+
}
12+
else
13+
{
14+
y = 4;
15+
}
16+
17+
return y;
18+
}

‎regression/test-c-gen/pointer1/test.desc

Lines changed: 30 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,30 @@
1+
CORE
2+
main.c
3+
--function fun --cover branch --gen-c-test-case
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^#include <assert\.h>$
7+
^#include <stdio\.h>$
8+
^#include <stdlib\.h>$
9+
10+
^#include "main\.c"$
11+
^int test_main(int argc, char\* argv)$
12+
^\{$
13+
^ signed int \* arg_fun_ptr_x = ((signed int \*)NULL);$
14+
15+
^ signed int \* arg_fun_ptr_x = ((signed int \*)malloc(sizeof(signed int)));$
16+
^ *arg_fun_ptr_x = -1;$
17+
18+
^ signed int ret_fun;$
19+
^ ret_fun = fun();$
20+
21+
^ assert(ret_fun == 4);$
22+
23+
^ assert(ret_fun == 0);$
24+
^ exit(0);$
25+
^ return 0;$
26+
^\}$
27+
28+
29+
--
30+
^warning: ignoring

‎regression/test-c-gen/return1/main.c

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,4 @@
1+
int fun()
2+
{
3+
return 5;
4+
}

‎regression/test-c-gen/return1/test.desc

Lines changed: 20 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,20 @@
1+
CORE
2+
main.c
3+
--function fun --cover branch --gen-c-test-case
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^#include <assert\.h>$
7+
^#include <stdio\.h>$
8+
^#include <stdlib\.h>$
9+
10+
^#include "main\.c"$
11+
^int test_main(int argc, char\* argv)$
12+
^\{$
13+
^ signed int ret_fun;
14+
^ ret_fun = fun();$
15+
^ assert(ret_fun == 5);$
16+
^ exit(0);$
17+
^ return 0;$
18+
^\}$
19+
--
20+
^warning: ignoring

‎regression/test-c-gen/return2/main.c

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
#include <stdbool.h>
2+
3+
struct example_s
4+
{
5+
bool b;
6+
int x;
7+
};
8+
9+
struct example_s fun()
10+
{
11+
struct example_s return_var = { .b = true, .x = 4 };
12+
return return_var;
13+
}

0 commit comments

Comments
 (0)