Implementation of a erroneous user input exception class.

Author: NlightNFotis

src/cbmc/cbmc_main.cpp

@@ -43,7 +43,7 @@ int main(int argc, const char **argv)
 #endif
   cbmc_parse_optionst parse_options(argc, argv);
 
-  int res=parse_options.main();
+  int res = parse_options.main();
 
   #ifdef IREP_HASH_STATS
   std::cout << "IREP_HASH_CNT=" << irep_hash_cnt << '\n';

src/cbmc/cbmc_parse_options.h

@@ -76,10 +76,9 @@ class optionst;
   "(claim):(show-claims)(floatbv)(all-claims)(all-properties)" // legacy, and will eventually disappear // NOLINT(whitespace/line_length)
 // clang-format on
 
-class cbmc_parse_optionst:
-  public parse_options_baset,
-  public xml_interfacet,
-  public messaget
+class cbmc_parse_optionst : public parse_options_baset,
+                            public xml_interfacet,
+                            public messaget
 {
 public:
   virtual int doit() override;

src/util/Makefile

@@ -13,6 +13,7 @@ SRC = arith_tools.cpp \
       expr.cpp \
       expr_initializer.cpp \
       expr_util.cpp \
+      exception_utils.cpp \
       file_util.cpp \
       find_macros.cpp \
       find_symbols.cpp \

src/util/exception_utils.cpp

@@ -0,0 +1,20 @@
+/*******************************************************************\
+
+Module: Exception helper utilities
+
+Author: Fotis Koutoulakis, [email protected]
+
+\*******************************************************************/
+
+#include "exception_utils.h"
+
+std::string invalid_user_input_exceptiont::what() const noexcept
+{
+  std::string res;
+  res += "\nInvalid User Input\n";
+  res += "Option: " + option + "\n";
+  res += "Reason: " + reason;
+  // Print an optional correct usage message assuming correct input parameters have been passed
+  res += correct_input.empty() ? "\n" : " Try: " + correct_input + "\n";
+  return res;
+}

src/util/exception_utils.h

@@ -0,0 +1,32 @@
+/*******************************************************************\
+
+Module: Exception helper utilities
+
+Author: Fotis Koutoulakis, [email protected]
+
+\*******************************************************************/
+
+#ifndef CPROVER_UTIL_EXCEPTION_UTILS_H
+#define CPROVER_UTIL_EXCEPTION_UTILS_H
+
+#include <string>
+
+class invalid_user_input_exceptiont
+{
+  std::string reason;
+  std::string option;
+  std::string correct_input;
+
+public:
+  invalid_user_input_exceptiont(
+    std::string reason,
+    std::string option,
+    std::string correct_input = "")
+    : reason(reason), option(option), correct_input(correct_input)
+  {
+  }
+
+  std::string what() const noexcept;
+};
+
+#endif // CPROVER_UTIL_EXCEPTION_UTILS_H

src/util/parse_options.cpp

@@ -18,6 +18,8 @@ Author: Daniel Kroening, [email protected]
 #endif
 
 #include "cmdline.h"
+#include "exception_utils.h"
+#include "exit_codes.h"
 #include "signal_catcher.h"
 
 parse_options_baset::parse_options_baset(
@@ -47,23 +49,34 @@ void parse_options_baset::unknown_option_msg()
 
 int parse_options_baset::main()
 {
-  if(parse_result)
+  // catch all exceptions here so that this code is not duplicated
+  // for each tool
+  try
   {
-    usage_error();
-    unknown_option_msg();
-    return EX_USAGE;
+    if(parse_result)
+    {
+      usage_error();
+      unknown_option_msg();
+      return EX_USAGE;
+    }
+
+    if(cmdline.isset('?') || cmdline.isset('h') || cmdline.isset("help"))
+    {
+      help();
+      return EX_OK;
+    }
+
+    // install signal catcher
+    install_signal_catcher();
+
+    return doit();
   }
-
-  if(cmdline.isset('?') || cmdline.isset('h') || cmdline.isset("help"))
+  catch(invalid_user_input_exceptiont &e)
   {
-    help();
-    return EX_OK;
+    std::cerr << e.what() << "\n";
+    return CPROVER_EXIT_USAGE_ERROR;
   }
-
-  // install signal catcher
-  install_signal_catcher();
-
-  return doit();
+  return CPROVER_EXIT_SUCCESS;
 }
 
 std::string