goto-instrument: add early output file validation

Validate output file presence before expensive analysis operations to
prevent wasted computation when command is malformed.

Fixes: #2593

Author: tautschnig

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -124,6 +124,69 @@ int goto_instrument_parse_optionst::doit()
     return CPROVER_EXIT_USAGE_ERROR;
   }
 
+  // Check if an output file is required before expensive operations
+  // Most operations that modify the model require an output file
+  if(cmdline.args.size() < 2)
+  {
+    // Check if this is a read-only operation that doesn't require output
+    // clang-format off
+    bool is_read_only_operation =
+      cmdline.isset("call-graph") ||
+      cmdline.isset("check-call-sequence") ||
+      cmdline.isset("document-claims-html") ||
+      cmdline.isset("document-claims-latex") ||
+      cmdline.isset("document-properties-html") ||
+      cmdline.isset("document-properties-latex") ||
+      cmdline.isset("dot") ||
+      cmdline.isset("dump-c") ||
+      cmdline.isset("horn") ||
+      cmdline.isset("interpreter") ||
+      cmdline.isset("list-calls-args") ||
+      cmdline.isset("list-goto-functions") ||
+      cmdline.isset("list-symbols") ||
+      cmdline.isset("list-undefined-functions") ||
+      cmdline.isset("print-internal-representation") ||
+      cmdline.isset("reachable-call-graph") ||
+      cmdline.isset("show-call-sequences") ||
+      cmdline.isset("show-claims") ||
+      cmdline.isset("show-custom-bitvector-analysis") ||
+      cmdline.isset("show-dependence-graph") ||
+      cmdline.isset("show-escape-analysis") ||
+      cmdline.isset("show-global-may-alias") ||
+      cmdline.isset("show-goto-function-call-graph") ||
+      cmdline.isset("show-goto-functions") ||
+      cmdline.isset("show-intervals") ||
+      cmdline.isset("show-lexical-loops") ||
+      cmdline.isset("show-local-bitvector-analysis") ||
+      cmdline.isset("show-local-safe-pointers") ||
+      cmdline.isset("show-locations") ||
+      cmdline.isset("show-loops") ||
+      cmdline.isset("show-natural-loops") ||
+      cmdline.isset("show-points-to") ||
+      cmdline.isset("show-properties") ||
+      cmdline.isset("show-reaching-definitions") ||
+      cmdline.isset("show-rw-set") ||
+      cmdline.isset("show-safe-dereferences") ||
+      cmdline.isset("show-sese-regions") ||
+      cmdline.isset("show-struct-alignment") ||
+      cmdline.isset("show-symbol-table") ||
+      cmdline.isset("show-threaded") ||
+      cmdline.isset("show-uninitialized") ||
+      cmdline.isset("show-value-sets") ||
+      cmdline.isset("validate-goto-binary") ||
+      cmdline.isset("validate-goto-model") ||
+      cmdline.isset("xml");
+    // clang-format on
+
+    if(!is_read_only_operation)
+    {
+      log.error() << "Error: Output file name required. "
+                  << "Run 'goto-instrument --help' for usage information."
+                  << messaget::eom;
+      return CPROVER_EXIT_USAGE_ERROR;
+    }
+  }
+
   messaget::eval_verbosity(
     cmdline.get_value("verbosity"), messaget::M_STATUS, ui_message_handler);