Merge pull request #93 from danpoe/function-nondet-structs

--function with nondet structs for Java

Author: peterschrammel

regression/cbmc-java/function1/Main.class

@@ -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();
+  }
+}
+

regression/cbmc-java/function1/Main.java

@@ -0,0 +1,8 @@
+CORE
+Main.class
+--function "java::Other.fail:()V"
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring

regression/cbmc-java/function1/Other.class

@@ -0,0 +1,34 @@
+
+class A
+{
+  public int i;
+}
+
+class B extends A
+{
+  public int j;
+}
+
+class C extends B
+{
+  public int k;
+}
+
+class D
+{
+  protected C c;
+
+  public void fail()
+  {
+    assert c.i == 0 || c.j == 0 || c.k == 0;
+  }
+}
+
+public class Main
+{
+  public static void main(String[] args)
+  {
+    D d = new D();
+  }
+}
+

regression/cbmc-java/function1/test.desc

@@ -0,0 +1,8 @@
+CORE
+Main.class
+--function "java::D.fail:()V"
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring

regression/cbmc-java/function2/A.class

@@ -0,0 +1,22 @@
+
+class A
+{
+  public void dummy() {}
+
+  public B b;
+}
+
+class B
+{
+  public A a;
+}
+
+
+public class Main
+{
+  public static void main(String[] args)
+  {
+    B B = new B();
+  }
+}
+

regression/cbmc-java/function2/B.class

@@ -0,0 +1,8 @@
+CORE
+Main.class
+--function "java::A.dummy:()V"
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring