Skip to content

Commit 1359349

Browse files
committed
Testing error conditions in builtin_functions.cpp works
64c5d86 introduced the tests as KNOWNBUG, even though they always worked as described in their test specification. What is possibly buggy about them is the hope that the errors would be caught earlier, but the C front-end already does warn that the declaration is missing.
1 parent 0be893f commit 1359349

File tree

7 files changed

+14
-7
lines changed

7 files changed

+14
-7
lines changed

regression/cbmc/assert_func_four/test.desc

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,7 @@
1-
KNOWNBUG
1+
CORE
22
main.c
33

4+
function .* is not declared
45
^EXIT=6$
56
^SIGNAL=0$
67
expected to have four arguments

regression/cbmc/assert_lhs/test.desc

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,7 @@
1-
KNOWNBUG
1+
CORE
22
main.c
33

4+
function .* is not declared
45
^EXIT=6$
56
^SIGNAL=0$
67
expected not to have LHS

regression/cbmc/assert_one/test.desc

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,7 @@
1-
KNOWNBUG
1+
CORE
22
main.c
33

4+
function .* is not declared
45
^EXIT=6$
56
^SIGNAL=0$
67
expected to have one argument

regression/cbmc/assert_rtn_four/test.desc

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,7 @@
1-
KNOWNBUG
1+
CORE
22
main.c
33

4+
function .* is not declared
45
^EXIT=6$
56
^SIGNAL=0$
67
expected to have four arguments

regression/cbmc/gcc_builtin_va_arg_one/test.desc

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,7 @@
1-
KNOWNBUG
1+
CORE
22
main.c
33

4+
function .* is not declared
45
^EXIT=6$
56
^SIGNAL=0$
67
expected to have one argument

regression/cbmc/verifier_error_lhs/test.desc

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,7 @@
1-
KNOWNBUG
1+
CORE
22
main.c
33

4+
function .* is not declared
45
^EXIT=6$
56
^SIGNAL=0$
67
expected not to have LHS

regression/cbmc/verifier_error_zero/test.desc

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,7 @@
1-
KNOWNBUG
1+
CORE
22
main.c
33

4+
function .* is not declared
45
^EXIT=6$
56
^SIGNAL=0$
67
expected to have no arguments

0 commit comments

Comments
 (0)