Skip to content

Commit 54aac43

Browse files
cristina-davidcristina-david
authored
Merge pull request #9 from smowton/test_gen
Merge in master, test_gen_mocks and @mgu's variable table fixes
2 parents eee80e1 + 56870e8 commit 54aac43

File tree

93 files changed

+2135
-917
lines changed

Some content is hidden

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

93 files changed

+2135
-917
lines changed

‎COMPILING

Lines changed: 7 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -52,14 +52,10 @@ We assume that you have a Debian/Ubuntu or Red Hat-like distribution.
5252
COMPILATION ON SOLARIS 11
5353
-------------------------
5454

55-
0) We recommend you get OpenCSW. Follow the instructions at
56-
57-
http://www.opencsw.org/manual/for-administrators/getting-started.html
58-
5955
1) As root, get the necessary development tools:
6056

61-
pkg install system/header
62-
/opt/csw/bin/pkgutil -i gzip coreutils wget CSWpm-libwww-perl git flex bison CSWgcc4g++
57+
pkg install system/header developer/lexer/flex developer/parser/bison developer/versioning/git
58+
pkg install --accept developer/gcc-49
6359

6460
2) As a user, get the CBMC source via
6561

@@ -70,13 +66,16 @@ COMPILATION ON SOLARIS 11
7066
cd cbmc-git
7167
wget http://ftp.debian.org/debian/pool/main/m/minisat2/minisat2_2.2.1.orig.tar.gz
7268
gtar xfz minisat_2.2.1.orig.tar.gz
69+
mv minisat2-2.2.1 minisat-2.2.1
7370
(cd minisat-2.2.1; patch -p1 < ../scripts/minisat-2.2.1-patch)
7471

7572
4) Type
7673

77-
cd src; gmake CXX=/opt/csw/bin/g++
74+
cd src; gmake
75+
76+
That should do it. To run, you will need
7877

79-
That should do it.
78+
export LD_LIBRARY_PATH=/usr/gcc/4.9/lib
8079

8180
Do not attempt to compile with gcc-45 that comes with Solaris 11.
8281
It will mis-optimize MiniSat2.

‎regression/cbmc-concurrency/norace_array2/main.c

Lines changed: 33 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,33 @@
1+
#include <assert.h>
2+
#include <pthread.h>
3+
#include <stdlib.h>
4+
5+
unsigned long data[2];
6+
7+
void *thread0(void *arg)
8+
{
9+
data[0] = 1;
10+
return NULL;
11+
}
12+
13+
void *thread1(void *arg)
14+
{
15+
data[1] = 1;
16+
return NULL;
17+
}
18+
19+
int main(int argc, char *argv[])
20+
{
21+
pthread_t t0;
22+
pthread_t t1;
23+
24+
pthread_create(&t0, NULL, thread0, NULL);
25+
pthread_create(&t1, NULL, thread1, NULL);
26+
pthread_join(t0, NULL);
27+
pthread_join(t1, NULL);
28+
29+
assert(data[0] == 1);
30+
assert(data[1] == 1);
31+
32+
return 0;
33+
}

‎regression/cbmc-concurrency/norace_array2/test.desc

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
KNOWNBUG
2+
main.c
3+
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$
7+
--
8+
^warning: ignoring

‎regression/cbmc-java/bitwise1/bitwise1.class

574 Bytes
Binary file not shown.

‎regression/cbmc-java/bitwise1/bitwise1.java

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
public class bitwise1
2+
{
3+
static char c;
4+
public static void main(String[] args)
5+
{
6+
c=1;
7+
int i = (c | 2);
8+
assert i==3;
9+
}
10+
}

‎regression/cbmc-java/bitwise1/test.desc

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
bitwise1.class
3+
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$
7+
--
8+
^warning: ignoring

‎regression/cbmc-java/recursion3/recursion3.class

633 Bytes
Binary file not shown.

‎regression/cbmc-java/recursion3/recursion3.java

Lines changed: 19 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,19 @@
1+
public class recursion3
2+
{
3+
static int f(int n)
4+
{
5+
int arg_copy = n;
6+
int to_ret;
7+
if(n <= 0)
8+
to_ret=1;
9+
else
10+
to_ret = n * f(n-1);
11+
return to_ret + arg_copy;
12+
}
13+
14+
public static void main()
15+
{
16+
int ret = f(1);
17+
assert(ret == 2);
18+
}
19+
}

