Add explanation for return value and tighten error checking for number of args passed

Author: NlightNFotis

doc/man/goto-inspect.1

@@ -30,4 +30,4 @@ If you encounter a problem please create an issue at
 .BR goto-cc (1)
 .BR goto-instrument (1)
 .SH COPYRIGHT
-2023, Fotis Koutoulakis
+2023, Diffblue Ltd.

src/goto-inspect/goto_inspect_parse_options.cpp

@@ -21,13 +21,13 @@ int goto_inspect_parse_optionst::doit()
     return CPROVER_EXIT_SUCCESS;
   }
 
-  // Before we do anything else, positional arguments needs to be > 1.
-  // (i.e. a filename has been given).
-  if(cmdline.args.size() < 1)
+  // Before we do anything else, ensure that positional + optional arguments > 2.
+  // (i.e. a filename and an inspection option has been given).
+  if(cmdline.args.size() < 2)
   {
     help();
     throw invalid_command_line_argument_exceptiont{
-      "failed to supply a goto-binary name",
+      "failed to supply a goto-binary name or an option for inspection",
       "<input goto-binary> <inspection-option>"};
   }
 
@@ -63,7 +63,14 @@ int goto_inspect_parse_optionst::doit()
     return CPROVER_EXIT_SUCCESS;
   }
 
-  // No options was passed in - erroneously?
+  // If an option + binary was provided, the program will have exited gracefully
+  // through different a different branch. If we hit the code below, it means
+  // that something has gone wrong - normally both the happy and the error paths
+  // should be handled through the dispatching if blocks above, but we need a
+  // return statement to satisfy the compiler and the signature of `doit()`,
+  // hence why we have this here as a dummy return value that attempts to be
+  // somewhat semantically relevant and consistent to the behaviour of other
+  // tools.
   return CPROVER_EXIT_INCORRECT_TASK;
 }