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

@@ -0,0 +1,30 @@
+#include <assert.h>
+
+// 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);
+}
+

regression/cbmc/Array_Initialization1/test.desc

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

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;
+}

regression/cbmc/Array_Initialization2/test.desc

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

regression/cbmc/Array_Initialization3/main.c

@@ -0,0 +1,26 @@
+#include <assert.h>
+
+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;
+}

regression/cbmc/Array_Initialization3/test.desc

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

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]);
+}

regression/cbmc/Unwinding_Locality1/test.desc

@@ -0,0 +1,7 @@
+CORE
+main.c
+
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--

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);
+}

regression/cbmc/Visual_Studio_Types1/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--i386-win32
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

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);
+}

regression/cbmc/Visual_Studio_Types2/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--winx64
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

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;
+}

regression/cbmc/__func__1/test.desc

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