From 53fc818ec887729f9adec050721f514e6e71b7af Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Sun, 30 Nov 2025 13:52:42 +0000
Subject: [PATCH] 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
---
 .../goto_instrument_parse_options.cpp         | 71 +++++++++++++++++++
 1 file changed, 71 insertions(+)

diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp
index 570554155b4..a20ff5cf9f5 100644
--- a/src/goto-instrument/goto_instrument_parse_options.cpp
+++ b/src/goto-instrument/goto_instrument_parse_options.cpp
@@ -124,6 +124,77 @@ 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)
+  {
+    const char *read_only_options[] = {
+      "call-graph",
+      "check-call-sequence",
+      "document-claims-html",
+      "document-claims-latex",
+      "document-properties-html",
+      "document-properties-latex",
+      "dot",
+      "dump-c",
+      "horn",
+      "interpreter",
+      "list-calls-args",
+      "list-goto-functions",
+      "list-symbols",
+      "list-undefined-functions",
+      "print-internal-representation",
+      "reachable-call-graph",
+      "show-call-sequences",
+      "show-claims",
+      "show-custom-bitvector-analysis",
+      "show-dependence-graph",
+      "show-escape-analysis",
+      "show-global-may-alias",
+      "show-goto-function-call-graph",
+      "show-goto-functions",
+      "show-intervals",
+      "show-lexical-loops",
+      "show-local-bitvector-analysis",
+      "show-local-safe-pointers",
+      "show-locations",
+      "show-loops",
+      "show-natural-loops",
+      "show-points-to",
+      "show-properties",
+      "show-reaching-definitions",
+      "show-rw-set",
+      "show-safe-dereferences",
+      "show-sese-regions",
+      "show-struct-alignment",
+      "show-symbol-table",
+      "show-threaded",
+      "show-uninitialized",
+      "show-value-sets",
+      "validate-goto-binary",
+      "validate-goto-model",
+      "xml",
+    };
+
+    bool is_read_only = false;
+    for(const char *opt : read_only_options)
+    {
+      if(cmdline.isset(opt))
+      {
+        is_read_only = true;
+        break;
+      }
+    }
+
+    if(!is_read_only)
+    {
+      log.error() << "output file name missing, run "
+                     "'goto-instrument input.gb output.gb [options]'"
+                  << messaget::eom;
+      return CPROVER_EXIT_USAGE_ERROR;
+    }
+  }
+
   messaget::eval_verbosity(
     cmdline.get_value("verbosity"), messaget::M_STATUS, ui_message_handler);