diff --git a/regression/cbmc/json-ui/no_entry.c b/regression/cbmc/json-ui/no_entry.c new file mode 100644 index 00000000000..8fa576f8d0f --- /dev/null +++ b/regression/cbmc/json-ui/no_entry.c @@ -0,0 +1,4 @@ +int I_am_not_main() +{ + return 0; +} diff --git a/regression/cbmc/json-ui/no_entry.desc b/regression/cbmc/json-ui/no_entry.desc new file mode 100644 index 00000000000..949d5e73631 --- /dev/null +++ b/regression/cbmc/json-ui/no_entry.desc @@ -0,0 +1,10 @@ +KNOWNBUG +no_entry.c +--json-ui +activate-multi-line-match +^EXIT=6$ +^SIGNAL=0$ +"messageText": "the program has no entry point",[\n ]*"messageType": "ERROR", +-- +^warning: ignoring +^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc/json-ui/syntax_error.c b/regression/cbmc/json-ui/syntax_error.c new file mode 100644 index 00000000000..a62f57f3656 --- /dev/null +++ b/regression/cbmc/json-ui/syntax_error.c @@ -0,0 +1,6 @@ +int main() +{ + // clang-format off + I AM A SYNTAX ERROR + return 0; +} diff --git a/regression/cbmc/json-ui/syntax_error.desc b/regression/cbmc/json-ui/syntax_error.desc new file mode 100644 index 00000000000..7c35f907dfb --- /dev/null +++ b/regression/cbmc/json-ui/syntax_error.desc @@ -0,0 +1,10 @@ +KNOWNBUG +syntax_error.c +--json-ui +activate-multi-line-match +^EXIT=6$ +^SIGNAL=0$ +"messageText": "syntax error before .*",[\n ]*"messageType": "ERROR",[\n ]*"sourceLocation": {[\n ]*"file": "syntax_error.c",[\n ]*"function": "main",[\n ]*"line": "4", +-- +^warning: ignoring +^VERIFICATION SUCCESSFUL$