diff --git a/doc/assets/xml_spec.xsd b/doc/assets/xml_spec.xsd
index 40f7c078ea4..ba251ee4e29 100644
--- a/doc/assets/xml_spec.xsd
+++ b/doc/assets/xml_spec.xsd
@@ -181,6 +181,8 @@
+
+
@@ -190,6 +192,7 @@
+
diff --git a/regression/array-refinement/Array_UF1/main.c b/regression/array-refinement/Array_UF1/main.c
deleted file mode 100644
index 27c5f15cbd8..00000000000
--- a/regression/array-refinement/Array_UF1/main.c
+++ /dev/null
@@ -1,13 +0,0 @@
-int main()
-{
- int a[10], b[10];
- int x,y,z;
- __CPROVER_assume(2<=y && y<=4);
- __CPROVER_assume(6<=z && z<=8);
- b[y] = x;
- b[z] = x;
- for(unsigned i = 0;i<10;i++) {
- a[i] = b[i];
- }
- __CPROVER_assert(a[y]==a[z], "a[y]==a[z]");
-}
diff --git a/regression/array-refinement/Array_UF10/main.c b/regression/array-refinement/Array_UF10/main.c
deleted file mode 100644
index 935392f577c..00000000000
--- a/regression/array-refinement/Array_UF10/main.c
+++ /dev/null
@@ -1,21 +0,0 @@
-extern void __VERIFIER_error() __attribute__ ((__noreturn__));
-
-int __VERIFIER_nondet_int();
-
- char x[100], y[100];
- int i,j,k;
-
-void main() {
- k = __VERIFIER_nondet_int();
-
- i = 0;
- while(x[i] != 0){
- y[i] = x[i];
- i++;
- }
- y[i] = 0;
-
- if(k >= 0 && k < i)
- if(y[k] == 0)
- {ERROR: __VERIFIER_error();}
-}
diff --git a/regression/array-refinement/Array_UF11/main.c b/regression/array-refinement/Array_UF11/main.c
deleted file mode 100644
index f4a3234cf70..00000000000
--- a/regression/array-refinement/Array_UF11/main.c
+++ /dev/null
@@ -1,32 +0,0 @@
-extern void __VERIFIER_error() __attribute__ ((__noreturn__));
-
-void __VERIFIER_assert(int cond) {
- if (!(cond)) {
- ERROR: __VERIFIER_error();
- }
- return;
-}
-
-_Bool __VERIFIER_nondet_bool();
-
-int main(){
- int a[5];
- int len=0;
- _Bool c=__VERIFIER_nondet_bool();
- int i;
-
-
- while(c){
-
- if (len==4)
- len =0;
-
- a[len]=0;
-
- len++;
- }
- __VERIFIER_assert(len==5);
- return 1;
-
-
-}
diff --git a/regression/array-refinement/Array_UF12/main.c b/regression/array-refinement/Array_UF12/main.c
deleted file mode 100644
index 8932da571d6..00000000000
--- a/regression/array-refinement/Array_UF12/main.c
+++ /dev/null
@@ -1,40 +0,0 @@
-extern void __VERIFIER_error() __attribute__ ((__noreturn__));
-
-void __VERIFIER_assert(int cond) {
- if (!(cond)) {
- ERROR: __VERIFIER_error();
- }
- return;
-}
-int b;
-_Bool __VERIFIER_nondet_bool();
-int main(){
- _Bool k=__VERIFIER_nondet_bool();
- int i,n,j;
- int a[1025];
-
- if (k){
- n=0;
- } else {
- n=1023;
- }
-
- i=0;
-
- while ( i <= n){
- i++;
- j= j +2;
- }
-
- a[i]=0;
- a[j]=0;
- __VERIFIER_assert(j<1025);
- a[b]=0;
- if (b >= 0 && b < 1023)
- a[b]=1;
- else
- a[b%1023] =1;
-
- return 1;
-
-}
diff --git a/regression/array-refinement/Array_UF13/main.c b/regression/array-refinement/Array_UF13/main.c
deleted file mode 100644
index d64444acb02..00000000000
--- a/regression/array-refinement/Array_UF13/main.c
+++ /dev/null
@@ -1,27 +0,0 @@
-extern void __VERIFIER_error() __attribute__ ((__noreturn__));
-
-void __VERIFIER_assert(int cond) {
- if (!(cond)) {
- ERROR: __VERIFIER_error();
- }
- return;
-}
-int __VERIFIER_nondet_int();
-
- char x[100], y[100];
- int i,j,k;
-
-void main() {
- k = __VERIFIER_nondet_int();
-
- i = 0;
- while(x[i] != 0){
- y[i] = x[i];
- i++;
- }
- y[i] = 0;
-
- if(k >= 0 && k < i)
- if(y[k] != 0)
- {__VERIFIER_assert(0);}
-}
diff --git a/regression/array-refinement/Array_UF14/main.c b/regression/array-refinement/Array_UF14/main.c
deleted file mode 100644
index 1335adf8785..00000000000
--- a/regression/array-refinement/Array_UF14/main.c
+++ /dev/null
@@ -1,59 +0,0 @@
-extern void __VERIFIER_error() __attribute__ ((__noreturn__));
-
-extern void __VERIFIER_assume(int);
-void __VERIFIER_assert(int cond) {
- if (!(cond)) {
- ERROR: __VERIFIER_error();
- }
- return;
-}
-
-
-
-extern char __VERIFIER_nondet_char();
-
-main()
-{
- char string_A[5], string_B[5];
- int i, j, nc_A, nc_B, found=0;
-
-
- for(i=0; i<5; i++)
- string_A[i]=__VERIFIER_nondet_char();
- __VERIFIER_assume(string_A[5 -1]=='\0');
-
- for(i=0; i<5; i++)
- string_B[i]=__VERIFIER_nondet_char();
- __VERIFIER_assume(string_B[5 -1]=='\0');
-
- nc_A = 0;
- while(string_A[nc_A]!='\0')
- nc_A++;
-
- nc_B = 0;
- while(string_B[nc_B]!='\0')
- nc_B++;
-
- __VERIFIER_assume(nc_B >= nc_A);
-
-
- i=j=0;
- while((inc_B-1)<= nc_A);
-
-
- i=j=0;
- while((inc_B-1);
-
- __VERIFIER_assert(found == 0 || found == 1);
-}
diff --git a/regression/array-refinement/Array_UF16/main.c b/regression/array-refinement/Array_UF16/main.c
deleted file mode 100644
index aea6c758494..00000000000
--- a/regression/array-refinement/Array_UF16/main.c
+++ /dev/null
@@ -1,29 +0,0 @@
-extern void __VERIFIER_error() __attribute__ ((__noreturn__));
-
-extern int __VERIFIER_nondet_int(void);
-void __VERIFIER_assert(int cond) {
- if (!(cond)) {
- ERROR: __VERIFIER_error();
- }
- return;
-}
-extern unsigned int __VERIFIER_nondet_uint();
-
-int main()
-{
- unsigned int M = __VERIFIER_nondet_uint();
- int A[M], B[M], C[M];
- unsigned int i;
-
- for(i=0;i=2) {
- return -1;
- }
- r_strncpy(str2, str+start, j-start+1);
- str2[j-start+1] = 0;
- } else {
- return -1;
- }
- start = i+1;
- }
- } while (str[i] != 0);
- return 0;
-}
-int main ()
-{
- char A [2 + 2 + 4 +1];
- A[2 + 2 + 4] = 0;
- parse_expression_list (A);
- return 0;
-}
diff --git a/regression/array-refinement/Array_UF19/main.c b/regression/array-refinement/Array_UF19/main.c
deleted file mode 100644
index 0b8ac7904eb..00000000000
--- a/regression/array-refinement/Array_UF19/main.c
+++ /dev/null
@@ -1,79 +0,0 @@
-extern void __VERIFIER_error() __attribute__ ((__noreturn__));
-
-void __VERIFIER_assert(int cond) {
- if (!(cond)) {
- ERROR: __VERIFIER_error();
- }
- return;
-}
-typedef int size_t;
-typedef int bool;
-char *strchr(const char *s, int c);
-char *strrchr(const char *s, int c);
-char *strstr(const char *haystack, const char *needle);
-char *strncpy (char *dest, const char *src, size_t n);
-char *strncpy_ptr (char *dest, const char *src, size_t n);
-char *strcpy (char *dest, const char *src);
-unsigned strlen(const char *s);
-int strncmp (const char *s1, const char *s2, size_t n);
-int strcmp (const char *s1, const char *s2);
-char *strcat(char *dest, const char *src);
-void *memcpy(void *dest, const void *src, size_t n);
-int isascii (int c);
-int isspace (int c);
-int getc ( );
-char *strrand (char *s);
-int istrrand (char *s);
-int istrchr(const char *s, int c);
-int istrrchr(const char *s, int c);
-int istrncmp (const char *s1, int start, const char *s2, size_t n);
-int istrstr(const char *haystack, const char *needle);
-char *r_strncpy (char *dest, const char *src, size_t n);
-char *r_strcpy (char *dest, const char *src);
-char *r_strcat(char *dest, const char *src);
-char *r_strncat(char *dest, const char *src, size_t n);
-void *r_memcpy(void *dest, const void *src, size_t n);
-typedef unsigned int u_int;
-typedef unsigned char u_int8_t;
-struct ieee80211_scan_entry {
- u_int8_t *se_rsn_ie;
-};
-typedef int NSS_STATUS;
-typedef char fstring[2];
-struct sockaddr_un
-{
- char sun_path[2 + 1];
-};
-static int parse_expression_list(char *str)
-{
- int start=0, i=-1, j=-1;
- char str2[2];
- if (!str) return -1;
- do {
- i++;
- switch(str[i]) {
- case 0:
- while ((str[start] == ' ') || (str[start] == '\t')) start++;
- if (str[start] == '"') start++;
- j = i-1;
- while ((0 < j) && ((str[j] == ' ') || (str[j] == '\t'))) j--;
- if ((0 < j) && (str[j] == '"')) j--;
- if (start<=j) {
- r_strncpy(str2, str+start, j-start+1);
- __VERIFIER_assert(j - start + 1 < 2);
- str2[j-start+1] = 0;
- } else {
- return -1;
- }
- start = i+1;
- }
- } while (str[i] != 0);
- return 0;
-}
-int main ()
-{
- char A [2 + 2 + 4 +1];
- A[2 + 2 + 4] = 0;
- parse_expression_list (A);
- return 0;
-}
diff --git a/regression/array-refinement/Array_UF2/main.c b/regression/array-refinement/Array_UF2/main.c
deleted file mode 100644
index b2f11c543c0..00000000000
--- a/regression/array-refinement/Array_UF2/main.c
+++ /dev/null
@@ -1,13 +0,0 @@
-int main()
-{
- int a[4], b[4];
- int x,y,z;
- __CPROVER_assume(1<=y && y<=3);
- __CPROVER_assume(0<=z && z<=2);
- b[y] = x;
- b[z] = x;
- for(unsigned i = 0;i<4;i++) {
- a[i] = b[i];
- }
- __CPROVER_assert(a[y]==a[z], "a[y]==a[z]");
-}
diff --git a/regression/array-refinement/Array_UF4/main.c b/regression/array-refinement/Array_UF4/main.c
deleted file mode 100644
index 02db0e1a5b1..00000000000
--- a/regression/array-refinement/Array_UF4/main.c
+++ /dev/null
@@ -1,27 +0,0 @@
-extern void __VERIFIER_error() __attribute__ ((__noreturn__));
-
-void __VERIFIER_assert(int cond) {
- if (!(cond)) {
- ERROR: __VERIFIER_error();
- }
- return;
-}
-int __VERIFIER_nondet_int();
-
-main()
-{
- unsigned int SIZE=1;
- unsigned int j,k;
- int array[SIZE], menor;
-
- menor = __VERIFIER_nondet_int();
-
- for(j=0;j=menor);
-}
diff --git a/regression/array-refinement/Array_UF5/main.c b/regression/array-refinement/Array_UF5/main.c
deleted file mode 100644
index 096648bf99c..00000000000
--- a/regression/array-refinement/Array_UF5/main.c
+++ /dev/null
@@ -1,27 +0,0 @@
-extern void __VERIFIER_error() __attribute__ ((__noreturn__));
-
-void __VERIFIER_assert(int cond) {
- if (!(cond)) {
- ERROR: __VERIFIER_error();
- }
- return;
-}
-int __VERIFIER_nondet_int();
-
-main()
-{
- unsigned int SIZE=1;
- unsigned int j,k;
- int array[SIZE], menor;
-
- menor = __VERIFIER_nondet_int();
-
- for(j=0;jmenor);
-}
diff --git a/regression/array-refinement/Array_UF6/main.c b/regression/array-refinement/Array_UF6/main.c
deleted file mode 100644
index 641bf3bcad8..00000000000
--- a/regression/array-refinement/Array_UF6/main.c
+++ /dev/null
@@ -1,60 +0,0 @@
-extern void __VERIFIER_error() __attribute__ ((__noreturn__));
-
-void __VERIFIER_assert(int cond) {
- if (!(cond)) {
- ERROR: __VERIFIER_error();
- }
- return;
-}
-int INFINITY = 899;
-unsigned int __VERIFIER_nondet_uint();
-void main(){
- int nodecount = __VERIFIER_nondet_int();
- int edgecount = __VERIFIER_nondet_int();
- __VERIFIER_assume(0 <= nodecount <= 4);
- __VERIFIER_assume(0 <= edgecount <= 19);
- int source = 0;
- int Source[20] = {0,4,1,1,0,0,1,3,4,4,2,2,3,0,0,3,1,2,2,3};
- int Dest[20] = {1,3,4,1,1,4,3,4,3,0,0,0,0,2,3,0,2,1,0,4};
- int Weight[20] = {0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19};
- int distance[5];
- int x,y;
- int i,j;
-
- for(i = 0; i < nodecount; i++){
- if(i == source){
- distance[i] = 0;
- }
- else {
- distance[i] = INFINITY;
- }
- }
-
- for(i = 0; i < nodecount; i++)
- {
- for(j = 0; j < edgecount; j++)
- {
- x = Dest[j];
- y = Source[j];
- if(distance[x] > distance[y] + Weight[j])
- {
- distance[x] = -1;
- }
- }
- }
- for(i = 0; i < edgecount; i++)
- {
- x = Dest[i];
- y = Source[i];
- if(distance[x] > distance[y] + Weight[i])
- {
- return;
- }
- }
-
- for(i = 0; i < nodecount; i++)
- {
- __VERIFIER_assert(distance[i]>=0);
- }
-
-}
diff --git a/regression/array-refinement/Array_UF7/main.c b/regression/array-refinement/Array_UF7/main.c
deleted file mode 100644
index 7425e0dcd15..00000000000
--- a/regression/array-refinement/Array_UF7/main.c
+++ /dev/null
@@ -1,35 +0,0 @@
-extern void __VERIFIER_error() __attribute__ ((__noreturn__));
-
-void __VERIFIER_assert(int cond) {
- if (!(cond)) {
- ERROR: __VERIFIER_error();
- }
- return;
-}
-char __VERIFIER_nondet_char();
-unsigned int __VERIFIER_nondet_uint();
-
-int main() {
- int MAX = __VERIFIER_nondet_uint();
- char str1[MAX], str2[MAX];
- int cont, i, j;
- cont = 0;
-
- for (i=0; i= 0; i--) {
- str2[j] = str1[0];
- j++;
- }
-
- j = MAX-1;
- for (i=0; i= 0; i--) {
- str2[j] = str1[i];
- j++;
- }
-
- j = max-1;
- for (i=0; i= 0 && k < i)
+ if(y[k] == 0)
+ {
+ ERROR:
+ __VERIFIER_error();
+ }
+}
diff --git a/regression/array-refinement/Array_UF10/test.desc b/regression/cbmc/Array_UF10/test.desc
similarity index 100%
rename from regression/array-refinement/Array_UF10/test.desc
rename to regression/cbmc/Array_UF10/test.desc
diff --git a/regression/cbmc/Array_UF11/main.c b/regression/cbmc/Array_UF11/main.c
new file mode 100644
index 00000000000..cb6f88fe814
--- /dev/null
+++ b/regression/cbmc/Array_UF11/main.c
@@ -0,0 +1,33 @@
+extern void __VERIFIER_error();
+
+void __VERIFIER_assert(int cond)
+{
+ if(!(cond))
+ {
+ ERROR:
+ __VERIFIER_error();
+ }
+ return;
+}
+
+_Bool __VERIFIER_nondet_bool();
+
+int main()
+{
+ int a[5];
+ int len = 0;
+ _Bool c = __VERIFIER_nondet_bool();
+ int i;
+
+ while(c)
+ {
+ if(len == 4)
+ len = 0;
+
+ a[len] = 0;
+
+ len++;
+ }
+ __VERIFIER_assert(len == 5);
+ return 1;
+}
diff --git a/regression/array-refinement/Array_UF11/test.desc b/regression/cbmc/Array_UF11/test.desc
similarity index 100%
rename from regression/array-refinement/Array_UF11/test.desc
rename to regression/cbmc/Array_UF11/test.desc
diff --git a/regression/cbmc/Array_UF12/main.c b/regression/cbmc/Array_UF12/main.c
new file mode 100644
index 00000000000..def2fa51b97
--- /dev/null
+++ b/regression/cbmc/Array_UF12/main.c
@@ -0,0 +1,47 @@
+extern void __VERIFIER_error();
+
+void __VERIFIER_assert(int cond)
+{
+ if(!(cond))
+ {
+ ERROR:
+ __VERIFIER_error();
+ }
+ return;
+}
+int b;
+_Bool __VERIFIER_nondet_bool();
+int main()
+{
+ _Bool k = __VERIFIER_nondet_bool();
+ int i, n, j;
+ int a[1025];
+
+ if(k)
+ {
+ n = 0;
+ }
+ else
+ {
+ n = 1023;
+ }
+
+ i = 0;
+
+ while(i <= n)
+ {
+ i++;
+ j = j + 2;
+ }
+
+ a[i] = 0;
+ a[j] = 0;
+ __VERIFIER_assert(j < 1025);
+ a[b] = 0;
+ if(b >= 0 && b < 1023)
+ a[b] = 1;
+ else
+ a[b % 1023] = 1;
+
+ return 1;
+}
diff --git a/regression/array-refinement/Array_UF12/test.desc b/regression/cbmc/Array_UF12/test.desc
similarity index 100%
rename from regression/array-refinement/Array_UF12/test.desc
rename to regression/cbmc/Array_UF12/test.desc
diff --git a/regression/cbmc/Array_UF13/main.c b/regression/cbmc/Array_UF13/main.c
new file mode 100644
index 00000000000..b467c63f7f4
--- /dev/null
+++ b/regression/cbmc/Array_UF13/main.c
@@ -0,0 +1,34 @@
+extern void __VERIFIER_error();
+
+void __VERIFIER_assert(int cond)
+{
+ if(!(cond))
+ {
+ ERROR:
+ __VERIFIER_error();
+ }
+ return;
+}
+int __VERIFIER_nondet_int();
+
+char x[100], y[100];
+int i, j, k;
+
+void main()
+{
+ k = __VERIFIER_nondet_int();
+
+ i = 0;
+ while(x[i] != 0)
+ {
+ y[i] = x[i];
+ i++;
+ }
+ y[i] = 0;
+
+ if(k >= 0 && k < i)
+ if(y[k] != 0)
+ {
+ __VERIFIER_assert(0);
+ }
+}
diff --git a/regression/array-refinement/Array_UF13/test.desc b/regression/cbmc/Array_UF13/test.desc
similarity index 100%
rename from regression/array-refinement/Array_UF13/test.desc
rename to regression/cbmc/Array_UF13/test.desc
diff --git a/regression/cbmc/Array_UF14/main.c b/regression/cbmc/Array_UF14/main.c
new file mode 100644
index 00000000000..767bf718c96
--- /dev/null
+++ b/regression/cbmc/Array_UF14/main.c
@@ -0,0 +1,57 @@
+extern void __VERIFIER_error();
+
+extern void __VERIFIER_assume(int);
+void __VERIFIER_assert(int cond)
+{
+ if(!(cond))
+ {
+ ERROR:
+ __VERIFIER_error();
+ }
+ return;
+}
+
+extern char __VERIFIER_nondet_char();
+
+main()
+{
+ char string_A[5], string_B[5];
+ int i, j, nc_A, nc_B, found = 0;
+
+ for(i = 0; i < 5; i++)
+ string_A[i] = __VERIFIER_nondet_char();
+ __VERIFIER_assume(string_A[5 - 1] == '\0');
+
+ for(i = 0; i < 5; i++)
+ string_B[i] = __VERIFIER_nondet_char();
+ __VERIFIER_assume(string_B[5 - 1] == '\0');
+
+ nc_A = 0;
+ while(string_A[nc_A] != '\0')
+ nc_A++;
+
+ nc_B = 0;
+ while(string_B[nc_B] != '\0')
+ nc_B++;
+
+ __VERIFIER_assume(nc_B >= nc_A);
+
+ i = j = 0;
+ while((i < nc_A) && (j < nc_B))
+ {
+ if(string_A[i] == string_B[j])
+ {
+ i++;
+ j++;
+ }
+ else
+ {
+ i = i - j + 1;
+ j = 0;
+ }
+ }
+
+ found = (j > nc_B - 1) << i;
+
+ __VERIFIER_assert(found == 0 || found == 1);
+}
diff --git a/regression/array-refinement/Array_UF14/test.desc b/regression/cbmc/Array_UF14/test.desc
similarity index 87%
rename from regression/array-refinement/Array_UF14/test.desc
rename to regression/cbmc/Array_UF14/test.desc
index 3830439f347..2a5c51a9f90 100644
--- a/regression/array-refinement/Array_UF14/test.desc
+++ b/regression/cbmc/Array_UF14/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE thorough-paths
main.c
--arrays-uf-always --no-propagation --refine-arrays --unwind 6
^EXIT=10$
diff --git a/regression/cbmc/Array_UF15/main.c b/regression/cbmc/Array_UF15/main.c
new file mode 100644
index 00000000000..6849b8b3aff
--- /dev/null
+++ b/regression/cbmc/Array_UF15/main.c
@@ -0,0 +1,57 @@
+extern void __VERIFIER_error();
+
+extern void __VERIFIER_assume(int);
+void __VERIFIER_assert(int cond)
+{
+ if(!(cond))
+ {
+ ERROR:
+ __VERIFIER_error();
+ }
+ return;
+}
+
+extern char __VERIFIER_nondet_char();
+
+main()
+{
+ char string_A[5], string_B[5];
+ int i, j, nc_A, nc_B, found = 0;
+
+ for(i = 0; i < 5; i++)
+ string_A[i] = __VERIFIER_nondet_char();
+ __VERIFIER_assume(string_A[5 - 1] == '\0');
+
+ for(i = 0; i < 5; i++)
+ string_B[i] = __VERIFIER_nondet_char();
+ __VERIFIER_assume(string_B[5 - 1] == '\0');
+
+ nc_A = 0;
+ while(string_A[nc_A] != '\0')
+ nc_A++;
+
+ nc_B = 0;
+ while(string_B[nc_B] != '\0')
+ nc_B++;
+
+ __VERIFIER_assume(nc_B >= nc_A);
+
+ i = j = 0;
+ while((i < nc_A) && (j < nc_B))
+ {
+ if(string_A[i] == string_B[j])
+ {
+ i++;
+ j++;
+ }
+ else
+ {
+ i = i - j + 1;
+ j = 0;
+ }
+ }
+
+ found = (j > nc_B - 1);
+
+ __VERIFIER_assert(found == 0 || found == 1);
+}
diff --git a/regression/array-refinement/Array_UF18/test.desc b/regression/cbmc/Array_UF15/test.desc
similarity index 87%
rename from regression/array-refinement/Array_UF18/test.desc
rename to regression/cbmc/Array_UF15/test.desc
index 61e3418f5e6..15690b94615 100644
--- a/regression/array-refinement/Array_UF18/test.desc
+++ b/regression/cbmc/Array_UF15/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE thorough-paths
main.c
--arrays-uf-always --no-propagation --refine-arrays --unwind 11
^EXIT=0$
diff --git a/regression/cbmc/Array_UF16/main.c b/regression/cbmc/Array_UF16/main.c
new file mode 100644
index 00000000000..6fac8ee376e
--- /dev/null
+++ b/regression/cbmc/Array_UF16/main.c
@@ -0,0 +1,32 @@
+extern void __VERIFIER_error();
+
+extern int __VERIFIER_nondet_int(void);
+void __VERIFIER_assert(int cond)
+{
+ if(!(cond))
+ {
+ ERROR:
+ __VERIFIER_error();
+ }
+ return;
+}
+extern unsigned int __VERIFIER_nondet_uint();
+
+int main()
+{
+ unsigned int M = __VERIFIER_nondet_uint();
+ int A[M], B[M], C[M];
+ unsigned int i;
+
+ for(i = 0; i < M; i++)
+ A[i] = __VERIFIER_nondet_int();
+
+ for(i = 0; i < M; i++)
+ B[i] = __VERIFIER_nondet_int();
+
+ for(i = 0; i < M; i++)
+ C[i] = A[i] + B[i];
+
+ for(i = 0; i < M; i++)
+ __VERIFIER_assert(C[i] == A[i] - B[i]);
+}
diff --git a/regression/array-refinement/Array_UF16/test.desc b/regression/cbmc/Array_UF16/test.desc
similarity index 100%
rename from regression/array-refinement/Array_UF16/test.desc
rename to regression/cbmc/Array_UF16/test.desc
diff --git a/regression/cbmc/Array_UF17/main.c b/regression/cbmc/Array_UF17/main.c
new file mode 100644
index 00000000000..af0d10ab711
--- /dev/null
+++ b/regression/cbmc/Array_UF17/main.c
@@ -0,0 +1,96 @@
+extern void __VERIFIER_error();
+
+void __VERIFIER_assert(int cond)
+{
+ if(!(cond))
+ {
+ ERROR:
+ __VERIFIER_error();
+ }
+ return;
+}
+typedef int size_t;
+typedef int bool;
+char *strchr(const char *s, int c);
+char *strrchr(const char *s, int c);
+char *strstr(const char *haystack, const char *needle);
+char *strncpy(char *dest, const char *src, size_t n);
+char *strncpy_ptr(char *dest, const char *src, size_t n);
+char *strcpy(char *dest, const char *src);
+unsigned strlen(const char *s);
+int strncmp(const char *s1, const char *s2, size_t n);
+int strcmp(const char *s1, const char *s2);
+char *strcat(char *dest, const char *src);
+void *memcpy(void *dest, const void *src, size_t n);
+int isascii(int c);
+int isspace(int c);
+int getc();
+char *strrand(char *s);
+int istrrand(char *s);
+int istrchr(const char *s, int c);
+int istrrchr(const char *s, int c);
+int istrncmp(const char *s1, int start, const char *s2, size_t n);
+int istrstr(const char *haystack, const char *needle);
+char *r_strncpy(char *dest, const char *src, size_t n);
+char *r_strcpy(char *dest, const char *src);
+char *r_strcat(char *dest, const char *src);
+char *r_strncat(char *dest, const char *src, size_t n);
+void *r_memcpy(void *dest, const void *src, size_t n);
+typedef unsigned int u_int;
+typedef unsigned char u_int8_t;
+struct ieee80211_scan_entry
+{
+ u_int8_t *se_rsn_ie;
+};
+typedef int NSS_STATUS;
+typedef char fstring[2];
+struct sockaddr_un
+{
+ char sun_path[2 + 1];
+};
+static int parse_expression_list(char *str)
+{
+ int start = 0, i = -1, j = -1;
+ char str2[2];
+ if(!str)
+ return -1;
+ do
+ {
+ i++;
+ switch(str[i])
+ {
+ case 0:
+ while((str[start] == ' ') || (str[start] == '\t'))
+ start++;
+ if(str[start] == '"')
+ start++;
+ j = i - 1;
+ while((0 < j) && ((str[j] == ' ') || (str[j] == '\t')))
+ j--;
+ if((0 < j) && (str[j] == '"'))
+ j--;
+ if(start <= j)
+ {
+ if(j - start + 1 >= 2)
+ {
+ return -1;
+ }
+ r_strncpy(str2, str + start, j - start + 1);
+ str2[j - start + 1] = 0;
+ }
+ else
+ {
+ return -1;
+ }
+ start = i + 1;
+ }
+ } while(str[i] != 0);
+ return 0;
+}
+int main()
+{
+ char A[2 + 2 + 4 + 1];
+ A[2 + 2 + 4] = 0;
+ parse_expression_list(A);
+ return 0;
+}
diff --git a/regression/array-refinement/Array_UF17/test.desc b/regression/cbmc/Array_UF17/test.desc
similarity index 87%
rename from regression/array-refinement/Array_UF17/test.desc
rename to regression/cbmc/Array_UF17/test.desc
index 4b585860724..e9939c1e8c3 100644
--- a/regression/array-refinement/Array_UF17/test.desc
+++ b/regression/cbmc/Array_UF17/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE thorough-paths
main.c
--arrays-uf-always --no-propagation --refine-arrays --unwind 9
^EXIT=0$
diff --git a/regression/array-refinement/Array_UF18/main.c b/regression/cbmc/Array_UF18/main.c
similarity index 53%
rename from regression/array-refinement/Array_UF18/main.c
rename to regression/cbmc/Array_UF18/main.c
index 63362ce18d8..e60e37d6bf2 100644
--- a/regression/array-refinement/Array_UF18/main.c
+++ b/regression/cbmc/Array_UF18/main.c
@@ -1,12 +1,15 @@
-extern void __VERIFIER_error() __attribute__ ((__noreturn__));
+extern void __VERIFIER_error();
-void __VERIFIER_assert(int cond) {
- if (!(cond)) {
- ERROR: __VERIFIER_error();
+void __VERIFIER_assert(int cond)
+{
+ if(!(cond))
+ {
+ ERROR:
+ __VERIFIER_error();
}
return;
}
-int main (void)
+int main(void)
{
char in[11];
char *s;
@@ -18,7 +21,7 @@ int main (void)
s = in;
i = 0;
c = in[idx_in];
- while (('0' <= c) && (c <= '9'))
+ while(('0' <= c) && (c <= '9'))
{
j = c - '0';
i = i * 10U + j;
@@ -26,6 +29,6 @@ int main (void)
c = in[idx_in];
}
- __VERIFIER_assert (i >= 0);
+ __VERIFIER_assert(i >= 0);
return 0;
}
diff --git a/regression/array-refinement/Array_UF15/test.desc b/regression/cbmc/Array_UF18/test.desc
similarity index 100%
rename from regression/array-refinement/Array_UF15/test.desc
rename to regression/cbmc/Array_UF18/test.desc
diff --git a/regression/cbmc/Array_UF19/main.c b/regression/cbmc/Array_UF19/main.c
new file mode 100644
index 00000000000..40b092cda2e
--- /dev/null
+++ b/regression/cbmc/Array_UF19/main.c
@@ -0,0 +1,93 @@
+extern void __VERIFIER_error();
+
+void __VERIFIER_assert(int cond)
+{
+ if(!(cond))
+ {
+ ERROR:
+ __VERIFIER_error();
+ }
+ return;
+}
+typedef int size_t;
+typedef int bool;
+char *strchr(const char *s, int c);
+char *strrchr(const char *s, int c);
+char *strstr(const char *haystack, const char *needle);
+char *strncpy(char *dest, const char *src, size_t n);
+char *strncpy_ptr(char *dest, const char *src, size_t n);
+char *strcpy(char *dest, const char *src);
+unsigned strlen(const char *s);
+int strncmp(const char *s1, const char *s2, size_t n);
+int strcmp(const char *s1, const char *s2);
+char *strcat(char *dest, const char *src);
+void *memcpy(void *dest, const void *src, size_t n);
+int isascii(int c);
+int isspace(int c);
+int getc();
+char *strrand(char *s);
+int istrrand(char *s);
+int istrchr(const char *s, int c);
+int istrrchr(const char *s, int c);
+int istrncmp(const char *s1, int start, const char *s2, size_t n);
+int istrstr(const char *haystack, const char *needle);
+char *r_strncpy(char *dest, const char *src, size_t n);
+char *r_strcpy(char *dest, const char *src);
+char *r_strcat(char *dest, const char *src);
+char *r_strncat(char *dest, const char *src, size_t n);
+void *r_memcpy(void *dest, const void *src, size_t n);
+typedef unsigned int u_int;
+typedef unsigned char u_int8_t;
+struct ieee80211_scan_entry
+{
+ u_int8_t *se_rsn_ie;
+};
+typedef int NSS_STATUS;
+typedef char fstring[2];
+struct sockaddr_un
+{
+ char sun_path[2 + 1];
+};
+static int parse_expression_list(char *str)
+{
+ int start = 0, i = -1, j = -1;
+ char str2[2];
+ if(!str)
+ return -1;
+ do
+ {
+ i++;
+ switch(str[i])
+ {
+ case 0:
+ while((str[start] == ' ') || (str[start] == '\t'))
+ start++;
+ if(str[start] == '"')
+ start++;
+ j = i - 1;
+ while((0 < j) && ((str[j] == ' ') || (str[j] == '\t')))
+ j--;
+ if((0 < j) && (str[j] == '"'))
+ j--;
+ if(start <= j)
+ {
+ r_strncpy(str2, str + start, j - start + 1);
+ __VERIFIER_assert(j - start + 1 < 2);
+ str2[j - start + 1] = 0;
+ }
+ else
+ {
+ return -1;
+ }
+ start = i + 1;
+ }
+ } while(str[i] != 0);
+ return 0;
+}
+int main()
+{
+ char A[2 + 2 + 4 + 1];
+ A[2 + 2 + 4] = 0;
+ parse_expression_list(A);
+ return 0;
+}
diff --git a/regression/array-refinement/Array_UF6/test.desc b/regression/cbmc/Array_UF19/test.desc
similarity index 87%
rename from regression/array-refinement/Array_UF6/test.desc
rename to regression/cbmc/Array_UF19/test.desc
index c47f81c71cc..d92ab778129 100644
--- a/regression/array-refinement/Array_UF6/test.desc
+++ b/regression/cbmc/Array_UF19/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE thorough-paths
main.c
--arrays-uf-always --no-propagation --refine-arrays --unwind 3
^EXIT=10$
diff --git a/regression/cbmc/Array_UF2/main.c b/regression/cbmc/Array_UF2/main.c
new file mode 100644
index 00000000000..e3ddf0d1d64
--- /dev/null
+++ b/regression/cbmc/Array_UF2/main.c
@@ -0,0 +1,14 @@
+int main()
+{
+ int a[4], b[4];
+ int x, y, z;
+ __CPROVER_assume(1 <= y && y <= 3);
+ __CPROVER_assume(0 <= z && z <= 2);
+ b[y] = x;
+ b[z] = x;
+ for(unsigned i = 0; i < 4; i++)
+ {
+ a[i] = b[i];
+ }
+ __CPROVER_assert(a[y] == a[z], "a[y]==a[z]");
+}
diff --git a/regression/array-refinement/Array_UF2/test.desc b/regression/cbmc/Array_UF2/test.desc
similarity index 100%
rename from regression/array-refinement/Array_UF2/test.desc
rename to regression/cbmc/Array_UF2/test.desc
diff --git a/regression/array-refinement/Array_UF20/main.c b/regression/cbmc/Array_UF20/main.c
similarity index 56%
rename from regression/array-refinement/Array_UF20/main.c
rename to regression/cbmc/Array_UF20/main.c
index d44354af92b..baa7d5a216a 100644
--- a/regression/array-refinement/Array_UF20/main.c
+++ b/regression/cbmc/Array_UF20/main.c
@@ -1,29 +1,32 @@
-extern void __VERIFIER_error() __attribute__ ((__noreturn__));
+extern void __VERIFIER_error();
extern char __VERIFIER_nondet_char();
-void __VERIFIER_assert(int cond) {
- if (!(cond)) {
- ERROR: __VERIFIER_error();
+void __VERIFIER_assert(int cond)
+{
+ if(!(cond))
+ {
+ ERROR:
+ __VERIFIER_error();
}
return;
}
-int main (void)
+int main(void)
{
char in[11];
char *s;
unsigned char c;
int i, j;
int idx_in;
- for (i = 0; i < 11; i++)
+ for(i = 0; i < 11; i++)
in[i] = __VERIFIER_nondet_char();
in[10] = 0;
idx_in = 0;
s = in;
i = 0;
c = in[idx_in];
- while (('0' <= c) && (c <= '9'))
+ while(('0' <= c) && (c <= '9'))
{
j = c - '0';
i = i * 10U + j;
@@ -31,6 +34,6 @@ int main (void)
c = in[idx_in];
}
- __VERIFIER_assert (i >= 0);
+ __VERIFIER_assert(i >= 0);
return 0;
}
diff --git a/regression/array-refinement/Array_UF20/test.desc b/regression/cbmc/Array_UF20/test.desc
similarity index 100%
rename from regression/array-refinement/Array_UF20/test.desc
rename to regression/cbmc/Array_UF20/test.desc
diff --git a/regression/array-refinement/Array_UF3/main.c b/regression/cbmc/Array_UF3/main.c
similarity index 56%
rename from regression/array-refinement/Array_UF3/main.c
rename to regression/cbmc/Array_UF3/main.c
index 4db1610f46e..fb705f95364 100644
--- a/regression/array-refinement/Array_UF3/main.c
+++ b/regression/cbmc/Array_UF3/main.c
@@ -1,19 +1,19 @@
main()
{
unsigned int N;
- __CPROVER_assume(N>0);
+ __CPROVER_assume(N > 0);
- unsigned int j,k;
+ unsigned int j, k;
int matrix[N], max;
max = __VERIFIER_nondet_int();
- for(j=0;j=max)
+ if(matrix[j] >= max)
max = matrix[j];
}
- assert(matrix[0]= menor);
+}
diff --git a/regression/array-refinement/Array_UF4/test.desc b/regression/cbmc/Array_UF4/test.desc
similarity index 93%
rename from regression/array-refinement/Array_UF4/test.desc
rename to regression/cbmc/Array_UF4/test.desc
index cc6143ea6d1..72779529649 100644
--- a/regression/array-refinement/Array_UF4/test.desc
+++ b/regression/cbmc/Array_UF4/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
main.c
--arrays-uf-always --no-propagation --refine-arrays --unwind 2
^EXIT=0$
diff --git a/regression/cbmc/Array_UF5/main.c b/regression/cbmc/Array_UF5/main.c
new file mode 100644
index 00000000000..6b4142b5e36
--- /dev/null
+++ b/regression/cbmc/Array_UF5/main.c
@@ -0,0 +1,31 @@
+extern void __VERIFIER_error();
+
+void __VERIFIER_assert(int cond)
+{
+ if(!(cond))
+ {
+ ERROR:
+ __VERIFIER_error();
+ }
+ return;
+}
+int __VERIFIER_nondet_int();
+
+main()
+{
+ unsigned int SIZE = 1;
+ unsigned int j, k;
+ int array[SIZE], menor;
+
+ menor = __VERIFIER_nondet_int();
+
+ for(j = 0; j < SIZE; j++)
+ {
+ array[j] = __VERIFIER_nondet_int();
+
+ if(array[j] <= menor)
+ menor = array[j];
+ }
+
+ __VERIFIER_assert(array[0] > menor);
+}
diff --git a/regression/array-refinement/Array_UF5/test.desc b/regression/cbmc/Array_UF5/test.desc
similarity index 100%
rename from regression/array-refinement/Array_UF5/test.desc
rename to regression/cbmc/Array_UF5/test.desc
diff --git a/regression/cbmc/Array_UF6/main.c b/regression/cbmc/Array_UF6/main.c
new file mode 100644
index 00000000000..1d5a83e93a7
--- /dev/null
+++ b/regression/cbmc/Array_UF6/main.c
@@ -0,0 +1,67 @@
+extern void __VERIFIER_error();
+
+void __VERIFIER_assert(int cond)
+{
+ if(!(cond))
+ {
+ ERROR:
+ __VERIFIER_error();
+ }
+ return;
+}
+int INFINITY = 899;
+unsigned int __VERIFIER_nondet_uint();
+void main()
+{
+ int nodecount = __VERIFIER_nondet_int();
+ int edgecount = __VERIFIER_nondet_int();
+ __VERIFIER_assume(0 <= nodecount <= 4);
+ __VERIFIER_assume(0 <= edgecount <= 19);
+ int source = 0;
+ int Source[20] = {0, 4, 1, 1, 0, 0, 1, 3, 4, 4, 2, 2, 3, 0, 0, 3, 1, 2, 2, 3};
+ int Dest[20] = {1, 3, 4, 1, 1, 4, 3, 4, 3, 0, 0, 0, 0, 2, 3, 0, 2, 1, 0, 4};
+ int Weight[20] = {0, 1, 2, 3, 4, 5, 6, 7, 8, 9,
+ 10, 11, 12, 13, 14, 15, 16, 17, 18, 19};
+ int distance[5];
+ int x, y;
+ int i, j;
+
+ for(i = 0; i < nodecount; i++)
+ {
+ if(i == source)
+ {
+ distance[i] = 0;
+ }
+ else
+ {
+ distance[i] = INFINITY;
+ }
+ }
+
+ for(i = 0; i < nodecount; i++)
+ {
+ for(j = 0; j < edgecount; j++)
+ {
+ x = Dest[j];
+ y = Source[j];
+ if(distance[x] > distance[y] + Weight[j])
+ {
+ distance[x] = -1;
+ }
+ }
+ }
+ for(i = 0; i < edgecount; i++)
+ {
+ x = Dest[i];
+ y = Source[i];
+ if(distance[x] > distance[y] + Weight[i])
+ {
+ return;
+ }
+ }
+
+ for(i = 0; i < nodecount; i++)
+ {
+ __VERIFIER_assert(distance[i] >= 0);
+ }
+}
diff --git a/regression/array-refinement/Array_UF7/test.desc b/regression/cbmc/Array_UF6/test.desc
similarity index 87%
rename from regression/array-refinement/Array_UF7/test.desc
rename to regression/cbmc/Array_UF6/test.desc
index c47f81c71cc..d92ab778129 100644
--- a/regression/array-refinement/Array_UF7/test.desc
+++ b/regression/cbmc/Array_UF6/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE thorough-paths
main.c
--arrays-uf-always --no-propagation --refine-arrays --unwind 3
^EXIT=10$
diff --git a/regression/cbmc/Array_UF7/main.c b/regression/cbmc/Array_UF7/main.c
new file mode 100644
index 00000000000..e0d9e5b702d
--- /dev/null
+++ b/regression/cbmc/Array_UF7/main.c
@@ -0,0 +1,42 @@
+extern void __VERIFIER_error();
+
+void __VERIFIER_assert(int cond)
+{
+ if(!(cond))
+ {
+ ERROR:
+ __VERIFIER_error();
+ }
+ return;
+}
+char __VERIFIER_nondet_char();
+unsigned int __VERIFIER_nondet_uint();
+
+int main()
+{
+ int MAX = __VERIFIER_nondet_uint();
+ char str1[MAX], str2[MAX];
+ int cont, i, j;
+ cont = 0;
+
+ for(i = 0; i < MAX; i++)
+ {
+ str1[i] = __VERIFIER_nondet_char();
+ }
+ str1[MAX - 1] = '\0';
+
+ j = 0;
+
+ for(i = MAX - 1; i >= 0; i--)
+ {
+ str2[j] = str1[0];
+ j++;
+ }
+
+ j = MAX - 1;
+ for(i = 0; i < MAX; i++)
+ {
+ __VERIFIER_assert(str1[i] == str2[j]);
+ j--;
+ }
+}
diff --git a/regression/array-refinement/Array_UF19/test.desc b/regression/cbmc/Array_UF7/test.desc
similarity index 100%
rename from regression/array-refinement/Array_UF19/test.desc
rename to regression/cbmc/Array_UF7/test.desc
diff --git a/regression/cbmc/Array_UF8/main.c b/regression/cbmc/Array_UF8/main.c
new file mode 100644
index 00000000000..e4dc753d4c8
--- /dev/null
+++ b/regression/cbmc/Array_UF8/main.c
@@ -0,0 +1,41 @@
+extern void __VERIFIER_error();
+
+void __VERIFIER_assert(int cond)
+{
+ if(!(cond))
+ {
+ ERROR:
+ __VERIFIER_error();
+ }
+ return;
+}
+char __VERIFIER_nondet_char();
+
+int main()
+{
+ unsigned int max = 5;
+ char str1[max], str2[max];
+ int i, j;
+
+ for(i = 0; i < max; i++)
+ {
+ str1[i] = __VERIFIER_nondet_char();
+ }
+
+ str1[max - 1] = '\0';
+
+ j = 0;
+
+ for(i = max - 1; i >= 0; i--)
+ {
+ str2[j] = str1[i];
+ j++;
+ }
+
+ j = max - 1;
+ for(i = 0; i < max; i++)
+ {
+ __VERIFIER_assert(str1[i] == str2[j]);
+ j--;
+ }
+}
diff --git a/regression/array-refinement/Array_UF8/test.desc b/regression/cbmc/Array_UF8/test.desc
similarity index 93%
rename from regression/array-refinement/Array_UF8/test.desc
rename to regression/cbmc/Array_UF8/test.desc
index 715300a8de6..ba128759099 100644
--- a/regression/array-refinement/Array_UF8/test.desc
+++ b/regression/cbmc/Array_UF8/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
main.c
--arrays-uf-always --no-propagation --refine-arrays --unwind 6
^EXIT=0$
diff --git a/regression/cbmc/Array_UF9/main.c b/regression/cbmc/Array_UF9/main.c
new file mode 100644
index 00000000000..159669be5f1
--- /dev/null
+++ b/regression/cbmc/Array_UF9/main.c
@@ -0,0 +1,34 @@
+extern void __VERIFIER_error();
+
+void __VERIFIER_assert(int cond)
+{
+ if(!(cond))
+ {
+ ERROR:
+ __VERIFIER_error();
+ }
+ return;
+}
+unsigned int __VERIFIER_nondet_uint();
+unsigned int SIZE;
+int linear_search(int *a, int n, int q)
+{
+ unsigned int j = 0;
+ while(j < n && a[j] != q)
+ {
+ j++;
+ if(j == 20)
+ j = -1;
+ }
+ if(j < SIZE)
+ return 1;
+ else
+ return 0;
+}
+int main()
+{
+ SIZE = (__VERIFIER_nondet_uint() / 2) + 1;
+ int a[SIZE];
+ a[SIZE / 2] = 3;
+ __VERIFIER_assert(linear_search(a, SIZE, 3));
+}
diff --git a/regression/array-refinement/Array_UF9/test.desc b/regression/cbmc/Array_UF9/test.desc
similarity index 100%
rename from regression/array-refinement/Array_UF9/test.desc
rename to regression/cbmc/Array_UF9/test.desc