Add json-interface to CBMC

Allows reading the commandline in JSON format
from stdin.

Author: peterschrammel

regression/cbmc/json-interface1/main.c

@@ -0,0 +1,12 @@
+#include <assert.h>
+
+void foo(int x)
+{
+  for(int i = 0; i < 5; ++i)
+  {
+    if(x)
+      assert(0);
+    assert(0);
+  }
+  assert(0);
+}

regression/cbmc/json-interface1/test.desc

@@ -0,0 +1,12 @@
+CORE broken-smt-backend
+--json-interface
+< test.json
+activate-multi-line-match
+^EXIT=10$
+^SIGNAL=0$
+Not unwinding loop foo\.0 iteration 3 file main\.c line 5 function foo thread 0
+\{\n\s*"description": "assertion 0",\n\s*"property": "foo\.assertion\.(1|3)",\n\s*"status": "SUCCESS"\n\s*\}
+\{\n\s*"description": "assertion 0",\n\s*"property": "foo\.assertion\.(1|3)",\n\s*"status": "FAILURE",\n\s*"trace": \[
+VERIFICATION FAILED
+--
+"property": "foo\.assertion\.2"

regression/cbmc/json-interface1/test.json

@@ -0,0 +1,15 @@
+{
+  "arguments": [
+    "main.c"
+  ],
+  "options": {
+    "function": "foo",
+    "unwind": 3,
+    "property": [
+      "foo.assertion.1",
+      "foo.assertion.3"
+    ],
+    "trace": true,
+    "show-properties": false
+  }	
+}

src/cbmc/cbmc_parse_options.cpp

@@ -79,6 +79,8 @@ Author: Daniel Kroening, [email protected]
 
 #include <langapi/mode.h>
 
+#include <json/json_interface.h>
+
 #include "c_test_input_generator.h"
 #include "xml_interface.h"
 
@@ -90,6 +92,7 @@ cbmc_parse_optionst::cbmc_parse_optionst(int argc, const char **argv)
       std::string("CBMC ") + CBMC_VERSION),
     xml_interfacet(cmdline)
 {
+  json_interface(cmdline, ui_message_handler);
 }
 
 ::cbmc_parse_optionst::cbmc_parse_optionst(
@@ -103,6 +106,7 @@ ::cbmc_parse_optionst::cbmc_parse_optionst(
       std::string("CBMC ") + CBMC_VERSION),
     xml_interfacet(cmdline)
 {
+  json_interface(cmdline, ui_message_handler);
 }
 
 void cbmc_parse_optionst::set_default_options(optionst &options)
@@ -1030,6 +1034,7 @@ void cbmc_parse_optionst::help()
     " --xml-ui                     use XML-formatted output\n"
     " --xml-interface              bi-directional XML interface\n"
     " --json-ui                    use JSON-formatted output\n"
+    " --json-interface             bi-directional JSON interface\n"
     // NOLINTNEXTLINE(whitespace/line_length)
     HELP_VALIDATE
     HELP_GOTO_TRACE

src/cbmc/cbmc_parse_options.h

@@ -49,7 +49,9 @@ class optionst;
   "(object-bits):" \
   OPT_GOTO_CHECK \
   "(no-assertions)(no-assumptions)" \
-  "(xml-ui)(xml-interface)(json-ui)" \
+  "(xml-ui)(xml-interface)" \
+  "(json-interface)" \
+  "(json-ui)" \
   "(smt1)(smt2)(fpa)(cvc3)(cvc4)(boolector)(yices)(z3)(mathsat)" \
   "(cprover-smt2)" \
   "(no-sat-preprocessor)" \

src/cbmc/module_dependencies.txt

@@ -7,6 +7,7 @@ goto-instrument
 goto-programs
 goto-symex
 jsil
+json
 json-symtab-language
 langapi # should go away
 linking