diffblue · tautschnig · Jan 2, 2019 · Dec 21, 2018
diff --git a/regression/cbmc/builtin_is/test.desc b/regression/cbmc/builtin_is/test.desc
diff --git a/regression/cbmc/builtin_va_copy_lvalue/test.desc b/regression/cbmc/builtin_va_copy_lvalue/test.desc
diff --git a/regression/cbmc/builtin_va_end_lvalue/test.desc b/regression/cbmc/builtin_va_end_lvalue/test.desc
diff --git a/regression/cbmc/builtin_va_start_lvalue/test.desc b/regression/cbmc/builtin_va_start_lvalue/test.desc
diff --git a/regression/cbmc/builtin_va_start_two/test.desc b/regression/cbmc/builtin_va_start_two/test.desc
diff --git a/regression/cbmc/builtin_is/main.c → regression/goto-gcc/builtin_is/main.c b/regression/cbmc/builtin_is/main.c → 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
@@ -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/...ession/cbmc/builtin_va_copy_lvalue/main.c → ...on/goto-gcc/builtin_va_copy_lvalue/main.c b/...ession/cbmc/builtin_va_copy_lvalue/main.c → ...on/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
@@ -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 → ...ssion/goto-gcc/builtin_va_copy_two/main.c b/regression/cbmc/builtin_va_copy_two/main.c → ...ssion/goto-gcc/builtin_va_copy_two/main.c
diff --git a/regression/cbmc/builtin_va_end_one/test.desc → ...on/goto-gcc/builtin_va_copy_two/test.desc b/regression/cbmc/builtin_va_end_one/test.desc → ...on/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 → ...ion/goto-gcc/builtin_va_end_lvalue/main.c b/regression/cbmc/builtin_va_end_lvalue/main.c → ...ion/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
@@ -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 → ...ession/goto-gcc/builtin_va_end_one/main.c b/regression/cbmc/builtin_va_end_one/main.c → ...ession/goto-gcc/builtin_va_end_one/main.c
diff --git a/...ession/cbmc/builtin_va_copy_two/test.desc → ...ion/goto-gcc/builtin_va_end_one/test.desc b/...ession/cbmc/builtin_va_copy_two/test.desc → ...ion/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/...ssion/cbmc/builtin_va_start_lvalue/main.c → ...n/goto-gcc/builtin_va_start_lvalue/main.c b/...ssion/cbmc/builtin_va_start_lvalue/main.c → ...n/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
@@ -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 → ...sion/goto-gcc/builtin_va_start_two/main.c b/regression/cbmc/builtin_va_start_two/main.c → ...sion/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
@@ -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.