Merge pull request #4588 from peterschrammel/json-interface-jbmc

Add json/xml-interface to JBMC

Author: smowton

jbmc/src/jbmc/jbmc_parse_options.cpp

@@ -81,6 +81,8 @@ jbmc_parse_optionst::jbmc_parse_optionst(int argc, const char **argv)
       argv,
       std::string("JBMC ") + CBMC_VERSION)
 {
+  json_interface(cmdline, ui_message_handler);
+  xml_interface(cmdline, ui_message_handler);
 }
 
 ::jbmc_parse_optionst::jbmc_parse_optionst(
@@ -93,6 +95,8 @@ ::jbmc_parse_optionst::jbmc_parse_optionst(
       argv,
       std::string("JBMC ") + CBMC_VERSION)
 {
+  json_interface(cmdline, ui_message_handler);
+  xml_interface(cmdline, ui_message_handler);
 }
 
 void jbmc_parse_optionst::set_default_options(optionst &options)
@@ -1090,8 +1094,8 @@ void jbmc_parse_optionst::help()
     "\n"
     "Other options:\n"
     " --version                    show version and exit\n"
-    " --xml-ui                     use XML-formatted output\n"
-    " --json-ui                    use JSON-formatted output\n"
+    HELP_XML_INTERFACE
+    HELP_JSON_INTERFACE
     HELP_VALIDATE
     HELP_GOTO_TRACE
     HELP_FLUSH

jbmc/src/jbmc/jbmc_parse_options.h

@@ -34,6 +34,9 @@ Author: Daniel Kroening, [email protected]
 
 #include <java_bytecode/java_bytecode_language.h>
 
+#include <json/json_interface.h>
+#include <xmllang/xml_interface.h>
+
 class goto_functionst;
 class optionst;
 
@@ -49,7 +52,8 @@ class optionst;
   "(object-bits):" \
   "(classpath):(cp):(main-class):" \
   "(no-assertions)(no-assumptions)" \
-  "(xml-ui)(json-ui)" \
+  OPT_XML_INTERFACE \
+  OPT_JSON_INTERFACE \
   "(smt1)(smt2)(fpa)(cvc3)(cvc4)(boolector)(yices)(z3)(mathsat)" \
   "(no-sat-preprocessor)" \
   "(beautify)" \

jbmc/src/jbmc/module_dependencies.txt

@@ -6,6 +6,7 @@ goto-programs
 goto-symex
 java_bytecode
 jbmc
+json
 langapi # should go away
 linking
 pointer-analysis
@@ -15,3 +16,4 @@ solvers/prop
 solvers/sat
 solvers/strings
 util
+xmllang

src/cbmc/cbmc_parse_options.cpp

@@ -79,9 +79,6 @@ Author: Daniel Kroening, [email protected]
 
 #include <langapi/mode.h>
 
-#include <json/json_interface.h>
-#include <xmllang/xml_interface.h>
-
 #include "c_test_input_generator.h"
 
 cbmc_parse_optionst::cbmc_parse_optionst(int argc, const char **argv)
@@ -1021,11 +1018,8 @@ void cbmc_parse_optionst::help()
     "\n"
     "Other options:\n"
     " --version                    show version and exit\n"
-    " --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_XML_INTERFACE
+    HELP_JSON_INTERFACE
     HELP_VALIDATE
     HELP_GOTO_TRACE
     HELP_FLUSH

src/cbmc/cbmc_parse_options.h

@@ -31,6 +31,9 @@ Author: Daniel Kroening, [email protected]
 
 #include <solvers/strings/string_refinement.h>
 
+#include <json/json_interface.h>
+#include <xmllang/xml_interface.h>
+
 class goto_functionst;
 class optionst;
 
@@ -47,9 +50,8 @@ class optionst;
   "(object-bits):" \
   OPT_GOTO_CHECK \
   "(no-assertions)(no-assumptions)" \
-  "(xml-ui)(xml-interface)" \
-  "(json-interface)" \
-  "(json-ui)" \
+  OPT_XML_INTERFACE \
+  OPT_JSON_INTERFACE \
   "(smt1)(smt2)(fpa)(cvc3)(cvc4)(boolector)(yices)(z3)(mathsat)" \
   "(cprover-smt2)" \
   "(no-sat-preprocessor)" \

src/json/json_interface.h

@@ -37,4 +37,14 @@ class message_handlert;
 /// \endcode
 void json_interface(cmdlinet &, message_handlert &);
 
+// clang-format off
+#define OPT_JSON_INTERFACE \
+  "(json-ui)" \
+  "(json-interface)"
+
+#define HELP_JSON_INTERFACE \
+  " --json-ui                     use JSON-formatted output\n" \
+  " --json-interface              bi-directional JSON interface\n"
+// clang-format on
+
 #endif // CPROVER_JSON_JSON_INTERFACE_H

src/xmllang/xml_interface.h

@@ -31,4 +31,14 @@ class message_handlert;
 /// \endcode
 void xml_interface(cmdlinet &, message_handlert &);
 
+// clang-format off
+#define OPT_XML_INTERFACE \
+  "(xml-ui)" \
+  "(xml-interface)"
+
+#define HELP_XML_INTERFACE \
+  " --xml-ui                     use XML-formatted output\n" \
+  " --xml-interface              bi-directional XML interface\n"
+// clang-format on
+
 #endif // CPROVER_XMLLANG_XML_INTERFACE_H