Do not (unnecessarily) require preprocessing for fixed 32/64 bit regression tests
This is not portable as some architectures might not provide header files for non-native bit widths. Preprocessing/the use of header files is not essential for any of these regression tests.
This commit is contained in:
parent
0d7a9437c6
commit
0a990efb9b
|
@ -101,7 +101,6 @@ jobs:
|
|||
- g++-5
|
||||
- libubsan0
|
||||
- parallel
|
||||
- libc6-dev-i386
|
||||
before_install:
|
||||
- mkdir bin
|
||||
- ln -s /usr/bin/gcc-5 bin/gcc
|
||||
|
@ -136,7 +135,6 @@ jobs:
|
|||
- libwww-perl
|
||||
- g++-5
|
||||
- libubsan0
|
||||
- libc6-dev-i386
|
||||
before_install:
|
||||
- mkdir bin
|
||||
- ln -s /usr/bin/gcc-5 bin/gcc
|
||||
|
@ -165,7 +163,6 @@ jobs:
|
|||
- libstdc++-5-dev
|
||||
- libubsan0
|
||||
- parallel
|
||||
- libc6-dev-i386
|
||||
before_install:
|
||||
- mkdir bin
|
||||
- ln -s /usr/bin/gcc-5 bin/gcc
|
||||
|
@ -194,7 +191,6 @@ jobs:
|
|||
- g++-5
|
||||
- libstdc++-5-dev
|
||||
- libubsan0
|
||||
- libc6-dev-i386
|
||||
before_install:
|
||||
- mkdir bin
|
||||
- ln -s /usr/bin/gcc-5 bin/gcc
|
||||
|
@ -220,7 +216,6 @@ jobs:
|
|||
- ubuntu-toolchain-r-test
|
||||
packages:
|
||||
- g++-5
|
||||
- libc6-dev-i386
|
||||
before_install:
|
||||
- mkdir bin
|
||||
- ln -s /usr/bin/gcc-5 bin/gcc
|
||||
|
@ -245,7 +240,6 @@ jobs:
|
|||
- ubuntu-toolchain-r-test
|
||||
packages:
|
||||
- g++-7
|
||||
- libc6-dev-i386
|
||||
before_install:
|
||||
- mkdir bin
|
||||
- ln -s /usr/bin/gcc-7 bin/gcc
|
||||
|
@ -276,7 +270,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
|
||||
|
|
|
@ -1,5 +1,5 @@
|
|||
CORE
|
||||
main.c
|
||||
main.i
|
||||
--win32 --xml-ui
|
||||
^EXIT=10$
|
||||
^SIGNAL=0$
|
||||
|
|
|
@ -1,5 +1,5 @@
|
|||
CORE
|
||||
main.c
|
||||
main.i
|
||||
--32
|
||||
^EXIT=0$
|
||||
^SIGNAL=0$
|
||||
|
|
|
@ -1,5 +1,5 @@
|
|||
CORE
|
||||
main.c
|
||||
main.i
|
||||
--32
|
||||
^EXIT=0$
|
||||
^SIGNAL=0$
|
||||
|
|
|
@ -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;
|
|
@ -1,5 +1,5 @@
|
|||
CORE
|
||||
main.c
|
||||
main.i
|
||||
--32 --little-endian
|
||||
^EXIT=0$
|
||||
^SIGNAL=0$
|
||||
|
|
|
@ -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;
|
||||
}
|
|
@ -1,5 +1,5 @@
|
|||
CORE
|
||||
main.c
|
||||
main.i
|
||||
--32
|
||||
^EXIT=0$
|
||||
^SIGNAL=0$
|
||||
|
|
|
@ -6,19 +6,14 @@ typedef union
|
|||
int b;
|
||||
} Union;
|
||||
|
||||
#ifdef __GNUC__
|
||||
typedef struct
|
||||
{
|
||||
int Count;
|
||||
Union List[1];
|
||||
} __attribute__((packed)) Struct3;
|
||||
#else
|
||||
#pragma pack(push)
|
||||
#pragma pack(1)
|
||||
typedef struct
|
||||
{
|
||||
int Count;
|
||||
Union List[1];
|
||||
} Struct3;
|
||||
#endif
|
||||
#pragma pack(pop)
|
||||
|
||||
int main()
|
||||
{
|
|
@ -1,5 +1,5 @@
|
|||
CORE
|
||||
main.c
|
||||
main.i
|
||||
--bounds-check --32 --no-simplify
|
||||
^EXIT=10$
|
||||
^SIGNAL=0$
|
||||
|
|
|
@ -1,5 +1,5 @@
|
|||
CORE
|
||||
main.c
|
||||
main.i
|
||||
--bounds-check --32
|
||||
^EXIT=10$
|
||||
^SIGNAL=0$
|
||||
|
|
|
@ -1,5 +1,5 @@
|
|||
KNOWNBUG
|
||||
main.c
|
||||
main.i
|
||||
--bounds-check --32 --no-simplify
|
||||
^EXIT=0$
|
||||
^SIGNAL=0$
|
||||
|
|
|
@ -1,8 +1,3 @@
|
|||
#include <assert.h>
|
||||
|
||||
#define STATIC_ASSERT(condition) \
|
||||
int some_array##__LINE__[(condition) ? 1 : -1]
|
||||
|
||||
struct my_struct1
|
||||
{
|
||||
int i;
|
||||
|
@ -40,22 +35,22 @@ struct my_struct3 {
|
|||
int i;
|
||||
} xx3= { 1, 2 };
|
||||
|
||||
STATIC_ASSERT(sizeof(xx1)==4+1+3+4+4);
|
||||
STATIC_ASSERT(sizeof(xx2)==4+4+4+4);
|
||||
int some_array1[(sizeof(xx1)==4+1+3+4+4) ? 1 : -1];
|
||||
int some_array2[(sizeof(xx2)==4+4+4+4) ? 1 : -1];
|
||||
|
||||
int main()
|
||||
{
|
||||
assert(xx1.i==1);
|
||||
assert(xx1.ch==2);
|
||||
assert(xx1.j==3);
|
||||
__CPROVER_assert(xx1.i==1, "");
|
||||
__CPROVER_assert(xx1.ch==2, "");
|
||||
__CPROVER_assert(xx1.j==3, "");
|
||||
|
||||
// let's probe the padding
|
||||
char *p=&xx1.ch;
|
||||
assert(p[0]==2);
|
||||
assert(p[1]==0);
|
||||
assert(p[2]==0);
|
||||
assert(p[3]==0);
|
||||
__CPROVER_assert(p[0]==2, "");
|
||||
__CPROVER_assert(p[1]==0, "");
|
||||
__CPROVER_assert(p[2]==0, "");
|
||||
__CPROVER_assert(p[3]==0, "");
|
||||
|
||||
assert(xx3.bit_field==1);
|
||||
assert(xx3.i==2);
|
||||
__CPROVER_assert(xx3.bit_field==1, "");
|
||||
__CPROVER_assert(xx3.i==2, "");
|
||||
}
|
|
@ -1,5 +1,5 @@
|
|||
CORE
|
||||
main.c
|
||||
main.i
|
||||
--32
|
||||
^EXIT=0$
|
||||
^SIGNAL=0$
|
||||
|
|
|
@ -1,48 +0,0 @@
|
|||
int main()
|
||||
{
|
||||
// these types are Visual Studio-specific
|
||||
#ifdef _MSC_VER
|
||||
__int8 i1;
|
||||
__int16 i2;
|
||||
__int32 i3;
|
||||
__int64 i4;
|
||||
|
||||
assert(sizeof(i1)==1);
|
||||
assert(sizeof(i2)==2);
|
||||
assert(sizeof(i3)==4);
|
||||
assert(sizeof(i4)==8);
|
||||
#endif
|
||||
|
||||
// general types
|
||||
|
||||
char c;
|
||||
short s;
|
||||
int i;
|
||||
long l;
|
||||
long long ll;
|
||||
|
||||
assert(sizeof(c)==1);
|
||||
assert(sizeof(s)==2);
|
||||
assert(sizeof(i)==4);
|
||||
assert(sizeof(l)==4);
|
||||
assert(sizeof(ll)==8);
|
||||
|
||||
// these constants are Visual Studio-specific
|
||||
#ifdef _MSC_VER
|
||||
assert(sizeof(1i8)==1);
|
||||
assert(sizeof(1i16)==2);
|
||||
assert(sizeof(1i32)==4);
|
||||
assert(sizeof(1i64)==8);
|
||||
assert(sizeof(1i128)==16);
|
||||
|
||||
// oh, and these pointer qualifiers are Visual Studio-specific
|
||||
int * __ptr32 p32;
|
||||
//int * __ptr64 p64;
|
||||
|
||||
// requires --i386-win32 to work
|
||||
assert(sizeof(p32)==4);
|
||||
//assert(sizeof(p64)==8);
|
||||
#endif
|
||||
|
||||
assert(sizeof(void *)==4);
|
||||
}
|
|
@ -0,0 +1,44 @@
|
|||
int main()
|
||||
{
|
||||
// these types are Visual Studio-specific
|
||||
__int8 i1;
|
||||
__int16 i2;
|
||||
__int32 i3;
|
||||
__int64 i4;
|
||||
|
||||
__CPROVER_assert(sizeof(i1) == 1, "");
|
||||
__CPROVER_assert(sizeof(i2) == 2, "");
|
||||
__CPROVER_assert(sizeof(i3) == 4, "");
|
||||
__CPROVER_assert(sizeof(i4) == 8, "");
|
||||
|
||||
// general types
|
||||
|
||||
char c;
|
||||
short s;
|
||||
int i;
|
||||
long l;
|
||||
long long ll;
|
||||
|
||||
__CPROVER_assert(sizeof(c) == 1, "");
|
||||
__CPROVER_assert(sizeof(s) == 2, "");
|
||||
__CPROVER_assert(sizeof(i) == 4, "");
|
||||
__CPROVER_assert(sizeof(l) == 4, "");
|
||||
__CPROVER_assert(sizeof(ll) == 8, "");
|
||||
|
||||
// these constants are Visual Studio-specific
|
||||
__CPROVER_assert(sizeof(1i8) == 1, "");
|
||||
__CPROVER_assert(sizeof(1i16) == 2, "");
|
||||
__CPROVER_assert(sizeof(1i32) == 4, "");
|
||||
__CPROVER_assert(sizeof(1i64) == 8, "");
|
||||
__CPROVER_assert(sizeof(1i128) == 16, "");
|
||||
|
||||
// oh, and these pointer qualifiers are Visual Studio-specific
|
||||
int * __ptr32 p32;
|
||||
//int * __ptr64 p64;
|
||||
|
||||
// requires --i386-win32 to work
|
||||
__CPROVER_assert(sizeof(p32) == 4, "");
|
||||
//__CPROVER_assert(sizeof(p64) == 8, "");
|
||||
|
||||
__CPROVER_assert(sizeof(void *) == 4, "");
|
||||
}
|
|
@ -1,5 +1,5 @@
|
|||
CORE
|
||||
main.c
|
||||
main.i
|
||||
--i386-win32
|
||||
^EXIT=0$
|
||||
^SIGNAL=0$
|
||||
|
|
|
@ -1,25 +0,0 @@
|
|||
int main()
|
||||
{
|
||||
// general types
|
||||
short s;
|
||||
int i;
|
||||
long l;
|
||||
long long ll;
|
||||
|
||||
assert(sizeof(s)==2);
|
||||
assert(sizeof(i)==4);
|
||||
assert(sizeof(l)==4);
|
||||
assert(sizeof(ll)==8);
|
||||
|
||||
// oh, and these pointer qualifiers are MS-specific
|
||||
#ifdef _MSC_VER
|
||||
int * __ptr32 p32;
|
||||
int * __ptr64 p64;
|
||||
|
||||
// requires --winx64 to work
|
||||
assert(sizeof(p32)==4);
|
||||
assert(sizeof(p64)==8);
|
||||
#endif
|
||||
|
||||
assert(sizeof(void *)==8);
|
||||
}
|
|
@ -0,0 +1,23 @@
|
|||
int main()
|
||||
{
|
||||
// general types
|
||||
short s;
|
||||
int i;
|
||||
long l;
|
||||
long long ll;
|
||||
|
||||
__CPROVER_assert(sizeof(s) == 2, "");
|
||||
__CPROVER_assert(sizeof(i) == 4, "");
|
||||
__CPROVER_assert(sizeof(l) == 4, "");
|
||||
__CPROVER_assert(sizeof(ll) == 8, "");
|
||||
|
||||
// oh, and these pointer qualifiers are MS-specific
|
||||
int * __ptr32 p32;
|
||||
int * __ptr64 p64;
|
||||
|
||||
// requires --winx64 to work
|
||||
__CPROVER_assert(sizeof(p32) == 4, "");
|
||||
__CPROVER_assert(sizeof(p64) == 8, "");
|
||||
|
||||
__CPROVER_assert(sizeof(void *) == 8, "");
|
||||
}
|
|
@ -1,5 +1,5 @@
|
|||
CORE
|
||||
main.c
|
||||
main.i
|
||||
--winx64
|
||||
^EXIT=0$
|
||||
^SIGNAL=0$
|
||||
|
|
|
@ -1,5 +1,5 @@
|
|||
KNOWNBUG
|
||||
test.c
|
||||
test.i
|
||||
--32 --object-bits 31 --unwind 11 --no-simplify
|
||||
dynamic object too large
|
||||
--
|
||||
|
|
|
@ -1,5 +1,3 @@
|
|||
#include <assert.h>
|
||||
|
||||
void *malloc(__CPROVER_size_t);
|
||||
|
||||
int main(int argc, char** argv)
|
||||
|
@ -7,5 +5,5 @@ int main(int argc, char** argv)
|
|||
char* c=(char*)malloc(10);
|
||||
char* d=c;
|
||||
for(char i=0; i<10; i++, d++);
|
||||
assert((size_t)d==(size_t)c+10);
|
||||
__CPROVER_assert((__CPROVER_size_t)d == (__CPROVER_size_t)c + 10, "");
|
||||
}
|
|
@ -1,8 +1,6 @@
|
|||
// copy of Pointer_Arithmetic12
|
||||
|
||||
#include <stdint.h>
|
||||
|
||||
#include <assert.h>
|
||||
typedef unsigned int uint32_t;
|
||||
|
||||
uint32_t __stack[32];
|
||||
|
||||
|
@ -100,35 +98,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;
|
|
@ -1,5 +1,5 @@
|
|||
CORE
|
||||
main.c
|
||||
main.i
|
||||
--32 --little-endian --object-bits 25 --pointer-check
|
||||
^EXIT=10$
|
||||
^SIGNAL=0$
|
||||
|
|
Loading…
Reference in New Issue