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,12 @@ 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 a file argument has been given.
+  if(cmdline.args.size() != 1)
   {
     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 +62,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 - it's also possible to fall through this case if no optional
+  // inspection flag is present in the argument vector. This will ensure that the
+  // return value in that case is semantically meaningful, and provide a return
+  // value that also satisfies the compiler's requirements based on the signature
+  // of `doit()`.
   return CPROVER_EXIT_INCORRECT_TASK;
 }