JSON output for the properties

regression/ebmc/CLI/json-properties.desc

@@ -0,0 +1,18 @@
+CORE
+json-properties.v
+--json-properties -
+activate-multi-line-match
+\[
+  \{
+    "description": "",
+    "location": \{
+      "file": "json-properties\.v",
+      "line": "3",
+      "workingDirectory": ".*"
+    \},
+    "name": "main\.property\.p0"
+  \}
+\]
+^EXIT=0$
+^SIGNAL=0$
+--

regression/ebmc/CLI/json-properties.v

@@ -0,0 +1,5 @@
+module main;
+
+  always assert p0: 1 == 2;
+
+endmodule

src/ebmc/ebmc_base.cpp

@@ -338,6 +338,12 @@ int ebmc_baset::get_properties()
     return 0;
   }
 
+  if(cmdline.isset("json-properties"))
+  {
+    json_properties(cmdline.get_value("json-properties"));
+    return 0;
+  }
+
   return -1; // done
 }
 

src/ebmc/ebmc_base.h

@@ -52,6 +52,7 @@ class ebmc_baset
   bool parse_property(const std::string &property);
   bool get_model_properties();
   void show_properties();
+  void json_properties(const std::string &file_name);
 
   bool parse();
   bool parse(const std::string &filename);

src/ebmc/ebmc_parse_options.h

@@ -32,7 +32,8 @@ class ebmc_parse_optionst:public parse_options_baset
         "(show-properties)(property):p:(trace)(waveform)(numbered-trace)"
         "(dimacs)(module):(top):"
         "(po)(cegar)(k-induction)(2pi)(bound2):"
-        "(outfile):(xml-ui)(verbosity):(gui)(json-result):"
+        "(outfile):(xml-ui)(verbosity):(gui)"
+        "(json-result):(json-properties):"
         "(neural-liveness)(neural-engine):"
         "(reset):"
         "(version)(verilog-rtl)(verilog-netlist)"

src/ebmc/show_properties.cpp

@@ -6,12 +6,16 @@ Author: Daniel Kroening, kroening@kroening.com
 
 \*******************************************************************/
 
-#include <iostream>
-
+#include <util/json.h>
+#include <util/json_irep.h>
+#include <util/unicode.h>
 #include <util/xml.h>
 #include <util/xml_irep.h>
 
 #include "ebmc_base.h"
+#include "ebmc_error.h"
+
+#include <iostream>
 
 /*******************************************************************\
 
@@ -62,3 +66,46 @@ void ebmc_baset::show_properties()
     p_nr++;
   }
 }
+
+/*******************************************************************\
+
+Function: ebmc_baset::json_properties
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void ebmc_baset::json_properties(const std::string &file_name)
+{
+  json_arrayt json;
+
+  for(const auto &p : properties.properties)
+  {
+    json_objectt json_property;
+    json_property["identifier"] = json_stringt{id2string(p.identifier)};
+    json_property["name"] = json_stringt{id2string(p.name)};
+    json_property["description"] = json_stringt{p.description};
+
+    if(p.location.is_not_nil())
+      json_property["location"] = ::json(p.location);
+
+    json.push_back(std::move(json_property));
+  }
+
+  if(file_name == "-")
+  {
+    std::cout << json;
+  }
+  else
+  {
+    std::ofstream out(widen_if_needed(file_name));
+    if(!out)
+      throw ebmc_errort() << "failed to open " << file_name;
+
+    out << json;
+  }
+}