introduce property_checker_resultt

src/ebmc/bdd_engine.cpp

@@ -22,8 +22,6 @@ Author: Daniel Kroening, [email protected]
 #include <trans-netlist/unwind_netlist.h>
 #include <verilog/sva_expr.h>
 
-#include "report_results.h"
-
 #include <algorithm>
 #include <iostream>
 
@@ -51,7 +49,7 @@ class bdd_enginet
   {
   }
 
-  int operator()();
+  property_checker_resultt operator()();
 
 protected:
   using propertiest = ebmc_propertiest;
@@ -173,7 +171,7 @@ Function: bdd_enginet::operator()
 
 \*******************************************************************/
 
-int bdd_enginet::operator()()
+property_checker_resultt bdd_enginet::operator()()
 {
   try
   {
@@ -216,30 +214,29 @@ int bdd_enginet::operator()()
       }
 
       std::cout << '\n';
-        
-      return 0;
+
+      return property_checker_resultt::SUCCESS;
     }
 
     if(properties.properties.empty())
     {
       message.error() << "no properties" << messaget::eom;
-      return 1;
+      return property_checker_resultt::ERROR;
     }
 
     for(propertyt &p : properties.properties)
       check_property(p);
 
-    report_results(cmdline, properties, ns, message.get_message_handler());
-    return properties.exit_code();
+    return property_checker_resultt::VERIFICATION_RESULT;
   }
   catch(const char *error_msg)
   {
     message.error() << error_msg << messaget::eom;
-    return 1;
+    return property_checker_resultt::ERROR;
   }
   catch(int)
   {
-    return 1;
+    return property_checker_resultt::ERROR;
   }
 }
 
@@ -1002,7 +999,7 @@ Function: bdd_engine
 
 \*******************************************************************/
 
