diff --git a/regression/cbmc-java/Makefile b/regression/cbmc-java/Makefile new file mode 100644 index 0000000000..5ac5a21995 --- /dev/null +++ b/regression/cbmc-java/Makefile @@ -0,0 +1,14 @@ +default: tests.log + +test: + @../test.pl -c ../../../src/cbmc/cbmc + +tests.log: ../test.pl + @../test.pl -c ../../../src/cbmc/cbmc + +show: + @for dir in *; do \ + if [ -d "$$dir" ]; then \ + vim -o "$$dir/*.java" "$$dir/*.out"; \ + fi; \ + done; diff --git a/regression/cbmc-java/assert1/assert1.class b/regression/cbmc-java/assert1/assert1.class new file mode 100644 index 0000000000..2ef2c11fb4 Binary files /dev/null and b/regression/cbmc-java/assert1/assert1.class differ diff --git a/regression/cbmc-java/assert1/assert1.java b/regression/cbmc-java/assert1/assert1.java new file mode 100644 index 0000000000..6c7999519f --- /dev/null +++ b/regression/cbmc-java/assert1/assert1.java @@ -0,0 +1,13 @@ +class assert1 +{ + public static void main(String[] args) + { + java.util.Random random = new java.util.Random(42); + + int i=random.nextInt(); + + if(i>=10) + assert i>=20; // should hold + } +} + diff --git a/regression/cbmc-java/assert1/test.desc b/regression/cbmc-java/assert1/test.desc new file mode 100644 index 0000000000..aa2e9dabdf --- /dev/null +++ b/regression/cbmc-java/assert1/test.desc @@ -0,0 +1,8 @@ +CORE +assert1.class + +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/regression/cbmc-java/assert2/assert2.class b/regression/cbmc-java/assert2/assert2.class new file mode 100644 index 0000000000..488b2a1237 Binary files /dev/null and b/regression/cbmc-java/assert2/assert2.class differ diff --git a/regression/cbmc-java/assert2/assert2.java b/regression/cbmc-java/assert2/assert2.java new file mode 100644 index 0000000000..7594f4c2ad --- /dev/null +++ b/regression/cbmc-java/assert2/assert2.java @@ -0,0 +1,13 @@ +class assert2 +{ + public static void main(String[] args) + { + java.util.Random random = new java.util.Random(42); + + int i=random.nextInt(); + + if(i>=1000) + assert i>1000; // should fail + } +} + diff --git a/regression/cbmc-java/basic1/test.desc b/regression/cbmc-java/basic1/test.desc new file mode 100644 index 0000000000..6d559f03df --- /dev/null +++ b/regression/cbmc-java/basic1/test.desc @@ -0,0 +1,8 @@ +CORE +helloworld.class + +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/regression/cbmc-java/basic2/test.desc b/regression/cbmc-java/basic2/test.desc new file mode 100644 index 0000000000..330ef6e655 --- /dev/null +++ b/regression/cbmc-java/basic2/test.desc @@ -0,0 +1,8 @@ +CORE +basic.class + +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/regression/cbmc-java/loop1/test.desc b/regression/cbmc-java/loop1/test.desc new file mode 100644 index 0000000000..af0a158e61 --- /dev/null +++ b/regression/cbmc-java/loop1/test.desc @@ -0,0 +1,8 @@ +CORE +loop1.class + +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/regression/test.pl b/regression/test.pl index 3f7e14bc68..57882e6cc9 100755 --- a/regression/test.pl +++ b/regression/test.pl @@ -54,7 +54,7 @@ sub test($$$$$) { $options =~ s/$ign//g if(defined($ign)); my $output = $input; - $output =~ s/\.(c|i|cpp|ii|xml)$/.out/; + $output =~ s/\.(c|i|cpp|ii|xml|class)$/.out/; if($output eq $input) { print("Error in test file -- $test\n"); @@ -169,7 +169,7 @@ follows the format specified below. Any line starting with // will be ignored. where is one of CORE, THOROUGH, FUTURE or KNOWNBUG -
is a file with extension .c/.i/.cpp/.ii/.xml +
is a file with extension .c/.i/.cpp/.ii/.xml/.class additional options to be passed to CMD one or more lines of regualar expressions that must occur in the output one or more lines of expressions that must not occur in output