Merge pull request #631 from peterschrammel/update-from-master

Update test-gen-support from master

Author: peterschrammel

.travis.yml

@@ -1,10 +1,35 @@
 language: cpp
 
-sudo: false
-
 matrix:
   include:
+
+    # Alpine Linux with musl-libc using g++
+    - os: linux
+      sudo: required
+      compiler: gcc
+      services:
+        - docker
+      before_install:
+        - docker pull diffblue/cbmc-builder:alpine
+      env:
+        - PRE_COMMAND="docker run -v ${TRAVIS_BUILD_DIR}:/cbmc diffblue/cbmc-builder:alpine"
+        - COMPILER=g++
+
+    # OS X using g++
+    - os: osx
+      sudo: false
+      compiler: gcc
+      env: COMPILER=g++
+
+    # OS X using clang++
+    - os: osx
+      sudo: false
+      compiler: clang
+      env: COMPILER=clang++
+
+    # Ubuntu Linux with glibc using g++-5
     - os: linux
+      sudo: false
       compiler: gcc
       addons:
         apt:
@@ -18,7 +43,10 @@ matrix:
         - mkdir bin ; ln -s /usr/bin/gcc-5 bin/gcc
       # env: COMPILER=g++-5 SAN_FLAGS="-fsanitize=undefined -fno-sanitize-recover -fno-omit-frame-pointer"
       env: COMPILER=g++-5
+
+    # Ubuntu Linux with glibc using clang++-3.7
     - os: linux
+      sudo: false
       compiler: clang
       addons:
         apt:
@@ -34,18 +62,17 @@ matrix:
         - mkdir bin ; ln -s /usr/bin/clang-3.7 bin/gcc
       # env: COMPILER=clang++-3.7 SAN_FLAGS="-fsanitize=undefined -fno-sanitize-recover=undefined,integer -fno-omit-frame-pointer"
       env: COMPILER=clang++-3.7
-    - os: osx
-      compiler: gcc
-      env: COMPILER=g++
-    - os: osx
-      compiler: clang
-      env: COMPILER=clang++
+
     - env: NAME="CPP-LINT"
       script: scripts/travis_lint.sh || true
 
 script:
   - if [ -L bin/gcc ] ; then export PATH=$PWD/bin:$PATH ; fi ;
-    make -C src minisat2-download &&
-    make -C src CXX=$COMPILER CXXFLAGS="-Wall -O2 -g -Werror -Wno-deprecated-register -pedantic -Wno-sign-compare" -j2 &&
-    env UBSAN_OPTIONS=print_stacktrace=1 make -C regression test &&
-    make -C src CXX=$COMPILER CXXFLAGS=$FLAGS -j2 cegis.dir clobber.dir memory-models.dir musketeer.dir
+    COMMAND="make -C src minisat2-download" &&
+    eval ${PRE_COMMAND} ${COMMAND} &&
+    COMMAND="make -C src CXX=$COMPILER CXXFLAGS=\"-Wall -O2 -g -Werror -Wno-deprecated-register -pedantic -Wno-sign-compare\" -j2" &&
+    eval ${PRE_COMMAND} ${COMMAND} &&
+    COMMAND="env UBSAN_OPTIONS=print_stacktrace=1 make -C regression test" &&
+    eval ${PRE_COMMAND} ${COMMAND} &&
+    COMMAND="make -C src CXX=$COMPILER CXXFLAGS=$FLAGS -j2 cegis.dir clobber.dir memory-models.dir musketeer.dir" &&
+    eval ${PRE_COMMAND} ${COMMAND}

COMPILING

@@ -48,8 +48,6 @@ We assume that you have a Debian/Ubuntu or Red Hat-like distribution.
 
    cd cbmc-git/src
    make minisat2-download
-   make libzip-download zlib-download
-   make libzip-build
    make
 
 
@@ -126,8 +124,6 @@ Follow these instructions:
 
    cd cbmc-git/src
    make minisat2-download
-   make libzip-download zlib-download
-   make libzip-build
    make
 
 

regression/cbmc-java/NullPointer3/NullPointer3.class

@@ -4,5 +4,4 @@ public static void main(String[] args)
   {
     throw null; // NULL pointer dereference
   }
-
 }

regression/cbmc-java/NullPointer3/NullPointer3.java

@@ -1,9 +1,9 @@
 CORE
 NullPointer3.class
---pointer-check --stop-on-fail
+--pointer-check
 ^EXIT=10$
 ^SIGNAL=0$
