For Java skip the check for dereference of a deallocated or dead object

COMPILING

@@ -142,7 +142,7 @@ Follow these instructions:
 1) You need a SAT solver (in source). We recommend MiniSat2. Using a
    browser, download from
 
-   http://minisat.se/downloads/minisat-2.2.1.tar.gz
+   http://ftp.debian.org/debian/pool/main/m/minisat2/minisat2_2.2.1.orig.tar.gz
 
    and then unpack with
 

regression/ansi-c/gcc_attributes7/main.i

@@ -0,0 +1,55 @@
+struct X {
+  int a;
+};
+
+struct S {
+ struct X x __attribute__((aligned(
+# 81 "ring.h" 3 4
+                         16
+# 81 "ring.h"
+                         )));
+ struct X x2 __attribute__((aligned(
+# 82 "ring.h" 3 4
+                        (((
+# 82 "ring.h"
+                        sizeof(struct X)
+# 82 "ring.h" 3 4
+                        )+16 -1)&~(16 -1))
+# 82 "ring.h"
+                        )));
+};
+
+typedef int int8_t
+# 194 "/usr/include/x86_64-linux-gnu/sys/types.h"
+__attribute__(
+# 194 "/usr/include/x86_64-linux-gnu/sys/types.h" 3 4
+(__mode__ (__QI__))
+# 194 "/usr/include/x86_64-linux-gnu/sys/types.h"
+)
+# 194 "/usr/include/x86_64-linux-gnu/sys/types.h" 3 4
+                   ;
+
+int extundelete_process_dir_block(int fs,
+        int b
+# 29 "block.h" 3 4
+                         __attribute__(
+# 29 "block.h"
+                         (unused)
+# 29 "block.h" 3 4
+                         )
+# 29 "block.h"
+                                              ,
+        int ref_offset
+# 30 "block.h" 3 4
+                      __attribute__(
+# 30 "block.h"
+                      (unused)
+# 30 "block.h" 3 4
+                      )
+# 30 "block.h"
+                                           ,
+        void *priv_data);
+
+int main()
+{
+}

regression/ansi-c/gcc_attributes7/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.i
+
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+^CONVERSION ERROR$

regression/cbmc-cover/Makefile

@@ -0,0 +1,20 @@
+default: tests.log
+
+test:
+	@if ! ../test.pl -c ../../../src/cbmc/cbmc ; then \
+		../failed-tests-printer.pl ; \
+		exit 1 ; \
+	fi
+
+tests.log: ../test.pl
+	@if ! ../test.pl -c ../../../src/cbmc/cbmc ; then \
+		../failed-tests-printer.pl ; \
+		exit 1 ; \
+	fi
+
+show:
+	@for dir in *; do \
+		if [ -d "$$dir" ]; then \
+			vim -o "$$dir/*.c" "$$dir/*.out"; \
+		fi; \
+	done;

regression/cbmc-cover/assertion1/main.c

@@ -0,0 +1,11 @@
+int main()
+{
+  int input1, input2;
+
+  __CPROVER_assert(!input1, "");
+
+  if(input1)
+  {
+    __CPROVER_assert(!input1, ""); // will work, we ignore the assertion
+  }
+}

regression/cbmc-cover/assertion1/test.desc

@@ -0,0 +1,9 @@
+CORE
+main.c
+--cover assertion
+^EXIT=0$
+^SIGNAL=0$
+^\[main.assertion.1\] file main.c line 5 function main: SATISFIED$
+^\[main.assertion.2\] file main.c line 9 function main: SATISFIED$
+--
+^warning: ignoring

regression/cbmc-cover/branch1/main.c

@@ -0,0 +1,17 @@
+int main()
+{
+  int input1, input2;
+
+  if(input1)
+  {
+    if(input1) // dependent
+    {
+    }
+  }
+  else
+  {
+    if(input2) // independent
+    {
+    }
+  }
+}