‎regression/cbmc/Pointer_array5/main.c

Lines changed: 26 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,26 @@
1+
#include <assert.h>
2+
#include <stdlib.h>
3+
4+
extern int nondet_int();
5+
6+
int main() {
7+
8+
int arraylen=nondet_int();
9+
10+
if(arraylen==3)
11+
{
12+
int** array_init = malloc(sizeof(int *)*arraylen);
13+
14+
int a0, a1, a2;
15+
16+
array_init[0] = &a0;
17+
array_init[1] = &a1;
18+
array_init[2] = &a2;
19+
20+
void **local_array=(void**)array_init;
21+
22+
int *address=(int *)local_array[0];
23+
assert(address==&a0);
24+
}
25+
26+
}

‎regression/cbmc/Pointer_array5/test.desc

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
KNOWNBUG
2+
main.c
3+
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$
7+
--
8+
^warning: ignoring

‎regression/cbmc/scanf1/main.c

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -11,6 +11,7 @@ int main(void)
1111
long double ld=0;
1212
long int li=0;
1313
void *p=0;
14+
char buffer[10];
1415

1516
__CPROVER_scanf("%c", &c);
1617
__CPROVER_scanf("%hhd", &si);
@@ -20,6 +21,7 @@ int main(void)
2021
__CPROVER_scanf("%Lf", &ld);
2122
__CPROVER_scanf("%li", &li);
2223
__CPROVER_scanf("%p", &p);
24+
__CPROVER_scanf("%s", buffer);
2325

2426
assert(c==0); // may fail
2527
assert(si==0); // may fail
@@ -28,6 +30,7 @@ int main(void)
2830
assert(d==0); // may fail
2931
assert(li==0); // may fail
3032
assert(p==0); // may fail
33+
assert(buffer[0]==0); // may fail
3134

3235
return 0;
3336
}

‎regression/cbmc/scanf1/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,6 +3,6 @@ main.c
33

44
^EXIT=10$
55
^SIGNAL=0$
6-
^\*\* 7 of 7 failed
6+
^\*\* 8 of 8 failed
77
--
88
^warning: ignoring

‎regression/test_gen/array_parameter/A.class

202 Bytes
Binary file not shown.

‎regression/test_gen/array_parameter/TestGenTest.class

639 Bytes
Binary file not shown.

‎regression/test_gen/array_parameter/TestGenTest.java

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
2+
public class TestGenTest {
3+
4+
public static void test(int[] got, A[] got2, long[] got3) {
5+
6+
assert(!(got != null && got.length == 2 && got[0] == 1 && got[1] == 2 && got2 != null && got2.length == 2 && got2[0] != null && got2[1] != null && got2[0].x == 3 && got2[1].x == 4 && got3 != null && got3.length == 1 && got3[0] == 100));
7+
8+
}
9+
10+
}
11+
12+
class A {
13+
14+
int x;
15+
16+
}

‎regression/test_gen/array_parameter/test.desc

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
CORE
2+
TestGenTest.class
3+
--stop-on-fail --gen-java-test-case --function TestGenTest.test
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^.*100l.*$
7+
^.*setInstanceField.*3.*$
8+
^.*setInstanceField.*4.*$
9+
^.*1, 2.*$

‎regression/test_gen/java1/TestGenTest.class

26 Bytes
Binary file not shown.