-^  file NullPointer3.java line 5 function java::NullPointer3.main:\(\[Ljava/lang/String;\)V bytecode_index 1$
+^.*Throw null: FAILURE$
 ^VERIFICATION FAILED$
 --
 ^warning: ignoring

regression/cbmc-java/NullPointer3/test.desc

@@ -0,0 +1,10 @@
+CORE
+test.class
+
+^EXIT=10$
+^SIGNAL=0$
+^.*assertion at file test.java line 26 function.*: FAILURE$
+\*\* 1 of 9 failed \(2 iterations\)$
+^VERIFICATION FAILED$
+--
+^warning: ignoring

regression/cbmc-java/exceptions1/A.class

@@ -0,0 +1,30 @@
+class A extends Throwable {}
+class B extends A {}
+class C extends B {}
+class D extends C {}
+
+public class test {
+ public static void main (String arg[]) {
+   try {
+     D d = new D();
+     C c = new C();
+     B b = new B();
+     A a = new A();
+     A e = a;
+     throw e;
+   }
+   catch(D exc) {
+     assert false;
+   }
+   catch(C exc) {
+     assert false;
+   }
+   catch(B exc) {
+     assert false;
+   }
+   catch(A exc) {
+     assert false;
+   }  
+ }
+}
+

regression/cbmc-java/exceptions1/B.class

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

regression/cbmc-java/exceptions1/C.class

@@ -0,0 +1,25 @@
+class A extends RuntimeException {}
+class B extends A {}
+class C extends B {}
+
+public class test {
+  static void foo() {
+    try {
+      A b = new A();
+      throw b;
+    }
+    catch(A exc) {
+      assert false;
+    }
+  }
+  
+  public static void main (String args[]) {
+    try {
+      A a = new A();
+      foo();
+    }
+    catch(B exc) {
+      assert false;
+    }
+  }
+}

regression/cbmc-java/exceptions1/D.class

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

regression/cbmc-java/exceptions1/test.class

@@ -0,0 +1,39 @@
+class A extends RuntimeException {
+  int i=1;
+};
+
+class B extends A {
+};
+
+public class test {
+  static int foo(int k) {
+    try {
+      if(k==0)
+      {
+	A a = new A();
+	throw a;
+      }
+      else
+      {
+	A b = new A();
+	throw b;
+      }
+	
+    }
+    catch(B exc) {
+      assert exc.i==1;
+    }
+    return 1;
+  }
+
+  
+  public static void main (String args[]) {
+    try {
+      A a = new A();
+      foo(6);
+    }
+    catch(A exc) {
+      assert exc.i==2;
+    }
+  }
+}

regression/cbmc-java/exceptions1/test.desc

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

regression/cbmc-java/exceptions1/test.java

@@ -0,0 +1,27 @@
+class A extends RuntimeException {}
+class B extends A {}
+class C extends B {}
+
+class F {
+  void foo() {
+    try {
+      B b = new B();
+      throw b;
+    }
+    catch(B exc) {
+      assert false;
+    }
+  }
+}
+
+public class test {
+  public static void main (String args[]) {
+    try {
+      F f = new F();
+      f.foo();
+    }
+    catch(B exc) {
+      assert false;
+    }
+  }
+}

regression/cbmc-java/exceptions10/A.class

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

regression/cbmc-java/exceptions10/B.class

@@ -0,0 +1,28 @@
+class A extends RuntimeException {}
+class B extends A {}
+class C extends B {}
+
+class F {
+  void foo() {
+    try {
+      B b = new B();
+      throw b;
+    }
+    catch(B exc) {
+      throw exc;
+    }
+  }
+}
+
+public class test {
+ 
+  public static void main (String args[]) {
+    try {
+      F f = new F();
+      f.foo();
+    }
+    catch(B exc) {
+      assert false;
+    }
+  }
+}

regression/cbmc-java/exceptions10/C.class

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

regression/cbmc-java/exceptions10/test.class

@@ -0,0 +1,24 @@
+class A extends RuntimeException {}
+class B extends A {}
+class C extends B {}
+
+public class test {
+  public static void main (String args[]) {
+    try {
+      try {
+	C c = new C();
+	A a = new A();
+      }
+      catch(C exc) {
+	assert false;
+      }
+      catch(B exc) {
+	assert false;
+      }
+    }
+    catch(A exc) {
+      assert false;
+    }
+
+  }
+}

regression/cbmc-java/exceptions10/test.desc

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

regression/cbmc-java/exceptions10/test.java

@@ -0,0 +1,20 @@
+class InetAddress {}
+class InetSocketAddress {}
+
+public class test {
+  public String lookupPtrRecord(InetAddress address) {
+    return "Foo";
+  }
+
+  public InetAddress reverse(InetAddress address) {
+    return address;
+  }
+
+  public void translate(InetAddress address, int i) {
+    try {
+      String domainName = lookupPtrRecord(reverse(address));
+    } catch (Exception e) {
+      assert false;
+    }
+  }
+}

regression/cbmc-java/exceptions11/A.class

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