regression/cbmc-cover/branch1/test.desc

@@ -0,0 +1,13 @@
+CORE
+main.c
+--cover branch
+^EXIT=0$
+^SIGNAL=0$
+^\[main.1\] file main.c line 5 function main function main block 1 branch false: SATISFIED$
+^\[main.2\] file main.c line 5 function main function main block 1 branch true: SATISFIED$
+^\[main.3\] file main.c line 7 function main function main block 2 branch false: FAILED$
+^\[main.4\] file main.c line 7 function main function main block 2 branch true: SATISFIED$
+^\[main.5\] file main.c line 13 function main function main block 4 branch false: SATISFIED$
+^\[main.6\] file main.c line 13 function main function main block 4 branch true: SATISFIED$
+--
+^warning: ignoring

regression/cbmc-cover/branch2/main.c

@@ -0,0 +1,9 @@
+#include <stdio.h>
+
+int main()
+{
+  int ch;
+  while((ch=getc(stdin))!=-1)
+  {
+  }
+}

regression/cbmc-cover/branch2/test.desc

@@ -0,0 +1,9 @@
+CORE
+main.c
+--cover branch --unwind 2
+^EXIT=0$
+^SIGNAL=0$
+^\[main.1\] file main.c line 6 function main function main block 2 branch false: SATISFIED
+^\[main.2\] file main.c line 6 function main function main block 2 branch true: SATISFIED
+--
+^warning: ignoring

regression/cbmc-cover/branch3/main.c

@@ -0,0 +1,20 @@
+#include <assert.h>
+#include <stdio.h>
+
+int main()
+{
+  char ch;
+  unsigned state=0;
+  while((ch=getc(stdin))!=-1)
+  {
+    switch(state)
+    {
+    case 0: if(ch=='<') state=1; else state=0; break;
+    case 1: if(ch=='h') state=2; else state=0; break;
+    case 2: if(ch=='t') state=3; else state=0; break;
+    case 3: if(ch=='m') state=4; else state=0; break;
+    case 4: if(ch=='l') state=5; else state=0; break;
+    default:;
+    }
+  }
+}

regression/cbmc-cover/branch3/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--cover branch --unwind 6
+^EXIT=0$
+^SIGNAL=0$
+^\*\* 22 of 22 covered (100.0%), using .* iterations$
+--
+^warning: ignoring

regression/cbmc-cover/condition1/main.c

@@ -0,0 +1,17 @@
+int main()
+{
+  int input1, input2;
+
+  if(input1 && input2)
+  {
+  }
+  else if(input1)
+  {
+  }
+  else if(input2)
+  {
+    if(input1) // can't be true
+    {
+    }
+  }
+}

regression/cbmc-cover/condition1/test.desc

@@ -0,0 +1,18 @@
+CORE
+main.c
+--cover condition
+^EXIT=0$
+^SIGNAL=0$
+^\[main.1] file main.c line 5 function main condition .* false: SATISFIED
+^\[main.2] file main.c line 5 function main condition .* true: SATISFIED
+^\[main.3] file main.c line 5 function main condition .* false: SATISFIED
+^\[main.4] file main.c line 5 function main condition .* true: SATISFIED
+^\[main.5] file main.c line 8 function main condition .* false: SATISFIED
+^\[main.6] file main.c line 8 function main condition .* true: SATISFIED
+^\[main.7] file main.c line 11 function main condition .* false: SATISFIED
+^\[main.8] file main.c line 11 function main condition .* true: SATISFIED
+^\[main.9] file main.c line 13 function main condition .* false: FAILED
+^\[main.10] file main.c line 13 function main condition .* true: SATISFIED
+^\*\* 9 of 10 covered (90.0%)
+--
+^warning: ignoring

regression/cbmc-cover/cover1/main.c

