text: /*******************************************************************\
  
  Module: Command Line Parsing
  
  Author: Daniel Kroening, kroening@kroening.com
  
  \*******************************************************************/
  
  /// \file
  /// Command Line Parsing
  
  #ifndef CPROVER_GOTO_INSTRUMENT_GOTO_INSTRUMENT_PARSE_OPTIONS_H
  #define CPROVER_GOTO_INSTRUMENT_GOTO_INSTRUMENT_PARSE_OPTIONS_H
  
  #include <ansi-c/ansi_c_language.h>
  
  #include <util/parse_options.h>
  #include <util/timestamper.h>
  #include <util/ui_message.h>
  #include <util/validation_interface.h>
  
  #include <goto-programs/class_hierarchy.h>
  #include <goto-programs/goto_functions.h>
  #include <goto-programs/remove_calls_no_body.h>
  #include <goto-programs/remove_const_function_pointers.h>
  #include <goto-programs/restrict_function_pointers.h>
  #include <goto-programs/show_goto_functions.h>
  #include <goto-programs/show_properties.h>
  
  #include <analyses/goto_check.h>
  
  #include "aggressive_slicer.h"
  #include "code_contracts.h"
  #include "generate_function_bodies.h"
  #include "insert_final_assert_false.h"
  #include "nondet_volatile.h"
  #include "replace_calls.h"
  
  #include "count_eloc.h"
  
  // clang-format off
  #define GOTO_INSTRUMENT_OPTIONS \
    "(all)" \
    "(document-claims-latex)(document-claims-html)" \
    "(document-properties-latex)(document-properties-html)" \
    "(dump-c-type-header):" \
    "(dump-c)(dump-cpp)(no-system-headers)(use-all-headers)(dot)(xml)" \
    "(harness)" \
    OPT_GOTO_CHECK \
    /* no-X-check are deprecated and ignored */ \
    "(no-bounds-check)(no-pointer-check)(no-div-by-zero-check)" \
    "(no-nan-check)" \
    "(remove-pointers)" \
    "(no-simplify)" \
    "(assert-to-assume)" \
    "(no-assertions)(no-assumptions)(uninitialized-check)" \
    "(race-check)(scc)(one-event-per-cycle)" \
    "(minimum-interference)" \
    "(mm):(my-events)" \
    "(unwind):(unwindset):(unwindset-file):" \
    "(unwinding-assertions)(partial-loops)(continue-as-loops)" \
    "(log):" \
    "(max-var):(max-po-trans):(ignore-arrays)" \
    "(cfg-kill)(no-dependencies)(force-loop-duplication)" \
    "(call-graph)(reachable-call-graph)" \
    OPT_INSERT_FINAL_ASSERT_FALSE \
    OPT_SHOW_CLASS_HIERARCHY \
    "(no-po-rendering)(render-cluster-file)(render-cluster-function)" \
    "(isr):" \
    "(stack-depth):(nondet-static)" \
    "(nondet-static-exclude):" \
    "(function-enter):(function-exit):(branch):" \
    OPT_SHOW_GOTO_FUNCTIONS \
    OPT_SHOW_PROPERTIES \
    "(drop-unused-functions)" \
    "(show-value-sets)" \
    "(show-global-may-alias)" \
    "(show-local-bitvector-analysis)(show-custom-bitvector-analysis)" \
    "(show-escape-analysis)(escape-analysis)" \
    "(custom-bitvector-analysis)" \
    "(show-struct-alignment)(interval-analysis)(show-intervals)" \
    "(show-uninitialized)(show-locations)" \
    "(full-slice)(reachability-slice)(slice-global-inits)" \
    "(fp-reachability-slice):" \
    "(inline)(partial-inline)(function-inline):(log):(no-caching)" \
    "(value-set-fi-fp-removal)" \
    OPT_REMOVE_CONST_FUNCTION_POINTERS \
    "(print-internal-representation)" \
    "(remove-function-pointers)" \
    "(show-claims)(property):" \
    "(show-symbol-table)(show-points-to)(show-rw-set)" \
    "(cav11)" \
    OPT_TIMESTAMP \
    "(show-natural-loops)(show-lexical-loops)(accelerate)(havoc-loops)" \
    "(error-label):(string-abstraction)" \
    "(verbosity):(version)(xml-ui)(json-ui)(show-loops)" \
    "(accelerate)(constant-propagator)" \
    "(k-induction):(step-case)(base-case)" \
    "(show-call-sequences)(check-call-sequence)" \
    "(interpreter)(show-reaching-definitions)" \
    "(list-symbols)(list-undefined-functions)" \
    "(z3)(add-library)(show-dependence-graph)" \
    "(horn)(skip-loops):(model-argc-argv):" \
    "(" FLAG_REPLACE_CALL "):" \
    "(" FLAG_REPLACE_ALL_CALLS ")" \
    "(" FLAG_ENFORCE_CONTRACT "):" \
    "(" FLAG_ENFORCE_ALL_CONTRACTS ")" \
    "(show-threaded)(list-calls-args)" \
    "(undefined-function-is-assume-false)" \
    "(remove-function-body):"\
    OPT_AGGRESSIVE_SLICER \
    OPT_FLUSH \
    "(splice-call):" \
    OPT_REMOVE_CALLS_NO_BODY \
    OPT_REPLACE_FUNCTION_BODY \
    OPT_GOTO_PROGRAM_STATS \
    "(show-local-safe-pointers)(show-safe-dereferences)" \
    "(show-sese-regions)" \
    OPT_REPLACE_CALLS \
    "(validate-goto-binary)" \
    OPT_VALIDATE \
    OPT_ANSI_C_LANGUAGE \
    OPT_RESTRICT_FUNCTION_POINTER \
    OPT_NONDET_VOLATILE \
    "(ensure-one-backedge-per-target)" \
    // empty last line
  
  // clang-format on
  
  class goto_instrument_parse_optionst : public parse_options_baset
  {
  public:
    virtual int doit();
    virtual void help();
  
    goto_instrument_parse_optionst(int argc, const char **argv)
      : parse_options_baset(
          GOTO_INSTRUMENT_OPTIONS,
          argc,
          argv,
          "goto-instrument"),
        function_pointer_removal_done(false),
        partial_inlining_done(false),
        remove_returns_done(false)
    {
    }
  
  protected:
    void register_languages();
  
    void get_goto_program();
    void instrument_goto_program();
  
    void do_indirect_call_and_rtti_removal(bool force=false);
    void do_remove_const_function_pointers_only();
    void do_partial_inlining();
    void do_remove_returns();
  
    bool function_pointer_removal_done;
    bool partial_inlining_done;
    bool remove_returns_done;
  
    goto_modelt goto_model;
  };
  
  #endif // CPROVER_GOTO_INSTRUMENT_GOTO_INSTRUMENT_PARSE_OPTIONS_H
  