diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index 570554155b4..791c43586f5 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/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);