ebmc: replace ebmc_baset in main flow

src/ebmc/ebmc_base.cpp

@@ -56,18 +56,6 @@ int ebmc_baset::get_properties()
   properties = ebmc_propertiest::from_command_line(
     cmdline, transition_system, message.get_message_handler());
 
-  if(cmdline.isset("show-properties"))
-  {
-    show_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

@@ -47,8 +47,6 @@ 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.cpp

@@ -24,6 +24,7 @@ Author: Daniel Kroening, [email protected]
 #include "property_checker.h"
 #include "random_traces.h"
 #include "ranking_function.h"
+#include "show_properties.h"
 #include "show_trans.h"
 
 #include <iostream>
@@ -210,94 +211,97 @@ int ebmc_parse_optionst::doit()
     // get the transition system
     auto transition_system = get_transition_system(cmdline, ui_message_handler);
 
+    // get the properties
+    auto properties = ebmc_propertiest::from_command_line(
+      cmdline, transition_system, ui_message_handler);
+
+    if(cmdline.isset("show-properties"))
+    {
+      show_properties(properties, ui_message_handler);
+      return 0;
+    }
+
+    if(cmdline.isset("json-properties"))
+    {
+      json_properties(properties, cmdline.get_value("json-properties"));
+      return 0;
+    }
+
+    // possibly apply liveness-to-safety
+    if(cmdline.isset("liveness-to-safety"))
+      liveness_to_safety(transition_system, properties);
+
+    if(cmdline.isset("show-varmap"))
+    {
+      auto netlist =
+        make_netlist(transition_system, properties, ui_message_handler);
+      netlist.var_map.output(std::cout);
+      return 0;
+    }
+
+    if(cmdline.isset("show-ldg"))
     {
       ebmc_baset ebmc_base(cmdline, ui_message_handler);
       ebmc_base.transition_system = std::move(transition_system);
+      ebmc_base.properties = std::move(properties);
+      ebmc_base.show_ldg(std::cout);
+      return 0;
+    }
+
+    if(cmdline.isset("show-netlist"))
+    {
+      auto netlist =
+        make_netlist(transition_system, properties, ui_message_handler);
+      netlist.print(std::cout);
+      return 0;
+    }
+
+    if(cmdline.isset("dot-netlist"))
+    {
+      auto netlist =
+        make_netlist(transition_system, properties, ui_message_handler);
+      auto filename = cmdline.value_opt("outfile").value_or("-");
+      output_filet outfile{filename};
+      outfile.stream() << "digraph netlist {\n";
+      netlist.output_dot(outfile.stream());
+      outfile.stream() << "}\n";
+      return 0;
+    }
+
+    if(cmdline.isset("smv-netlist"))
+    {
+      auto netlist =
+        make_netlist(transition_system, properties, ui_message_handler);
+      auto filename = cmdline.value_opt("outfile").value_or("-");
+      output_filet outfile{filename};
+      outfile.stream() << "-- Generated by EBMC " << EBMC_VERSION << '\n';
+      outfile.stream() << "-- Generated from "
+                       << transition_system.main_symbol->name << '\n';
+      outfile.stream() << '\n';
+      netlist.output_smv(outfile.stream());
+      return 0;
+    }
 
-      auto result = ebmc_base.get_properties();
-
-      if(result != -1)
-        return result;
-
-      // possibly apply liveness-to-safety
-      if(cmdline.isset("liveness-to-safety"))
-        liveness_to_safety(ebmc_base.transition_system, ebmc_base.properties);
-
-      if(cmdline.isset("show-varmap"))
-      {
-        netlistt netlist;
-        if(ebmc_base.make_netlist(netlist))
-          return 1;
-        netlist.var_map.output(std::cout);
-        return 0;
-      }
-
-      if(cmdline.isset("show-ldg"))
-      {
-        ebmc_base.show_ldg(std::cout);
-        return 0;
-      }
-
-      if(cmdline.isset("show-netlist"))
-      {
-        netlistt netlist;
-        if(ebmc_base.make_netlist(netlist))
-          return 1;
-        netlist.print(std::cout);
-        return 0;
-      }
-
-      if(cmdline.isset("dot-netlist"))
-      {
-        netlistt netlist;
-        if(ebmc_base.make_netlist(netlist))
-          return 1;
-        auto filename = cmdline.value_opt("outfile").value_or("-");
-        output_filet outfile{filename};
-        outfile.stream() << "digraph netlist {\n";
-        netlist.output_dot(outfile.stream());
-        outfile.stream() << "}\n";
-        return 0;
-      }
-
-      if(cmdline.isset("smv-netlist"))
-      {
-        netlistt netlist;
-        if(ebmc_base.make_netlist(netlist))
-          return 1;
-        auto filename = cmdline.value_opt("outfile").value_or("-");
-        output_filet outfile{filename};
-        outfile.stream() << "-- Generated by EBMC " << EBMC_VERSION << '\n';
-        outfile.stream() << "-- Generated from "
-                         << ebmc_base.transition_system.main_symbol->name
-                         << '\n';
-        outfile.stream() << '\n';
-        netlist.output_smv(outfile.stream());
-        return 0;
-      }
-
-      if(cmdline.isset("cegar"))
-      {
-        auto netlist = make_netlist(
-          ebmc_base.transition_system,
-          ebmc_base.properties,
-          ui_message_handler);
-        const namespacet ns(ebmc_base.transition_system.symbol_table);
-        return do_bmc_cegar(
-          netlist, ebmc_base.properties, ns, ui_message_handler);
-      }
-
-      if(cmdline.isset("compute-ct"))
-        return ebmc_base.do_compute_ct();
-
-      auto checker_result = property_checker(
-        cmdline,
-        ebmc_base.transition_system,
-        ebmc_base.properties,
-        ui_message_handler);
-
-      return checker_result.exit_code();
+    if(cmdline.isset("cegar"))
+    {
+      auto netlist =
+        make_netlist(transition_system, properties, ui_message_handler);
+      const namespacet ns(transition_system.symbol_table);
+      return do_bmc_cegar(netlist, properties, ns, ui_message_handler);
     }
+
+    if(cmdline.isset("compute-ct"))
+    {
+      ebmc_baset ebmc_base(cmdline, ui_message_handler);
+      ebmc_base.transition_system = std::move(transition_system);
+      ebmc_base.properties = std::move(properties);
+      return ebmc_base.do_compute_ct();
+    }
+
+    auto checker_result = property_checker(
+      cmdline, transition_system, properties, ui_message_handler);
+
+    return checker_result.exit_code();
   }
   catch(const ebmc_errort &ebmc_error)
   {

src/ebmc/show_properties.cpp

@@ -1,25 +1,27 @@
 /*******************************************************************\
 
-Module: Base for Verification Modules
+Module: Show Properties
 
 Author: Daniel Kroening, [email protected]
 
 \*******************************************************************/
 
+#include "show_properties.h"
+
 #include <util/json.h>
 #include <util/json_irep.h>
 #include <util/xml.h>
 #include <util/xml_irep.h>
 
-#include "ebmc_base.h"
 #include "ebmc_error.h"
+#include "ebmc_properties.h"
 #include "output_file.h"
 
 #include <iostream>
 
 /*******************************************************************\
 
-Function: ebmc_baset::show_properties
+Function: show_properties
 
   Inputs:
 
@@ -29,7 +31,9 @@ Function: ebmc_baset::show_properties
 
 \*******************************************************************/
 
-void ebmc_baset::show_properties()
+void show_properties(
+  const ebmc_propertiest &properties,
+  ui_message_handlert &message_handler)
 {
   unsigned p_nr=1;
 
@@ -49,8 +53,7 @@ void ebmc_baset::show_properties()
 
   for(const auto &p : properties.properties)
   {
-    switch(static_cast<ui_message_handlert &>(message.get_message_handler())
-             .get_ui())
+    switch(message_handler.get_ui())
     {
     case ui_message_handlert::uit::XML_UI:
       std::cout << make_xml(p, p_nr) << '\n';
@@ -70,7 +73,7 @@ void ebmc_baset::show_properties()
 
 /*******************************************************************\
 
-Function: ebmc_baset::json_properties
+Function: json_properties
 
   Inputs:
 
@@ -80,7 +83,9 @@ Function: ebmc_baset::json_properties
 
 \*******************************************************************/
 
-void ebmc_baset::json_properties(const std::string &file_name)
+void json_properties(
+  const ebmc_propertiest &properties,
+  const std::string &file_name)
 {
   json_arrayt json;
 

src/ebmc/show_properties.h

@@ -0,0 +1,20 @@
+/*******************************************************************\
+
+Module: Show Properties
+
+Author: Daniel Kroening, [email protected]
+
+\*******************************************************************/
+
+#ifndef CPROVER_EBMC_SHOW_PROPERTIES_H
+#define CPROVER_EBMC_SHOW_PROPERTIES_H
+
+#include <string>
+
+class ebmc_propertiest;
+class ui_message_handlert;
+
+void show_properties(const ebmc_propertiest &, ui_message_handlert &);
+void json_properties(const ebmc_propertiest &, const std::string &file_name);
+
+#endif