Add array-refinement regression tests

Moving these tests from a dedicated folder to cbmc to run them, also
making use of all three configurations that the cbmc folder is being
tested with. (Unnecessary) GCC attributes were removed to make sure
tests can be used on all platforms.

Author: tautschnig

regression/array-refinement/Makefile

@@ -1,4 +1,4 @@
-extern void __VERIFIER_error() __attribute__ ((__noreturn__));
+extern void __VERIFIER_error();
 
 int __VERIFIER_nondet_int();
 

…ession/array-refinement/Array_UF1/main.c regression/cbmc/Array_UF1/main.cregression/array-refinement/Array_UF1/main.c renamed to regression/cbmc/Array_UF1/main.c regression/array-refinement/Array_UF1/main.c renamed to regression/cbmc/Array_UF1/main.c

@@ -1,4 +1,4 @@
-extern void __VERIFIER_error() __attribute__ ((__noreturn__));
+extern void __VERIFIER_error();
 
 void __VERIFIER_assert(int cond) {
   if (!(cond)) {

…ion/array-refinement/Array_UF1/test.desc regression/cbmc/Array_UF1/test.descregression/array-refinement/Array_UF1/test.desc renamed to regression/cbmc/Array_UF1/test.desc regression/array-refinement/Array_UF1/test.desc renamed to regression/cbmc/Array_UF1/test.desc

@@ -1,4 +1,4 @@
-extern void __VERIFIER_error() __attribute__ ((__noreturn__));
+extern void __VERIFIER_error();
 
 void __VERIFIER_assert(int cond) {
   if (!(cond)) {

…ssion/array-refinement/Array_UF10/main.c regression/cbmc/Array_UF10/main.cregression/array-refinement/Array_UF10/main.c renamed to regression/cbmc/Array_UF10/main.c regression/array-refinement/Array_UF10/main.c renamed to regression/cbmc/Array_UF10/main.c

@@ -1,4 +1,4 @@
-extern void __VERIFIER_error() __attribute__ ((__noreturn__));
+extern void __VERIFIER_error();
 
 void __VERIFIER_assert(int cond) {
   if (!(cond)) {