Merge master 20170705

.gitignore

@@ -112,3 +112,6 @@ src/util/irep_ids_convert
 src/util/irep_ids_convert.exe
 
 *.pyc
+
+# auto generated documentation
+doc/html/

CHANGELOG

@@ -8,6 +8,8 @@
 * GOTO-ANALYZER: New option --unreachable-functions, --reachable-functions
 * GOTO-INSTRUMENT: New option --undefined-function-is-assume-false
 * GOTO-INSTRUMENT: New option --remove-function-body
+* GOTO-INSTRUMENT: New option --use-all-headers, changed --use-system-headers to
+  --no-system-headers
 
 
 5.7

regression/cbmc-java/LocalVarTable5/test.desc

@@ -4,7 +4,7 @@ test.class
 dead anonlocal::1i
 dead anonlocal::2i
 dead anonlocal::3a
-dead new_tmp0
+dead new_tmp[0-9]+
 ^EXIT=0$
 ^SIGNAL=0$
 --

regression/cbmc-java/array2/test.desc

@@ -0,0 +1,6 @@
+CORE
+test.class
+--function test.f --cover location
+\d+ of \d+ covered
+--
+^warning: ignoring

regression/cbmc-java/array2/test.java

@@ -0,0 +1,16 @@
+public class test {
+
+  public void f(int unknown) {
+
+    int[] arr;
+    if(unknown > 0)
+      arr = new int[1];
+    else
+      arr = new int[0];
+
+    if(unknown > 0)
+      arr[0]=1;
+
+  }
+
+}

regression/cbmc-java/destructor1/test.desc

@@ -5,4 +5,4 @@ Break.class
 ^SIGNAL=0$
 dead i;
 --
-GOTO 10
+GOTO 11

regression/cbmc-java/integer_without_simplify1/test.desc

@@ -0,0 +1,7 @@
+CORE
+test.class
+--no-simplify --function test.f --cover location
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring

regression/cbmc-java/integer_without_simplify1/test.java

@@ -0,0 +1,10 @@
+
+public class test {
+
+  public void f() {
+
+    int x = 50;
+
+  }
+
+}

regression/cbmc-java/stack_var1/README

@@ -0,0 +1,9 @@
+This regression test is created from the .j file with the jasmin assembler.
+https://github.com/Sable/jasmin
+
+On Ubuntu, it is available as jasmin-sable. To convert a .j file, it is
+sufficient to do
+
+> jasmin $FILE.j
+
+and it will create the corresponding $FILE.class file.

regression/cbmc-java/stack_var1/stack_test.java

@@ -0,0 +1,7 @@
+public class stack_test {
+  public static void main(String[] args) {
+    stack_var1 s = new stack_var1();
+    int n = s.f(1);
+    assert(n==0);
+  }
+}

regression/cbmc-java/stack_var1/stack_var1.j

@@ -0,0 +1,22 @@
+.class public stack_var1
+.super java/lang/Object
+
+.method public <init>()V
+   aload_0
+   invokenonvirtual java/lang/Object/<init>()V
+   return
+.end method
+
+.method public f(I)I
+   .limit stack 2
+   .limit locals 2
+
+   ;; copy of arg on stack
+   iload_1
+   ;; increment arg
+   iinc 1 1
+   ;; incremented copy on stack
+   iload_1
+   isub
+   ireturn
+.end method

regression/cbmc-java/stack_var1/test.desc

@@ -0,0 +1,9 @@
+CORE
+stack_test.class
+
+^EXIT=10$
+^SIGNAL=0$
+^.*assertion at file stack_test.java line 5 function.*: FAILURE$
+^VERIFICATION FAILED$
+--
+^warning: ignoring

regression/cbmc-java/stack_var10/README

@@ -0,0 +1,9 @@
+This regression test is created from the .j file with the jasmin assembler.
+https://github.com/Sable/jasmin
+
+On Ubuntu, it is available as jasmin-sable. To convert a .j file, it is
+sufficient to do
+
+> jasmin $FILE.j
+
+and it will create the corresponding $FILE.class file.

regression/cbmc-java/stack_var10/stack_test.java

@@ -0,0 +1,7 @@
+public class stack_test {
+  public static void main(String[] args) {
+    stack_var10 s = new stack_var10();
+    int n = s.f();
+    assert(n==0);
+  }
+}

regression/cbmc-java/stack_var10/stack_var10.j

@@ -0,0 +1,28 @@
+.class public stack_var10
+.super java/lang/Object
+
+.field private static n I
+
+.method public <init>()V
+.limit stack 5
+   aload_0
+   invokenonvirtual java/lang/Object/<init>()V
+   return
+.end method
+
+.method public f()I
+   .limit stack 8
+   .limit locals 5
+
+   iconst_1
+   istore_1
+   iconst_0
+   istore_2
+   ;; lvar1 is 1, lvar2 is 0
+   iload_1
+   iload_2
+   ;; on stack 1, 0
+   istore_1
+   ;; store 0 into lvar1
+   ireturn
+.end method

regression/cbmc-java/stack_var10/test.desc

@@ -0,0 +1,9 @@
+CORE
+stack_test.class
+
+^EXIT=10$
+^SIGNAL=0$
+^.*assertion at file stack_test.java line 5 function.*: FAILURE$
+^VERIFICATION FAILED$
+--
+^warning: ignoring

regression/cbmc-java/stack_var11/README

