Skip to content

Commit 2cdd3ee

Browse files
author
Daniel Kroening
committed
add two tests for error reporting when using --json-ui
Error-reporting is important, yet undertested, as shown by #3897.
1 parent e12c7ee commit 2cdd3ee

File tree

4 files changed

+30
-0
lines changed

4 files changed

+30
-0
lines changed

regression/cbmc/json-ui/no_entry.c

+4
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,4 @@
1+
int I_am_not_main()
2+
{
3+
return 0;
4+
}

regression/cbmc/json-ui/no_entry.desc

+10
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
KNOWNBUG
2+
no_entry.c
3+
--json-ui
4+
activate-multi-line-match
5+
^EXIT=6$
6+
^SIGNAL=0$
7+
"messageText": "the program has no entry point",[\n ]*"messageType": "ERROR",
8+
--
9+
^warning: ignoring
10+
^VERIFICATION SUCCESSFUL$
+6
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
int main()
2+
{
3+
// clang-format off
4+
I AM A SYNTAX ERROR
5+
return 0;
6+
}
+10
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
KNOWNBUG
2+
syntax_error.c
3+
--json-ui
4+
activate-multi-line-match
5+
^EXIT=6$
6+
^SIGNAL=0$
7+
"messageText": "syntax error before .*",[\n ]*"messageType": "ERROR",[\n ]*"sourceLocation": {[\n ]*"file": "syntax_error.c",[\n ]*"function": "main",[\n ]*"line": "4",
8+
--
9+
^warning: ignoring
10+
^VERIFICATION SUCCESSFUL$

0 commit comments

Comments
 (0)