From 6b6f6cb45a2603b617194b1a211ce76044cab25c Mon Sep 17 00:00:00 2001
From: Joel Allred <joel.allred@diffblue.com>
Date: Thu, 11 May 2017 11:53:45 +0100
Subject: [PATCH] Add message for unknown cbmc option

During command line parsing, if an unknown option is read, store it and
output an error message at parse_options_baset::main

Add regression tests to check the feature.
---
 regression/cbmc/bad_option/main.c             | 3 +++
 regression/cbmc/bad_option/test.desc          | 7 +++++++
 regression/cbmc/bad_option/test_multiple.desc | 7 +++++++
 src/util/cmdline.cpp                          | 3 +++
 src/util/cmdline.h                            | 1 +
 src/util/parse_options.cpp                    | 9 +++++++++
 src/util/parse_options.h                      | 1 +
 7 files changed, 31 insertions(+)
 create mode 100644 regression/cbmc/bad_option/main.c
 create mode 100644 regression/cbmc/bad_option/test.desc
 create mode 100644 regression/cbmc/bad_option/test_multiple.desc

diff --git a/regression/cbmc/bad_option/main.c b/regression/cbmc/bad_option/main.c
new file mode 100644
index 00000000000..4cce7f667ff
--- /dev/null
+++ b/regression/cbmc/bad_option/main.c
@@ -0,0 +1,3 @@
+int main() {
+  return 0;
+}
diff --git a/regression/cbmc/bad_option/test.desc b/regression/cbmc/bad_option/test.desc
new file mode 100644
index 00000000000..c7f22f5b873
--- /dev/null
+++ b/regression/cbmc/bad_option/test.desc
@@ -0,0 +1,7 @@
+CORE
+main.c
+-foo
+^EXIT=(64|1)$
+^SIGNAL=0$
+Unknown option: -foo
+--
diff --git a/regression/cbmc/bad_option/test_multiple.desc b/regression/cbmc/bad_option/test_multiple.desc
new file mode 100644
index 00000000000..30697b2267d
--- /dev/null
+++ b/regression/cbmc/bad_option/test_multiple.desc
@@ -0,0 +1,7 @@
+CORE
+main.c
+--trace --foo --refine-strings
+^EXIT=(64|1)$
+^SIGNAL=0$
+Unknown option: --foo
+--
diff --git a/src/util/cmdline.cpp b/src/util/cmdline.cpp
index 10ca6ac97c8..ab62a9b63a5 100644
--- a/src/util/cmdline.cpp
+++ b/src/util/cmdline.cpp
@@ -185,7 +185,10 @@ bool cmdlinet::parse(int argc, const char **argv, const char *optstring)
       }
 
       if(optnr<0)
+      {
+        unknown_arg=argv[i];
         return true;
+      }
       options[optnr].isset=true;
       if(options[optnr].hasval)
       {
diff --git a/src/util/cmdline.h b/src/util/cmdline.h
index 94ac1db5c6f..2d58daa8d44 100644
--- a/src/util/cmdline.h
+++ b/src/util/cmdline.h
@@ -33,6 +33,7 @@ class cmdlinet
 
   typedef std::vector<std::string> argst;
   argst args;
+  std::string unknown_arg;
 
   cmdlinet();
   virtual ~cmdlinet();
diff --git a/src/util/parse_options.cpp b/src/util/parse_options.cpp
index 2e4d91e75e9..75235cc9cf5 100644
--- a/src/util/parse_options.cpp
+++ b/src/util/parse_options.cpp
@@ -37,11 +37,20 @@ void parse_options_baset::usage_error()
   help();
 }
 
+/// Print an error message mentioning the option that was not recognized when
+/// parsing the command line.
+void parse_options_baset::unknown_option_msg()
+{
+  if(!cmdline.unknown_arg.empty())
+    std::cerr << "Unknown option: " << cmdline.unknown_arg << "\n";
+}
+
 int parse_options_baset::main()
 {
   if(parse_result)
   {
     usage_error();
+    unknown_option_msg();
     return EX_USAGE;
   }
 
diff --git a/src/util/parse_options.h b/src/util/parse_options.h
index 73f436cf331..b2e64722e85 100644
--- a/src/util/parse_options.h
+++ b/src/util/parse_options.h
@@ -31,6 +31,7 @@ class parse_options_baset
   virtual ~parse_options_baset() { }
 
 private:
+  void unknown_option_msg();
   bool parse_result;
 };