From 25de48d9fdcb079c2f1648156e9ca355e71de5c3 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 21 Dec 2018 09:03:00 +0000 Subject: [PATCH] Move regression tests of the C front-end to a suitable folder There is no bounded model checking expected or required by these tests, and also they use GCC-specific built-ins. There is still work left to be done, so most remain KNOWNBUG (but now the reason thereof is explained). --- regression/cbmc/builtin_is/test.desc | 7 ------- regression/cbmc/builtin_va_copy_lvalue/test.desc | 7 ------- regression/cbmc/builtin_va_end_lvalue/test.desc | 7 ------- regression/cbmc/builtin_va_start_lvalue/test.desc | 7 ------- regression/cbmc/builtin_va_start_two/test.desc | 7 ------- regression/{cbmc => goto-gcc}/builtin_is/main.c | 0 regression/goto-gcc/builtin_is/test.desc | 10 ++++++++++ .../{cbmc => goto-gcc}/builtin_va_copy_lvalue/main.c | 0 regression/goto-gcc/builtin_va_copy_lvalue/test.desc | 10 ++++++++++ .../{cbmc => goto-gcc}/builtin_va_copy_two/main.c | 0 .../builtin_va_copy_two}/test.desc | 2 +- .../{cbmc => goto-gcc}/builtin_va_end_lvalue/main.c | 0 regression/goto-gcc/builtin_va_end_lvalue/test.desc | 10 ++++++++++ .../{cbmc => goto-gcc}/builtin_va_end_one/main.c | 0 .../builtin_va_end_one}/test.desc | 2 +- .../{cbmc => goto-gcc}/builtin_va_start_lvalue/main.c | 0 regression/goto-gcc/builtin_va_start_lvalue/test.desc | 10 ++++++++++ .../{cbmc => goto-gcc}/builtin_va_start_two/main.c | 0 regression/goto-gcc/builtin_va_start_two/test.desc | 10 ++++++++++ 19 files changed, 52 insertions(+), 37 deletions(-) delete mode 100644 regression/cbmc/builtin_is/test.desc delete mode 100644 regression/cbmc/builtin_va_copy_lvalue/test.desc delete mode 100644 regression/cbmc/builtin_va_end_lvalue/test.desc delete mode 100644 regression/cbmc/builtin_va_start_lvalue/test.desc delete mode 100644 regression/cbmc/builtin_va_start_two/test.desc rename regression/{cbmc => goto-gcc}/builtin_is/main.c (100%) create mode 100644 regression/goto-gcc/builtin_is/test.desc rename regression/{cbmc => goto-gcc}/builtin_va_copy_lvalue/main.c (100%) create mode 100644 regression/goto-gcc/builtin_va_copy_lvalue/test.desc rename regression/{cbmc => goto-gcc}/builtin_va_copy_two/main.c (100%) rename regression/{cbmc/builtin_va_end_one => goto-gcc/builtin_va_copy_two}/test.desc (87%) rename regression/{cbmc => goto-gcc}/builtin_va_end_lvalue/main.c (100%) create mode 100644 regression/goto-gcc/builtin_va_end_lvalue/test.desc rename regression/{cbmc => goto-gcc}/builtin_va_end_one/main.c (100%) rename regression/{cbmc/builtin_va_copy_two => goto-gcc/builtin_va_end_one}/test.desc (87%) rename regression/{cbmc => goto-gcc}/builtin_va_start_lvalue/main.c (100%) create mode 100644 regression/goto-gcc/builtin_va_start_lvalue/test.desc rename regression/{cbmc => goto-gcc}/builtin_va_start_two/main.c (100%) create mode 100644 regression/goto-gcc/builtin_va_start_two/test.desc 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.