diff --git a/regression/cbmc/builtin_is/test.desc b/regression/cbmc/builtin_is/test.desc deleted file mode 100644 index 2b79617eedb..00000000000 --- a/regression/cbmc/builtin_is/test.desc +++ /dev/null @@ -1,7 +0,0 @@ -KNOWNBUG -main.c - -^EXIT=6$ -^SIGNAL=0$ -expected to have two float/double arguments --- diff --git a/regression/cbmc/builtin_va_copy_lvalue/test.desc b/regression/cbmc/builtin_va_copy_lvalue/test.desc deleted file mode 100644 index 27e7c0c6e96..00000000000 --- a/regression/cbmc/builtin_va_copy_lvalue/test.desc +++ /dev/null @@ -1,7 +0,0 @@ -KNOWNBUG -main.c - -^EXIT=6$ -^SIGNAL=0$ -argument expected to be lvalue --- diff --git a/regression/cbmc/builtin_va_end_lvalue/test.desc b/regression/cbmc/builtin_va_end_lvalue/test.desc deleted file mode 100644 index 27e7c0c6e96..00000000000 --- a/regression/cbmc/builtin_va_end_lvalue/test.desc +++ /dev/null @@ -1,7 +0,0 @@ -KNOWNBUG -main.c - -^EXIT=6$ -^SIGNAL=0$ -argument expected to be lvalue --- diff --git a/regression/cbmc/builtin_va_start_lvalue/test.desc b/regression/cbmc/builtin_va_start_lvalue/test.desc deleted file mode 100644 index 27e7c0c6e96..00000000000 --- a/regression/cbmc/builtin_va_start_lvalue/test.desc +++ /dev/null @@ -1,7 +0,0 @@ -KNOWNBUG -main.c - -^EXIT=6$ -^SIGNAL=0$ -argument expected to be lvalue --- diff --git a/regression/cbmc/builtin_va_start_two/test.desc b/regression/cbmc/builtin_va_start_two/test.desc deleted file mode 100644 index adaf8a6ccf2..00000000000 --- a/regression/cbmc/builtin_va_start_two/test.desc +++ /dev/null @@ -1,7 +0,0 @@ -KNOWNBUG -main.c - -^EXIT=6$ -^SIGNAL=0$ -expected to have two arguments --- diff --git a/regression/cbmc/builtin_is/main.c b/regression/goto-gcc/builtin_is/main.c similarity index 100% rename from regression/cbmc/builtin_is/main.c rename to regression/goto-gcc/builtin_is/main.c diff --git a/regression/goto-gcc/builtin_is/test.desc b/regression/goto-gcc/builtin_is/test.desc new file mode 100644 index 00000000000..ba0487fd27f --- /dev/null +++ b/regression/goto-gcc/builtin_is/test.desc @@ -0,0 +1,10 @@ +KNOWNBUG +main.c + +^EXIT=1$ +^SIGNAL=0$ +expected to have two float/double arguments +-- +-- +The C front-end should catch the problem during type checking, and not leave it +to goto-program conversion to detect the problem. diff --git a/regression/cbmc/builtin_va_copy_lvalue/main.c b/regression/goto-gcc/builtin_va_copy_lvalue/main.c similarity index 100% rename from regression/cbmc/builtin_va_copy_lvalue/main.c rename to regression/goto-gcc/builtin_va_copy_lvalue/main.c diff --git a/regression/goto-gcc/builtin_va_copy_lvalue/test.desc b/regression/goto-gcc/builtin_va_copy_lvalue/test.desc new file mode 100644 index 00000000000..413f198cf36 --- /dev/null +++ b/regression/goto-gcc/builtin_va_copy_lvalue/test.desc @@ -0,0 +1,10 @@ +KNOWNBUG +main.c + +^EXIT=1$ +^SIGNAL=0$ +argument expected to be lvalue +-- +-- +The C front-end should catch the problem during type checking, and not leave it +to goto-program conversion to detect the problem. diff --git a/regression/cbmc/builtin_va_copy_two/main.c b/regression/goto-gcc/builtin_va_copy_two/main.c similarity index 100% rename from regression/cbmc/builtin_va_copy_two/main.c rename to regression/goto-gcc/builtin_va_copy_two/main.c diff --git a/regression/cbmc/builtin_va_end_one/test.desc b/regression/goto-gcc/builtin_va_copy_two/test.desc similarity index 87% rename from regression/cbmc/builtin_va_end_one/test.desc rename to regression/goto-gcc/builtin_va_copy_two/test.desc index bca33a5dd6d..656aeffa3b3 100644 --- a/regression/cbmc/builtin_va_end_one/test.desc +++ b/regression/goto-gcc/builtin_va_copy_two/test.desc @@ -1,7 +1,7 @@ CORE main.c -^EXIT=6$ +^EXIT=1$ ^SIGNAL=0$ wrong number of function arguments -- diff --git a/regression/cbmc/builtin_va_end_lvalue/main.c b/regression/goto-gcc/builtin_va_end_lvalue/main.c similarity index 100% rename from regression/cbmc/builtin_va_end_lvalue/main.c rename to regression/goto-gcc/builtin_va_end_lvalue/main.c diff --git a/regression/goto-gcc/builtin_va_end_lvalue/test.desc b/regression/goto-gcc/builtin_va_end_lvalue/test.desc new file mode 100644 index 00000000000..413f198cf36 --- /dev/null +++ b/regression/goto-gcc/builtin_va_end_lvalue/test.desc @@ -0,0 +1,10 @@ +KNOWNBUG +main.c + +^EXIT=1$ +^SIGNAL=0$ +argument expected to be lvalue +-- +-- +The C front-end should catch the problem during type checking, and not leave it +to goto-program conversion to detect the problem. diff --git a/regression/cbmc/builtin_va_end_one/main.c b/regression/goto-gcc/builtin_va_end_one/main.c similarity index 100% rename from regression/cbmc/builtin_va_end_one/main.c rename to regression/goto-gcc/builtin_va_end_one/main.c diff --git a/regression/cbmc/builtin_va_copy_two/test.desc b/regression/goto-gcc/builtin_va_end_one/test.desc similarity index 87% rename from regression/cbmc/builtin_va_copy_two/test.desc rename to regression/goto-gcc/builtin_va_end_one/test.desc index bca33a5dd6d..656aeffa3b3 100644 --- a/regression/cbmc/builtin_va_copy_two/test.desc +++ b/regression/goto-gcc/builtin_va_end_one/test.desc @@ -1,7 +1,7 @@ CORE main.c -^EXIT=6$ +^EXIT=1$ ^SIGNAL=0$ wrong number of function arguments -- diff --git a/regression/cbmc/builtin_va_start_lvalue/main.c b/regression/goto-gcc/builtin_va_start_lvalue/main.c similarity index 100% rename from regression/cbmc/builtin_va_start_lvalue/main.c rename to regression/goto-gcc/builtin_va_start_lvalue/main.c diff --git a/regression/goto-gcc/builtin_va_start_lvalue/test.desc b/regression/goto-gcc/builtin_va_start_lvalue/test.desc new file mode 100644 index 00000000000..413f198cf36 --- /dev/null +++ b/regression/goto-gcc/builtin_va_start_lvalue/test.desc @@ -0,0 +1,10 @@ +KNOWNBUG +main.c + +^EXIT=1$ +^SIGNAL=0$ +argument expected to be lvalue +-- +-- +The C front-end should catch the problem during type checking, and not leave it +to goto-program conversion to detect the problem. diff --git a/regression/cbmc/builtin_va_start_two/main.c b/regression/goto-gcc/builtin_va_start_two/main.c similarity index 100% rename from regression/cbmc/builtin_va_start_two/main.c rename to regression/goto-gcc/builtin_va_start_two/main.c diff --git a/regression/goto-gcc/builtin_va_start_two/test.desc b/regression/goto-gcc/builtin_va_start_two/test.desc new file mode 100644 index 00000000000..b1d2dbc1ab3 --- /dev/null +++ b/regression/goto-gcc/builtin_va_start_two/test.desc @@ -0,0 +1,10 @@ +KNOWNBUG +main.c + +^EXIT=1$ +^SIGNAL=0$ +expected to have two arguments +-- +-- +The C front-end should catch the problem during type checking, and not leave it +to goto-program conversion to detect the problem.