Merge pull request #2529 from tautschnig/debian1

Do not (unnecessarily) require preprocessing for fixed 32/64 bit regression tests

Author: Daniel Kroening

.travis.yml

@@ -102,7 +102,6 @@ jobs:
             - g++-5
             - libubsan0
             - parallel
-            - libc6-dev-i386
       before_install:
         - mkdir bin
         - ln -s /usr/bin/gcc-5 bin/gcc
@@ -137,7 +136,6 @@ jobs:
             - libwww-perl
             - g++-5
             - libubsan0
-            - libc6-dev-i386
       before_install:
         - mkdir bin
         - ln -s /usr/bin/gcc-5 bin/gcc
@@ -166,7 +164,6 @@ jobs:
             - libstdc++-5-dev
             - libubsan0
             - parallel
-            - libc6-dev-i386
       before_install:
         - mkdir bin
         - ln -s /usr/bin/gcc-5 bin/gcc
@@ -195,7 +192,6 @@ jobs:
             - g++-5
             - libstdc++-5-dev
             - libubsan0
-            - libc6-dev-i386
       before_install:
         - mkdir bin
         - ln -s /usr/bin/gcc-5 bin/gcc
@@ -221,7 +217,6 @@ jobs:
             - ubuntu-toolchain-r-test
           packages:
             - g++-5
-            - libc6-dev-i386
       before_install:
         - mkdir bin
         - ln -s /usr/bin/gcc-5 bin/gcc
@@ -247,7 +242,6 @@ jobs:
             - ubuntu-toolchain-r-test
           packages:
             - g++-7
-            - libc6-dev-i386
       before_install:
         - mkdir bin
         - ln -s /usr/bin/gcc-7 bin/gcc
@@ -279,7 +273,6 @@ jobs:
             - libstdc++-5-dev
             - libubsan0
             - parallel
-            - libc6-dev-i386
       before_install:
         - mkdir bin
         # Use gcc/g++ 5 for tests, as Clang doesn't work yet

regression/cbmc/Float24/main.c renamed to regression/cbmc/Float24/main.i

@@ -1,5 +1,5 @@
 CORE
-main.c
+main.i
 --win32 --xml-ui
 ^EXIT=10$
 ^SIGNAL=0$

regression/cbmc/Float24/test.desc

@@ -1,5 +1,5 @@
 CORE
-main.c
+main.i
 --32
 ^EXIT=0$
 ^SIGNAL=0$

regression/cbmc/Malloc15/main.c renamed to regression/cbmc/Malloc15/main.i

@@ -1,5 +1,5 @@
 CORE
-main.c
+main.i
 --32
 ^EXIT=0$
 ^SIGNAL=0$

regression/cbmc/Malloc15/test.desc

@@ -1,6 +1,4 @@
-#include <stdint.h>
-
-#include <assert.h>
+typedef unsigned int uint32_t;
 
 uint32_t __stack[32];
 
@@ -98,35 +96,25 @@ int main()
   L_0x401_0: esp-=0x14;
   L_0x404_0: var15=ebp;
   L_0x404_1: var15-=0x4;
-#ifdef NONDET
-  L_0x404_2: *(uint32_t*)(var15)=nondet_uint();
-#else
   L_0x404_2: *(uint32_t*)(var15)=0xffffffff;
-#endif
   L_0x40b_0: var16=ebp;
   L_0x40b_1: var16-=0x4;
   L_0x40b_2: eax=*(uint32_t*)(var16);
   L_0x40e_0: *(uint32_t*)(esp)=eax;
   L_0x411_0: esp-=4; f__L_0x3c6_0(); esp+=4;
-#if 1
              uint32_t eax1=eax;
   C_0x3ff_0: ebp=esp;
   C_0x401_0: esp-=0x14;
   C_0x404_0: var15=ebp;
   C_0x404_1: var15-=0x4;
-#ifdef NONDET
-  C_0x404_2: *(uint32_t*)(var15)=nondet_uint();
-#else
   C_0x404_2: *(uint32_t*)(var15)=0xffffffff;
-#endif
   C_0x40b_0: var16=ebp;
   C_0x40b_1: var16-=0x4;
   C_0x40b_2: eax=*(uint32_t*)(var16);
   C_0x40e_0: *(uint32_t*)(esp)=eax;
   C_0x411_0: esp-=4; f__L_0x3c6_0(); esp+=4;
              uint32_t eax2=eax;
-             assert(eax2==eax1);
-#endif
+             __CPROVER_assert(eax2 == eax1, "");
   L_0x416_0: esp=ebp;
   L_0x416_1: ebp=*(uint32_t*)(esp);
   L_0x416_2: esp+=0x4;

regression/cbmc/Malloc16/main.c renamed to regression/cbmc/Malloc16/main.i

@@ -1,5 +1,5 @@
 CORE
-main.c
+main.i
 --32 --little-endian
 ^EXIT=0$
 ^SIGNAL=0$

regression/cbmc/Malloc16/test.desc

@@ -1,5 +1,3 @@
-#include <assert.h>
-
 int main()
 {
   int arrayOfIntegers[] = {1, 2, 3};
@@ -8,6 +6,6 @@ int main()
   int iFirst=(int)pointer2FirstElem;
   int iThird=(int)pointer2ThirdElem;
   int addrDiff = iThird-iFirst;
-  assert(addrDiff == 2* sizeof(int));
+  __CPROVER_assert(addrDiff == 2* sizeof(int), "");
   return 0;
 }