CBMC for Java regression testing

git-svn-id: svn+ssh://svn.cprover.org/srv/svn/cbmc/trunk@2533 6afb6bc1-c8e4-404c-8f48-9ae832c5b171

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;

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
+  }
+}
+

regression/cbmc-java/assert1/test.desc

@@ -0,0 +1,8 @@
+CORE
+assert1.class
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

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
+  }
+}
+

regression/cbmc-java/basic1/test.desc

@@ -0,0 +1,8 @@
+CORE
+helloworld.class
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/cbmc-java/basic2/test.desc

@@ -0,0 +1,8 @@
+CORE
+basic.class
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/cbmc-java/loop1/test.desc

@@ -0,0 +1,8 @@
+CORE
+loop1.class
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

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
   <level>                is one of CORE, THOROUGH, FUTURE or KNOWNBUG
-  <main source>          is a file with extension .c/.i/.cpp/.ii/.xml
+  <main source>          is a file with extension .c/.i/.cpp/.ii/.xml/.class
   <options>              additional options to be passed to CMD
   <required patterns>    one or more lines of regualar expressions that must occur in the output
   <disallowed patterns>  one or more lines of expressions that must not occur in output