Merge pull request #660 from peterschrammel/pull-from-master

Update test-gen-support from master

Author: forejtv

.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

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
 
@@ -57,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
 
@@ -83,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:
 

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.class

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

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

regression/cbmc-java/classtest1/test.desc

@@ -5,8 +5,8 @@ main.c
 ^SIGNAL=0$
 pointer outside dynamic object bounds in \*p: FAILURE
 pointer outside dynamic object bounds in \*p: FAILURE
-pointer outside dynamic object bounds in p2\[\(signed long int\)1\]: FAILURE
-pointer outside dynamic object bounds in p2\[\(signed long int\)0\]: FAILURE
+pointer outside dynamic object bounds in p2\[.*1\]: FAILURE
+pointer outside dynamic object bounds in p2\[.*0\]: FAILURE
 \*\* 4 of 36 failed \(3 iterations\)
 --
 ^warning: ignoring

regression/cbmc/Malloc23/test.desc

@@ -6,7 +6,7 @@ int main(int argc, char** argv) {
   if(argc != 2)
     return 0;
 
-  unsigned long x[argc];
+  unsigned long long x[argc];
   x[0]=0x0102030405060708;
   x[1]=0x1112131415161718;
 

regression/cbmc/byte_update2/main.c

@@ -13,7 +13,7 @@ int main(int argc, char** argv) {
   x[3]=0x0708;
   x[4]=0x090a;
 
-  unsigned long* alias=(unsigned long*)(((char*)x)+0);
+  unsigned long long* alias=(unsigned long long*)(((char*)x)+0);
   *alias=0xf1f2f3f4f5f6f7f8;
 
   unsigned char* alias2=(unsigned char*)x;

regression/cbmc/byte_update3/main.c

@@ -18,7 +18,7 @@ int main(int argc, char** argv) {
   x[8]=0x09;
   x[9]=0x0a;
 
-  unsigned long* alias=(unsigned long*)(((char*)x)+1);
+  unsigned long long* alias=(unsigned long long*)(((char*)x)+1);
   *alias=0xf1f2f3f4f5f6f7f8;
 
   unsigned char* alias2=(unsigned char*)x;