From 1976bf69f2ce07f28854efa624165119f88addea Mon Sep 17 00:00:00 2001 From: kroening Date: Sun, 22 Jul 2012 21:45:59 +0000 Subject: [PATCH] moved regressions from CVS git-svn-id: svn+ssh://svn.cprover.org/srv/svn/cbmc/trunk@1336 6afb6bc1-c8e4-404c-8f48-9ae832c5b171 --- regression/cbmc/Array_Initialization1/main.c | 30 +++++++++++++ .../cbmc/Array_Initialization1/test.desc | 8 ++++ regression/cbmc/Array_Initialization2/main.c | 11 +++++ .../cbmc/Array_Initialization2/test.desc | 8 ++++ regression/cbmc/Array_Initialization3/main.c | 26 +++++++++++ .../cbmc/Array_Initialization3/test.desc | 8 ++++ regression/cbmc/Unwinding_Locality1/main.c | 17 ++++++++ regression/cbmc/Unwinding_Locality1/test.desc | 7 +++ regression/cbmc/Visual_Studio_Types1/main.c | 43 +++++++++++++++++++ .../cbmc/Visual_Studio_Types1/test.desc | 8 ++++ regression/cbmc/Visual_Studio_Types2/main.c | 22 ++++++++++ .../cbmc/Visual_Studio_Types2/test.desc | 8 ++++ regression/cbmc/__func__1/main.c | 18 ++++++++ regression/cbmc/__func__1/test.desc | 8 ++++ 14 files changed, 222 insertions(+) create mode 100644 regression/cbmc/Array_Initialization1/main.c create mode 100644 regression/cbmc/Array_Initialization1/test.desc create mode 100644 regression/cbmc/Array_Initialization2/main.c create mode 100644 regression/cbmc/Array_Initialization2/test.desc create mode 100644 regression/cbmc/Array_Initialization3/main.c create mode 100644 regression/cbmc/Array_Initialization3/test.desc create mode 100644 regression/cbmc/Unwinding_Locality1/main.c create mode 100644 regression/cbmc/Unwinding_Locality1/test.desc create mode 100644 regression/cbmc/Visual_Studio_Types1/main.c create mode 100644 regression/cbmc/Visual_Studio_Types1/test.desc create mode 100644 regression/cbmc/Visual_Studio_Types2/main.c create mode 100644 regression/cbmc/Visual_Studio_Types2/test.desc create mode 100644 regression/cbmc/__func__1/main.c create mode 100644 regression/cbmc/__func__1/test.desc diff --git a/regression/cbmc/Array_Initialization1/main.c b/regression/cbmc/Array_Initialization1/main.c new file mode 100644 index 0000000000..db867b00d9 --- /dev/null +++ b/regression/cbmc/Array_Initialization1/main.c @@ -0,0 +1,30 @@ +#include + +// do both orderings + +extern const char *abc1[]; +const char *abc1[] = {"Hallo", "Welt"}; + +const char *abc2[] = {"Hallo", "Welt"}; +extern const char *abc2[]; + +// modifiers + +static const char * const a1[] = { "abc" }; +static const char * const a2[] = { "abc", "" }; + +char string_array[1][1][5] = {"1234"}; + +int main() +{ + // both must be complete + sizeof(abc1); + sizeof(abc2); + + assert(string_array[0][0][0]=='1'); + assert(string_array[0][0][1]=='2'); + assert(string_array[0][0][2]=='3'); + assert(string_array[0][0][3]=='4'); + assert(string_array[0][0][4]==0); +} + diff --git a/regression/cbmc/Array_Initialization1/test.desc b/regression/cbmc/Array_Initialization1/test.desc new file mode 100644 index 0000000000..9efefbc736 --- /dev/null +++ b/regression/cbmc/Array_Initialization1/test.desc @@ -0,0 +1,8 @@ +CORE +main.c + +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/regression/cbmc/Array_Initialization2/main.c b/regression/cbmc/Array_Initialization2/main.c new file mode 100644 index 0000000000..64706b67e2 --- /dev/null +++ b/regression/cbmc/Array_Initialization2/main.c @@ -0,0 +1,11 @@ +int nondet_int(); + +int arr[2] = {0,0}; + +int main() +{ + unsigned place = nondet_int(); + __CPROVER_assume(place<2); + assert(arr[place]==0); + return 0; +} diff --git a/regression/cbmc/Array_Initialization2/test.desc b/regression/cbmc/Array_Initialization2/test.desc new file mode 100644 index 0000000000..9efefbc736 --- /dev/null +++ b/regression/cbmc/Array_Initialization2/test.desc @@ -0,0 +1,8 @@ +CORE +main.c + +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/regression/cbmc/Array_Initialization3/main.c b/regression/cbmc/Array_Initialization3/main.c new file mode 100644 index 0000000000..99bad4546f --- /dev/null +++ b/regression/cbmc/Array_Initialization3/main.c @@ -0,0 +1,26 @@ +#include + +int array1[2][2] = { + {1, 2}, + {3, 4} +}; + +int array2[]={ [1]=10, [2]=20, [3]=30, [10]=100 }; + +extern int array3[8]; +int array3[]={ 1, 2, 3, 4, 5, 6, 7, 8 }; + +int main(void) +{ + assert(array1[0][1] ==2); + assert(array1[1][0] ==3); // returned false in this case + + assert(array2[0]==0); + assert(array2[1]==10); + assert(array2[10]==100); + assert(sizeof(array2)==sizeof(int)*11); + + assert(sizeof(array3)==sizeof(int)*8); + + return 0; +} diff --git a/regression/cbmc/Array_Initialization3/test.desc b/regression/cbmc/Array_Initialization3/test.desc new file mode 100644 index 0000000000..9efefbc736 --- /dev/null +++ b/regression/cbmc/Array_Initialization3/test.desc @@ -0,0 +1,8 @@ +CORE +main.c + +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/regression/cbmc/Unwinding_Locality1/main.c b/regression/cbmc/Unwinding_Locality1/main.c new file mode 100644 index 0000000000..91ac505729 --- /dev/null +++ b/regression/cbmc/Unwinding_Locality1/main.c @@ -0,0 +1,17 @@ +int main() { + int i; + + for(i=0; i<10; i++) { + const int a=i; + } + + int array[10]; + for(i=0; i<10; i++) + { + const int a; + array[i]=a; + } + + // these should all be allowed to be different + assert(array[0]==array[1]); +} diff --git a/regression/cbmc/Unwinding_Locality1/test.desc b/regression/cbmc/Unwinding_Locality1/test.desc new file mode 100644 index 0000000000..33900ad2b7 --- /dev/null +++ b/regression/cbmc/Unwinding_Locality1/test.desc @@ -0,0 +1,7 @@ +CORE +main.c + +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- diff --git a/regression/cbmc/Visual_Studio_Types1/main.c b/regression/cbmc/Visual_Studio_Types1/main.c new file mode 100644 index 0000000000..27784ccd2a --- /dev/null +++ b/regression/cbmc/Visual_Studio_Types1/main.c @@ -0,0 +1,43 @@ +int main() +{ + // these types are MS-specific + __int8 i1; + __int16 i2; + __int32 i3; + __int64 i4; + + assert(sizeof(i1)==1); + assert(sizeof(i2)==2); + assert(sizeof(i3)==4); + assert(sizeof(i4)==8); + + // 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 MS-specific + 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 MS-specific + int * __ptr32 p32; + //int * __ptr64 p64; + + // requires --i386-win32 to work + assert(sizeof(p32)==4); + //assert(sizeof(p64)==8); + assert(sizeof(void *)==4); +} diff --git a/regression/cbmc/Visual_Studio_Types1/test.desc b/regression/cbmc/Visual_Studio_Types1/test.desc new file mode 100644 index 0000000000..e59b02c324 --- /dev/null +++ b/regression/cbmc/Visual_Studio_Types1/test.desc @@ -0,0 +1,8 @@ +CORE +main.c +--i386-win32 +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/regression/cbmc/Visual_Studio_Types2/main.c b/regression/cbmc/Visual_Studio_Types2/main.c new file mode 100644 index 0000000000..ef48ae5d30 --- /dev/null +++ b/regression/cbmc/Visual_Studio_Types2/main.c @@ -0,0 +1,22 @@ +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 + int * __ptr32 p32; + int * __ptr64 p64; + + // requires --winx64 to work + assert(sizeof(p32)==4); + assert(sizeof(p64)==8); + assert(sizeof(void *)==8); +} diff --git a/regression/cbmc/Visual_Studio_Types2/test.desc b/regression/cbmc/Visual_Studio_Types2/test.desc new file mode 100644 index 0000000000..7ce542782a --- /dev/null +++ b/regression/cbmc/Visual_Studio_Types2/test.desc @@ -0,0 +1,8 @@ +CORE +main.c +--winx64 +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/regression/cbmc/__func__1/main.c b/regression/cbmc/__func__1/main.c new file mode 100644 index 0000000000..93870e6aba --- /dev/null +++ b/regression/cbmc/__func__1/main.c @@ -0,0 +1,18 @@ +int main() +{ + char ch0, ch1, ch2, ch3, ch4; + + ch0=__func__[0]; + ch1=__func__[1]; + ch2=__func__[2]; + ch3=__func__[3]; + ch4=__func__[4]; + + assert(ch0=='m'); + assert(ch1=='a'); + assert(ch2=='i'); + assert(ch3=='n'); + assert(ch4==0); + + return 0; +} diff --git a/regression/cbmc/__func__1/test.desc b/regression/cbmc/__func__1/test.desc new file mode 100644 index 0000000000..9efefbc736 --- /dev/null +++ b/regression/cbmc/__func__1/test.desc @@ -0,0 +1,8 @@ +CORE +main.c + +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring