Merge master into Security scanner support

.gitignore

@@ -1,5 +1,16 @@
 # Local files generated by IDEs
+.vs/*
 .vscode/*
+~AutoRecover.*
+*.sln
+*.vcxproj*
+scripts/__pycache__/*
+src/goto-analyzer/taint_driver_scripts/.idea/*
+/*.config
+/*.creator
+/*.creator.user
+/*.files
+/*.includes
 
 # compilation files
 *.lo

.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:
@@ -20,7 +45,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:
@@ -38,18 +66,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

@@ -10,10 +10,10 @@ environments:
 
 - Solaris 11
 
-- FreeBSD 10 or 11
+- FreeBSD 11
 
 - Cygwin
-  (We recommend the i686-pc-mingw32-g++ cross compiler, version 4.7 or above.)
+  (We recommend the i686-pc-mingw32-g++ cross compiler, version 5.4 or above.)
 
 - Microsoft's Visual Studio version 12 (2013), version 14 (2015),
   or version 15 (older versions won't work)
@@ -29,16 +29,16 @@ COMPILATION ON LINUX
 We assume that you have a Debian/Ubuntu or Red Hat-like distribution.
 
 0) You need a C/C++ compiler, Flex and Bison, and GNU make.
-   The GNU Make needs to be version 3.81 or higher. On Debian-like
-   distributions, do
+   The GNU Make needs to be version 3.81 or higher.
+   On Debian-like distributions, do
 
-   apt-get install g++ gcc flex bison make git libz-dev libwww-perl patch libzip-dev
+   apt-get install g++-6 gcc flex bison make git libwww-perl patch
 
    On Red Hat/Fedora or derivates, do
 
    yum install gcc gcc-c++ flex bison perl-libwww-perl patch
 
-   Note that you need g++ version 4.9 or newer.
+   Note that you need g++ version 5.2 or newer.
 
 1) As a user, get the CBMC source via
 
@@ -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
 
 
@@ -59,7 +57,7 @@ COMPILATION ON SOLARIS 11
 1) As root, get the necessary development tools:
 
    pkg install system/header developer/lexer/flex developer/parser/bison developer/versioning/git
-   pkg install --accept developer/gcc-49
+   pkg install --accept developer/gcc-5
 
 2) As a user, get the CBMC source via
 
@@ -85,8 +83,8 @@ COMPILATION ON SOLARIS 11
    It will mis-optimize MiniSat2.
 
 
-COMPILATION ON FREEBSD 10/11
-----------------------------
+COMPILATION ON FREEBSD 11
+-------------------------
 
 1) As root, get the necessary tools:
 
@@ -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.java

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

regression/cbmc-java/NullPointer3/test.desc

@@ -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/VarLengthArrayTrace1/test.desc

@@ -3,7 +3,7 @@ VarLengthArrayTrace1.class
 --trace
 ^EXIT=10$
 ^SIGNAL=0$
-dynamic_3_array\[1l\]=10
+dynamic_3_array\[1.*\]=10
 --
 ^warning: ignoring
 assignment removed

regression/cbmc-java/classtest1/classtest1.java

@@ -0,0 +1,11 @@
+public class classtest1
+{
+  static void main(String[] args)
+  {
+    g(classtest1.class);
+  }
+  static void g(Object c)
+  {
+    assert true;
+  }
+}

regression/cbmc-java/classtest1/test.desc

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

regression/cbmc-java/exceptions1/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/test.java

@@ -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/exceptions10/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/exceptions10/test.java

@@ -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/exceptions11/test.desc

@@ -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/exceptions11/test.java

@@ -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/exceptions12/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/exceptions12/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/exceptions13/test.desc

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