‎regression/test_gen/java1/TestGenTest.java

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -35,6 +35,10 @@ public class TestGenTest
3535
{
3636
public static void f(B param0, C param1, int param2)
3737
{
38+
39+
if(param0 == null || param1 == null || param1.c_field_1 == null)
40+
return;
41+
3842
int a_field_0=param0.a_field_0;
3943
int a_field_1=param0.a_field_1;
4044
int b_field_0=param0.b_field_0;

‎regression/test_gen/java1/test.desc

Lines changed: 13 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -3,19 +3,19 @@ TestGenTest.class
33
--gen-java-test-case --stop-on-fail --function TestGenTest.f
44
^EXIT=0$
55
^SIGNAL=0$
6-
^ *B tmp_object_factory[$]5=[(]B[)] com.diffblue.java_testcase.Reflector.forceInstance[(]"B"[)];$
7-
^ *com.diffblue.java_testcase.Reflector.setInstanceField[(]tmp_object_factory[$]5,"a_field_0",495[)];$
8-
^ *com.diffblue.java_testcase.Reflector.setInstanceField[(]tmp_object_factory[$]5,"a_field_1",494[)];$
9-
^ *com.diffblue.java_testcase.Reflector.setInstanceField[(]tmp_object_factory[$]5,"b_field_0",493[)];$
10-
^ *C tmp_object_factory[$]4=[(]C[)] com.diffblue.java_testcase.Reflector.forceInstance[(]"C"[)];$
11-
^ *com.diffblue.java_testcase.Reflector.setInstanceField[(]tmp_object_factory[$]4,"c_field_0",496[)];$
12-
^ *com.diffblue.java_testcase.Reflector.setInstanceField[(]tmp_object_factory$4,"c_field_1",tmp_object_factory[$]5[)];$
13-
^ *B tmp_object_factory[$]3=[(]B[)] com.diffblue.java_testcase.Reflector.forceInstance[(]"B"[)];$
14-
^ *com.diffblue.java_testcase.Reflector.setInstanceField[(]tmp_object_factory[$]3,"a_field_0",499[)];$
15-
^ *com.diffblue.java_testcase.Reflector.setInstanceField[(]tmp_object_factory[$]3,"a_field_1",498[)];$
16-
^ *com.diffblue.java_testcase.Reflector.setInstanceField[(]tmp_object_factory[$]3,"b_field_0",497[)];$
17-
^ *B arg0a=tmp_object_factory[$]3;$
18-
^ *C arg1a=tmp_object_factory[$]4;$
6+
^ *B tmp_object_factory[$].*=[(]B[)] com.diffblue.java_testcase.Reflector.forceInstance[(]"B"[)];$
7+
^ *com.diffblue.java_testcase.Reflector.setInstanceField[(]tmp_object_factory[$].*,"a_field_0",495[)];$
8+
^ *com.diffblue.java_testcase.Reflector.setInstanceField[(]tmp_object_factory[$].*,"a_field_1",494[)];$
9+
^ *com.diffblue.java_testcase.Reflector.setInstanceField[(]tmp_object_factory[$].*,"b_field_0",493[)];$
10+
^ *C tmp_object_factory[$].*=[(]C[)] com.diffblue.java_testcase.Reflector.forceInstance[(]"C"[)];$
11+
^ *com.diffblue.java_testcase.Reflector.setInstanceField[(]tmp_object_factory[$].*,"c_field_0",496[)];$
12+
^ *com.diffblue.java_testcase.Reflector.setInstanceField[(]tmp_object_factory[$].*,"c_field_1",tmp_object_factory[$].*[)];$
13+
^ *B tmp_object_factory[$].*=[(]B[)] com.diffblue.java_testcase.Reflector.forceInstance[(]"B"[)];$
14+
^ *com.diffblue.java_testcase.Reflector.setInstanceField[(]tmp_object_factory[$].*,"a_field_0",499[)];$
15+
^ *com.diffblue.java_testcase.Reflector.setInstanceField[(]tmp_object_factory[$].*,"a_field_1",498[)];$
16+
^ *com.diffblue.java_testcase.Reflector.setInstanceField[(]tmp_object_factory[$].*,"b_field_0",497[)];$
17+
^ *B arg0a=tmp_object_factory[$].*;$
18+
^ *C arg1a=tmp_object_factory[$].*;$
1919
^ *int arg2i=492;$
2020
^ *TestGenTest.f[(]arg0a, arg1a, arg2i[)];$
2121
--

‎regression/test_gen/opaque_direct_constructor_fields/test.desc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -3,5 +3,5 @@ TestGenTest.class
33
--stop-on-fail --gen-java-test-case --function TestGenTest.test
44
^EXIT=0$
55
^SIGNAL=0$
6-
^.*Reflector.setInstanceField(to_construct$1,"x",1).*$
7-
^.*Reflector.setInstanceField(to_construct$1,"y",2).*$
6+
^.*Reflector.setInstanceField(dynamic_object.,"x",1).*$
7+
^.*Reflector.setInstanceField(dynamic_object.,"y",2).*$

‎regression/test_gen/opaque_instance_object/test.desc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -3,5 +3,5 @@ TestGenTest.class
33
--stop-on-fail --gen-java-test-case --function TestGenTest.test
44
^EXIT=0$
55
^SIGNAL=0$
6-
^.*Reflector.setInstanceField(to_return\$2,"x",1).*$
7-
^.*Reflector.setInstanceField(to_return\$2,"x",2).*$
6+
^.*Reflector.setInstanceField(dynamic_object.,"x",1).*$
7+
^.*Reflector.setInstanceField(dynamic_object.,"x",2).*$

‎regression/test_gen/opaque_object_tree/test.desc

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -3,6 +3,6 @@ TestGenTest.class
33
--stop-on-fail --gen-java-test-case --function TestGenTest.test
44
^EXIT=0$
55
^SIGNAL=0$
6-
^.*Reflector.setInstanceField(dynamic_object2,"x",2).*$
7-
^.*Reflector.setInstanceField(to_construct$2,"y",dynamic_object2).*$
8-
^.*Reflector.setInstanceField(to_construct$2,"x",1).*$
6+
^.*Reflector.setInstanceField(dynamic_object.,"x",2).*$
7+
^.*Reflector.setInstanceField(dynamic_object.,"y",dynamic_object.).*$
8+
^.*Reflector.setInstanceField(dynamic_object.,"x",1).*$

‎regression/test_gen/opaque_object_tree_methods/test.desc

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ TestGenTest.class
33
--stop-on-fail --gen-java-test-case --function TestGenTest.test
44
^EXIT=0$
55
^SIGNAL=0$
6-
^.*Reflector.setInstanceField(dynamic_object2,"x",2).*$
7-
^.*Reflector.setInstanceField(to_construct$2,"y",dynamic_object2).*$
8-
^.*Reflector.setInstanceField(to_construct$2,"x",1).*$
6+
^.*Reflector.setInstanceField(dynamic_object.,"x",2).*$
7+
^.*Reflector.setInstanceField(dynamic_object.,"y",dynamic_object.).*$
8+
^.*Reflector.setInstanceField(dynamic_object.,"x",1).*$
99
^.*Opaque2_get_answer_list.add(3).*$

‎regression/test_gen/opaque_returns_null_object/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,5 +3,5 @@ TestGenTest.class
33
--stop-on-fail --gen-java-test-case --function TestGenTest.test
44
^EXIT=0$
55
^SIGNAL=0$
6-
^.*Reflector\.setInstanceField(to_return$1,"x",2).*$
6+
^.*Reflector\.setInstanceField(dynamic_object.,"x",2).*$
77
^.*to_return$1=null.*$

‎regression/test_gen/opaque_static_object/test.desc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -3,5 +3,5 @@ TestGenTest.class
33
--stop-on-fail --gen-java-test-case --function TestGenTest.test
44
^EXIT=0$
55
^SIGNAL=0$
6-
^.*Reflector\.setInstanceField(to_return\$3,"x",1).*$
7-
^.*Reflector\.setInstanceField(to_return\$3,"x",2);.*$
6+
^.*Reflector\.setInstanceField(dynamic_object.,"x",1).*$
7+
^.*Reflector\.setInstanceField(dynamic_object.,"x",2).*$

‎scripts/generate_vcxproj

Lines changed: 13 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,8 @@
1-
dest=../src
1+
#/bin/bash
22

3-
if ! [ -e $dest/Makefile ] ; then echo Makefile not found ; exit 1; fi
3+
dest=..
4+
5+
if ! [ -e $dest/src/Makefile ] ; then echo Makefile not found ; exit 1; fi
46

57
echo Generating Visual Studio Project files in $dest
68

@@ -12,13 +14,13 @@ function doit {
1214
# this collects all the files needed
1315
echo " <ItemGroup>" >> $dest/$1.vcxproj
1416
for dir in $dirs ; do
15-
sources="`(cd $dest/$dir; make sources)`"
17+
sources="`(cd $dest/src/$dir; make sources)`"
1618
for s in $sources ; do
17-
echo " <ClCompile Include=\"${dir}\\${s}\"/>" >> $dest/$1.vcxproj
19+
echo " <ClCompile Include=\"src\\${dir}\\${s}\"/>" >> $dest/$1.vcxproj
1820
done
1921
done
20-
echo " <ClCompile Include=\"..\\minisat-2.2.0\\core\\Solver.cc\"/>" >> $dest/$1.vcxproj
21-
echo " <ClCompile Include=\"..\\minisat-2.2.0\\simp\\SimpSolver.cc\"/>" >> $dest/$1.vcxproj
22+
echo " <ClCompile Include=\"minisat-2.2.1\\minisat\\core\\Solver.cc\"/>" >> $dest/$1.vcxproj
23+
echo " <ClCompile Include=\"minisat-2.2.1\\minisat\\simp\\SimpSolver.cc\"/>" >> $dest/$1.vcxproj
2224
echo " </ItemGroup>" >> $dest/$1.vcxproj
2325

2426
cat vcxproj.2 >> $dest/$1.vcxproj
@@ -32,13 +34,13 @@ function doit {
3234

3335
echo " <ItemGroup>" >> $dest/$1.vcxproj.filters
3436
for dir in $dirs ; do
35-
sources="`(cd $dest/$dir; make sources)`"
37+
sources="`(cd $dest/src/$dir; make sources)`"
3638
for s in $sources ; do
37-
echo " <ClCompile Include=\"${dir}\\${s}\"><Filter>${dir}</Filter></ClCompile>" >> $dest/$1.vcxproj.filters
39+
echo " <ClCompile Include=\"src\\${dir}\\${s}\"><Filter>${dir}</Filter></ClCompile>" >> $dest/$1.vcxproj.filters
3840
done
3941
done
40-
echo " <ClCompile Include=\"..\\minisat-2.2.0\\core\\Solver.cc\"><Filter>minisat2</Filter></ClCompile>" >> $dest/$1.vcxproj.filters
41-
echo " <ClCompile Include=\"..\\minisat-2.2.0\\simp\\SimpSolver.cc\"><Filter>minisat2</Filter></ClCompile>" >> $dest/$1.vcxproj.filters
42+
echo " <ClCompile Include=\"minisat-2.2.1\\minisat\\core\\Solver.cc\"><Filter>minisat2</Filter></ClCompile>" >> $dest/$1.vcxproj.filters
43+
echo " <ClCompile Include=\"minisat-2.2.1\\minisat\\simp\\SimpSolver.cc\"><Filter>minisat2</Filter></ClCompile>" >> $dest/$1.vcxproj.filters
4244
echo " </ItemGroup>" >> $dest/$1.vcxproj.filters
4345

4446
for dir in $dirs minisat2 ; do
@@ -51,7 +53,7 @@ function doit {
5153
dirs="big-int langapi util ansi-c assembler cpp java_bytecode xmllang solvers goto-symex analyses pointer-analysis goto-programs linking cbmc"
5254
doit cbmc
5355

54-
dirs="big-int langapi util ansi-c assembler cpp java_bytecode xmllang solvers goto-symex analyses pointer-analysis goto-programs linking goto-cc"
56+
dirs="big-int langapi util ansi-c assembler cpp java_bytecode xmllang solvers goto-symex analyses pointer-analysis goto-programs linking jsil goto-cc"
5557
doit goto-cc
5658

5759
dirs="big-int langapi util ansi-c assembler cpp java_bytecode xmllang solvers goto-symex analyses pointer-analysis goto-programs linking goto-instrument"

‎scripts/vcxproj.1

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -49,7 +49,7 @@
4949
<WarningLevel>Level3</WarningLevel>
5050
<Optimization>Disabled</Optimization>
5151
<PreprocessorDefinitions>WIN32;_DEBUG;_WINDOWS;%(PreprocessorDefinitions);STL_HASH_TR1;HAVE_MINISAT2</PreprocessorDefinitions>
52-
<AdditionalIncludeDirectories>$(ProjectDir);$(ProjectDir)/../minisat-2.2.0</AdditionalIncludeDirectories>
52+
<AdditionalIncludeDirectories>$(ProjectDir)/src;$(ProjectDir)/minisat-2.2.1</AdditionalIncludeDirectories>
5353
</ClCompile>
5454
<Link>
5555
<SubSystem>Console</SubSystem>
@@ -64,7 +64,7 @@
6464
<FunctionLevelLinking>true</FunctionLevelLinking>
6565
<IntrinsicFunctions>true</IntrinsicFunctions>
6666
<PreprocessorDefinitions>WIN32;NDEBUG;_WINDOWS;%(PreprocessorDefinitions);STL_HASH_TR1;HAVE_MINISAT2</PreprocessorDefinitions>
67-
<AdditionalIncludeDirectories>$(ProjectDir);$(ProjectDir)/../minisat-2.2.0</AdditionalIncludeDirectories>
67+
<AdditionalIncludeDirectories>$(ProjectDir)/src;$(ProjectDir)/minisat-2.2.1</AdditionalIncludeDirectories>
6868
</ClCompile>
6969
<Link>
7070
<SubSystem>Console</SubSystem>

0 commit comments

Comments
 (0)