@@ -0,0 +1,9 @@
+This regression test is created from the .j file with the jasmin assembler.
+https://github.com/Sable/jasmin
+
+On Ubuntu, it is available as jasmin-sable. To convert a .j file, it is
+sufficient to do
+
+> jasmin $FILE.j
+
+and it will create the corresponding $FILE.class file.

regression/cbmc-java/stack_var11/stack_test.java

@@ -0,0 +1,7 @@
+public class stack_test {
+  public static void main(String[] args) {
+    stack_var11 s = new stack_var11();
+    int n = s.f();
+    assert(n==0);
+  }
+}

regression/cbmc-java/stack_var11/stack_var11.j

@@ -0,0 +1,31 @@
+.class public stack_var11
+.super java/lang/Object
+
+.field private arr [I
+
+.method public <init>()V
+.limit stack 5
+   aload_0
+   invokenonvirtual java/lang/Object/<init>()V
+   aload_0
+   iconst_2
+   newarray int
+   putfield stack_var11/arr [I
+   return
+.end method
+
+.method public f()I
+   .limit stack 8
+   .limit locals 5
+   aload_0
+   getfield stack_var11/arr [I
+   iconst_0
+   iaload ;; put arr[0] on stack (currently 0)
+   aload_0
+   getfield stack_var11/arr [I
+   iconst_0
+   iconst_1
+   iastore ;; store 1 in arr[0],
+           ;; value on stack should not be touched
+   ireturn
+.end method

regression/cbmc-java/stack_var2/README

@@ -0,0 +1,9 @@
+This regression test is created from the .j file with the jasmin assembler.
+https://github.com/Sable/jasmin
+
+On Ubuntu, it is available as jasmin-sable. To convert a .j file, it is
+sufficient to do
+
+> jasmin $FILE.j
+
+and it will create the corresponding $FILE.class file.

regression/cbmc-java/stack_var2/stack_test.java

@@ -0,0 +1,7 @@
+public class stack_test {
+  public static void main(String[] args) {
+    stack_var2 s = new stack_var2();
+    int n = s.f(1);
+    assert(n==0);
+  }
+}

regression/cbmc-java/stack_var2/stack_var2.j

@@ -0,0 +1,25 @@
+.class public stack_var2
+.super java/lang/Object
+
+.method public <init>()V
+   aload_0
+   invokenonvirtual java/lang/Object/<init>()V
+   return
+.end method
+
+.method public f(I)I
+   .limit stack 3
+   .limit locals 2
+
+   ;; push local var1
+   iload_1
+   ;; duplicate
+   dup
+   ;; increment local var1
+   iinc 1 1
+   ;; push local var1
+   iload_1
+   isub
+   ;; incremented copy on stack
+   ireturn
+.end method

regression/cbmc-java/stack_var2/test.desc

@@ -0,0 +1,9 @@
+CORE
+stack_test.class
+
+^EXIT=10$
+^SIGNAL=0$
+^.*assertion at file stack_test.java line 5 function.*: FAILURE$
+^VERIFICATION FAILED$
+--
+^warning: ignoring

regression/cbmc-java/stack_var3/README

@@ -0,0 +1,9 @@
+This regression test is created from the .j file with the jasmin assembler.
+https://github.com/Sable/jasmin
+
+On Ubuntu, it is available as jasmin-sable. To convert a .j file, it is
+sufficient to do
+
+> jasmin $FILE.j
+
+and it will create the corresponding $FILE.class file.

regression/cbmc-java/stack_var3/stack_test.java

@@ -0,0 +1,7 @@
+public class stack_test {
+  public static void main(String[] args) {
+    stack_var3 s = new stack_var3();
+    int n = s.f();
+    assert(n==0);
+  }
+}

regression/cbmc-java/stack_var3/stack_var3.j

@@ -0,0 +1,33 @@
+.class public stack_var3
+.super java/lang/Object
+
+.method public <init>()V
+   aload_0
+   invokenonvirtual java/lang/Object/<init>()V
+   return
+.end method
+
+.method public f()I
+   .limit stack 5
+   .limit locals 3
+
+   ;; 1->var1
+   ;; 0->var2
+   iconst_1
+   istore_1
+   iconst_0
+   istore_2
+   ;; push local var2 / var1
+   iload_2
+   iload_1
+   ;; dup var1
+   dup_x1
+   ;; sub one from var1
+   iinc 1 -1
+   ;; pop first var1
+   pop
+   ;; sub
+   isub
+   ;; incremented copy on stack
+   ireturn
+.end method

regression/cbmc-java/stack_var3/test.desc

@@ -0,0 +1,9 @@
+CORE
+stack_test.class
+
+^EXIT=10$
+^SIGNAL=0$
+^.*assertion at file stack_test.java line 5 function.*: FAILURE$
+^VERIFICATION FAILED$
+--
+^warning: ignoring

regression/cbmc-java/stack_var4/README

@@ -0,0 +1,9 @@
+This regression test is created from the .j file with the jasmin assembler.
+https://github.com/Sable/jasmin
+
+On Ubuntu, it is available as jasmin-sable. To convert a .j file, it is
+sufficient to do
+
+> jasmin $FILE.j
+
+and it will create the corresponding $FILE.class file.

regression/cbmc-java/stack_var4/stack_test.java

@@ -0,0 +1,7 @@
+public class stack_test {
+  public static void main(String[] args) {
+    stack_var4 s = new stack_var4();
+    int n = s.f();
+    assert(n==0);
+  }
+}