@@ -0,0 +1,15 @@
+int main()
+{
+  int input1, input2;
+
+  __CPROVER_cover(input1);
+  __CPROVER_cover(!input1);
+
+  if(input1)
+  {
+    __CPROVER_cover(!input1); // won't work
+  }
+
+  // should not produce a goal
+  __CPROVER_assert(input1, "");
+}

regression/cbmc-cover/cover1/test.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+--cover cover
+^EXIT=0$
+^SIGNAL=0$
+^\[main.1] file main.c line 5 function main condition .*: SATISFIED$
+^\[main.2] file main.c line 6 function main condition .*: SATISFIED$
+^\[main.3] file main.c line 10 function main condition .*: FAILED$
+^\*\* 2 of 3 covered (66.7%), using .* iterations$
+--
+^warning: ignoring

regression/cbmc-cover/decision1/main.c

@@ -0,0 +1,11 @@
+int main()
+{
+  int input1, input2, input3;
+
+  if(input1 && input2 && input3)
+  {
+  }
+  else
+  {
+  }
+}

regression/cbmc-cover/decision1/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--cover decision
+^EXIT=0$
+^SIGNAL=0$
+^\*\* 2 of 2 covered (100.0%), using 2 iterations$
+--
+^warning: ignoring

regression/cbmc-cover/location1/main.c

@@ -0,0 +1,15 @@
+int main()
+{
+  int input1;
+  int x=0;
+
+  if(input1)
+  {
+    x=1;
+  }
+
+  if(input1 && !x)
+  {
+    x=2; // I am dead!
+  }
+}

regression/cbmc-cover/location1/test.desc

@@ -0,0 +1,13 @@
+CORE
+main.c
+--cover location
+^EXIT=0$
+^SIGNAL=0$
+^\[main.1\] file main.c line 3 function main block 1: SATISFIED$
+^\[main.2\] file main.c line 8 function main block 2: SATISFIED$
+^\[main.3\] file main.c line 11 function main block 3: SATISFIED$
+^\[main.4\] file main.c line 13 function main block 4: FAILED$
+^\[main.5\] file main.c line 15 function main block 5: SATISFIED$
+^\*\* 4 of 5 covered (80.0%)
+--
+^warning: ignoring

regression/cbmc-cover/mcdc1/main.c

@@ -0,0 +1,14 @@
+int main()
+{
+  // Condition and decision coverage can be had with 2 tests,
+  // but MC/DC needs six (n+1 for n conditions).
+
+  __CPROVER_bool A, B, C, D, E;
+
+  if ((A || B) && C && D && E)
+  {
+  }
+  else
+  {
+  }
+}

regression/cbmc-cover/mcdc1/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--cover mcdc
+^EXIT=0$
+^SIGNAL=0$
+^\*\* .* of .* covered (100.0%), using 6 iterations$
+--
+^warning: ignoring

regression/cbmc-java/enum1/enum1.java

@@ -0,0 +1,27 @@
+public class enum1 { 
+
+    public enum Name { 
+        ASCII(1, String.class),
+        BIGINT(2, Long.class),
+        BOOLEAN(3, Boolean.class),
+        COUNTER(4, Long.class);
+
+        final int protocolId;
+        final Class<?> javaType;
+
+        private Name(int protocolId, Class<?> javaType) {
+            this.protocolId = protocolId;
+            this.javaType = javaType;
+        }
+
+    };
+
+    public static void main(String args[]) { 
+	int i = 0;
+        for (Name t : Name.values()) { 
+	  i += t.protocolId;
+        } 
+
+    } 
+} 
+

regression/cbmc-java/enum1/test.desc

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

regression/cbmc-java/function1/Main.java

@@ -0,0 +1,19 @@
+
+class Other
+{
+  public void fail()
+  {
+    assert i == 0;
+  }
+
+  private int i;
+}
+
+public class Main
+{
+  public static void main(String[] args)
+  {
+    Other o = new Other();
+  }
+}
+