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,13 @@ 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 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;
 }