Add json/xml-interface to JBMC

Author: peterschrammel

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