Skip to content

Commit 651c6aa

Browse files
Add json-interface to CBMC
Allows reading the commandline in JSON format from stdin.
1 parent fd6e0e0 commit 651c6aa

File tree

6 files changed

+47
-1
lines changed

6 files changed

+47
-1
lines changed
Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
#include <assert.h>
2+
3+
void foo(int x)
4+
{
5+
for(int i = 0; i < 5; ++i)
6+
{
7+
if(x)
8+
assert(0);
9+
assert(0);
10+
}
11+
assert(0);
12+
}
Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
CORE broken-smt-backend
2+
--json-interface
3+
< test.json
4+
activate-multi-line-match
5+
^EXIT=10$
6+
^SIGNAL=0$
7+
Not unwinding loop foo\.0 iteration 3 file main\.c line 5 function foo thread 0
8+
\{\n\s*"description": "assertion 0",\n\s*"property": "foo\.assertion\.(1|3)",\n\s*"status": "SUCCESS"\n\s*\}
9+
\{\n\s*"description": "assertion 0",\n\s*"property": "foo\.assertion\.(1|3)",\n\s*"status": "FAILURE",\n\s*"trace": \[
10+
VERIFICATION FAILED
11+
--
12+
"property": "foo\.assertion\.2"
Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
{
2+
"arguments": [
3+
"main.c"
4+
],
5+
"options": {
6+
"function": "foo",
7+
"unwind": 3,
8+
"property": [
9+
"foo.assertion.1",
10+
"foo.assertion.3"
11+
],
12+
"trace": true,
13+
"show-properties": false
14+
}
15+
}

src/cbmc/cbmc_parse_options.cpp

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -79,6 +79,7 @@ Author: Daniel Kroening, [email protected]
7979

8080
#include <langapi/mode.h>
8181

82+
#include <json/json_interface.h>
8283
#include <xmllang/xml_interface.h>
8384

8485
#include "c_test_input_generator.h"
@@ -90,6 +91,7 @@ cbmc_parse_optionst::cbmc_parse_optionst(int argc, const char **argv)
9091
argv,
9192
std::string("CBMC ") + CBMC_VERSION)
9293
{
94+
json_interface(cmdline, ui_message_handler);
9395
xml_interface(cmdline, ui_message_handler);
9496
}
9597

@@ -103,6 +105,7 @@ ::cbmc_parse_optionst::cbmc_parse_optionst(
103105
argv,
104106
std::string("CBMC ") + CBMC_VERSION)
105107
{
108+
json_interface(cmdline, ui_message_handler);
106109
xml_interface(cmdline, ui_message_handler);
107110
}
108111

@@ -1021,6 +1024,7 @@ void cbmc_parse_optionst::help()
10211024
" --xml-ui use XML-formatted output\n"
10221025
" --xml-interface bi-directional XML interface\n"
10231026
" --json-ui use JSON-formatted output\n"
1027+
" --json-interface bi-directional JSON interface\n"
10241028
// NOLINTNEXTLINE(whitespace/line_length)
10251029
HELP_VALIDATE
10261030
HELP_GOTO_TRACE

src/cbmc/cbmc_parse_options.h

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -47,7 +47,9 @@ class optionst;
4747
"(object-bits):" \
4848
OPT_GOTO_CHECK \
4949
"(no-assertions)(no-assumptions)" \
50-
"(xml-ui)(xml-interface)(json-ui)" \
50+
"(xml-ui)(xml-interface)" \
51+
"(json-interface)" \
52+
"(json-ui)" \
5153
"(smt1)(smt2)(fpa)(cvc3)(cvc4)(boolector)(yices)(z3)(mathsat)" \
5254
"(cprover-smt2)" \
5355
"(no-sat-preprocessor)" \

src/cbmc/module_dependencies.txt

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -7,6 +7,7 @@ goto-instrument
77
goto-programs
88
goto-symex
99
jsil
10+
json
1011
json-symtab-language
1112
langapi # should go away
1213
linking

0 commit comments

Comments
 (0)