Output options in JBMC

Author: peterschrammel

jbmc/regression/jbmc/output-options/Main.class

@@ -0,0 +1,6 @@
+public class Main {
+  public static void main(String[] args) {
+    for(String arg : args) {
+    }
+  }
+}

jbmc/regression/jbmc/output-options/Main.java

@@ -0,0 +1,23 @@
+CORE symex-driven-lazy-loading-expected-failure
+Main.class
+--verbosity 10 --unwind 2 --disable-uncaught-exception-check --throw-assertion-error
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+assertions: "1"
+assumptions: "1"
+java-threading: "0"
+lazy-methods: "1"
+propagation: "1"
+refine-strings: "1"
+sat-preprocessor: "1"
+simplify: "1"
+simplify-if: "1"
+symex-driven-lazy-loading: "0"
+throw-assertion-error: "1"
+throw-runtime-exceptions: "0"
+uncaught-exception-check: "0"
+unwind: "2"
+--
+--
+Symex-driven lazy loading would expect symex-driven-lazy-loading: "1".

jbmc/regression/jbmc/output-options/test.desc

@@ -20,6 +20,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/exit_codes.h>
 #include <util/invariant.h>
 #include <util/unicode.h>
+#include <util/xml.h>
 #include <util/version.h>
 
 #include <langapi/language.h>
@@ -422,6 +423,28 @@ int jbmc_parse_optionst::doit()
            << "-bit " << config.this_architecture() << " "
            << config.this_operating_system() << eom;
 
+  // output the options
+  switch(ui_message_handler.get_ui())
+  {
+    case ui_message_handlert::uit::PLAIN:
+      conditional_output(debug(), [&options](messaget::mstreamt &mstream) {
+        mstream << "\nOptions: \n";
+        options.output(mstream);
+        mstream << messaget::eom;
+      });
+      break;
+    case ui_message_handlert::uit::JSON_UI:
+    {
+      json_objectt json_options;
+      json_options["options"] = options.to_json();
+      debug() << json_options;
+      break;
+    }
+    case ui_message_handlert::uit::XML_UI:
+      debug() << options.to_xml();
+      break;
+  }
+
   register_language(new_ansi_c_language);
   register_language(new_java_bytecode_language);