-int bdd_engine(
+property_checker_resultt bdd_engine(
   const cmdlinet &cmdline,
   transition_systemt &transition_system,
   ebmc_propertiest &properties,

src/ebmc/bdd_engine.h

@@ -9,12 +9,9 @@ Author: Daniel Kroening, [email protected]
 #ifndef CPROVER_EBMC_BDD_ENGINE_H
 #define CPROVER_EBMC_BDD_ENGINE_H
 
-#include <util/cmdline.h>
-#include <util/message.h>
+#include "property_checker.h"
 
-#include "ebmc_properties.h"
-
-int bdd_engine(
+property_checker_resultt bdd_engine(
   const cmdlinet &,
   transition_systemt &,
   ebmc_propertiest &,

src/ebmc/k_induction.cpp

@@ -19,7 +19,6 @@ Author: Daniel Kroening, [email protected]
 #include "ebmc_error.h"
 #include "ebmc_solver_factory.h"
 #include "liveness_to_safety.h"
-#include "report_results.h"
 
 #include <fstream>
 
@@ -118,7 +117,7 @@ Function: k_induction
 
 \*******************************************************************/
 
-int k_induction(
+property_checker_resultt k_induction(
   const cmdlinet &cmdline,
   transition_systemt &transition_system,
   ebmc_propertiest &properties,
@@ -154,9 +153,7 @@ int k_induction(
   k_induction(
     k, transition_system, properties, solver_factory, message_handler);
 
-  const namespacet ns(transition_system.symbol_table);
-  report_results(cmdline, properties, ns, message_handler);
-  return properties.exit_code();
+  return property_checker_resultt::VERIFICATION_RESULT;
 }
 
 /*******************************************************************\

src/ebmc/k_induction.h

@@ -13,11 +13,12 @@ Author: Daniel Kroening, [email protected]
 #include <util/message.h>
 
 #include "ebmc_solver_factory.h"
+#include "property_checker.h"
 
 class transition_systemt;
 class ebmc_propertiest;
 
-int k_induction(
+property_checker_resultt k_induction(
   const cmdlinet &,
   transition_systemt &,
   ebmc_propertiest &,

src/ebmc/property_checker.cpp

@@ -27,7 +27,7 @@ Author: Daniel Kroening, [email protected]
 #include <chrono>
 #include <iostream>
 
-int word_level_bmc(
+property_checker_resultt word_level_bmc(
   const cmdlinet &cmdline,
   const transition_systemt &transition_system,
   ebmc_propertiest &properties,
@@ -38,8 +38,6 @@ int word_level_bmc(
   bool convert_only = cmdline.isset("smt2") || cmdline.isset("outfile") ||
                       cmdline.isset("show-formula");
 
-  int result = 0;
-
   try
   {
     if(cmdline.isset("max-bound"))
@@ -93,38 +91,34 @@ int word_level_bmc(
         solver_factory,
         message_handler);
 
-      if(!convert_only)
-      {
-        const namespacet ns(transition_system.symbol_table);
-        report_results(cmdline, properties, ns, message_handler);
-        result = properties.exit_code();
-      }
+      if(convert_only)
+        return property_checker_resultt::SUCCESS;
     }
   }
 
   catch(const char *e)
   {
     messaget message{message_handler};
     message.error() << e << messaget::eom;
-    return 10;
+    return property_checker_resultt::ERROR;
   }
 
   catch(const std::string &e)
   {
     messaget message{message_handler};
     message.error() << e << messaget::eom;
-    return 10;
+    return property_checker_resultt::ERROR;
   }
 
   catch(int)
   {
-    return 10;
+    return property_checker_resultt::ERROR;
   }
 
-  return result;
+  return property_checker_resultt::VERIFICATION_RESULT;
 }
 
-int finish_bit_level_bmc(
+property_checker_resultt finish_bit_level_bmc(
   std::size_t bound,
   const bmc_mapt &bmc_map,
   propt &solver,
@@ -179,12 +173,12 @@ int finish_bit_level_bmc(
 
     case propt::resultt::P_ERROR:
       message.error() << "Error from decision procedure" << messaget::eom;
-      return 2;
+      return property_checker_resultt::ERROR;
 
     default:
       message.error() << "Unexpected result from decision procedure"
                       << messaget::eom;
-      return 1;
+      return property_checker_resultt::ERROR;
     }
   }
 
@@ -195,10 +189,10 @@ int finish_bit_level_bmc(
     << std::chrono::duration<double>(sat_stop_time - sat_start_time).count()
     << messaget::eom;
 
-  return properties.exit_code();
+  return property_checker_resultt::VERIFICATION_RESULT;
 }
 
-int bit_level_bmc(
+property_checker_resultt bit_level_bmc(
   cnft &solver,
   bool convert_only,
   const cmdlinet &cmdline,
@@ -220,8 +214,6 @@ int bit_level_bmc(
     bound = 1;
   }
 
-  int result;
-
   try
   {
     bmc_mapt bmc_map;
@@ -288,38 +280,35 @@ int bit_level_bmc(
     }
 
     if(convert_only)
-      result = 0;
+      return property_checker_resultt::SUCCESS;
     else
     {
-      result = finish_bit_level_bmc(
+      return finish_bit_level_bmc(
         bound, bmc_map, solver, transition_system, properties, message_handler);
-      report_results(cmdline, properties, ns, message_handler);
     }
   }
 
   catch(const char *e)
   {
     messaget message{message_handler};
     message.error() << e << messaget::eom;
-    return 10;
+    return property_checker_resultt::ERROR;
   }
 
   catch(const std::string &e)
   {
     messaget message{message_handler};
     message.error() << e << messaget::eom;
-    return 10;
+    return property_checker_resultt::ERROR;
   }
 
   catch(int)
   {
-    return 10;
+    return property_checker_resultt::ERROR;
   }
-
-  return result;
 }
 
-int bit_level_bmc(
+property_checker_resultt bit_level_bmc(
   const cmdlinet &cmdline,
   transition_systemt &transition_system,
   ebmc_propertiest &properties,
@@ -380,23 +369,43 @@ int property_checker(
   ebmc_propertiest &properties,
   message_handlert &message_handler)
 {
+  property_checker_resultt result;
+
   if(cmdline.isset("bdd") || cmdline.isset("show-bdds"))
   {
-    return bdd_engine(cmdline, transition_system, properties, message_handler);
+    result =
+      bdd_engine(cmdline, transition_system, properties, message_handler);
   }
   else if(cmdline.isset("aig") || cmdline.isset("dimacs"))
   {
-    return bit_level_bmc(
-      cmdline, transition_system, properties, message_handler);
+    result =
+      bit_level_bmc(cmdline, transition_system, properties, message_handler);
   }
   else if(cmdline.isset("k-induction"))
   {
-    return k_induction(cmdline, transition_system, properties, message_handler);
+    result =
+      k_induction(cmdline, transition_system, properties, message_handler);
   }
   else
   {
     // default engine is word-level BMC
-    return word_level_bmc(
-      cmdline, transition_system, properties, message_handler);
+    result =
+      word_level_bmc(cmdline, transition_system, properties, message_handler);
+  }
+
+  switch(result)
+  {
+  case property_checker_resultt::ERROR:
+    return 10;
+
+  case property_checker_resultt::SUCCESS:
+    return 0;
+
+  case property_checker_resultt::VERIFICATION_RESULT:
+    const namespacet ns{transition_system.symbol_table};
+    report_results(cmdline, properties, ns, message_handler);
+    return properties.exit_code();
   }
+
+  UNREACHABLE;
 }

src/ebmc/property_checker.h

@@ -12,6 +12,13 @@ Author: Daniel Kroening, [email protected]
 #include "ebmc_properties.h"
 #include "transition_system.h"
 
+enum class property_checker_resultt
+{
+  VERIFICATION_RESULT,
+  SUCCESS,
+  ERROR
+};
+
 int property_checker(
   const cmdlinet &,
   transition_systemt &,