goto_analyzer_parse_options.h

Go to the documentation of this file.

/*******************************************************************\
 
Module: Goto-Analyser Command Line Option Processing
 
Author: Daniel Kroening, kroening@kroening.com
 
\*******************************************************************/
 
 
#ifndef CPROVER_GOTO_ANALYZER_GOTO_ANALYZER_PARSE_OPTIONS_H
#define CPROVER_GOTO_ANALYZER_GOTO_ANALYZER_PARSE_OPTIONS_H
 
#include <util/config.h>
#include <util/parse_options.h>
#include <util/timestamper.h>
#include <util/ui_message.h>
#include <util/validation_interface.h>
 
#include <goto-programs/goto_model.h>
#include <goto-programs/show_goto_functions.h>
#include <goto-programs/show_properties.h>
 
#include <analyses/variable-sensitivity/variable_sensitivity_domain.h>
#include <ansi-c/goto-conversion/goto_check_c.h>
#include <langapi/language.h>
 
class optionst;
 
// clang-format off
#define GOTO_ANALYSER_OPTIONS_TASKS \
  "(show)(verify)(simplify):" \
  "(show-on-source)" \
  "(unreachable-instructions)(unreachable-functions)" \
  "(reachable-functions)"           \
  "(no-standard-checks)"
#define GOTO_ANALYSER_OPTIONS_TASKS \ …
 
#define GOTO_ANALYSER_OPTIONS_AI \
  "(recursive-interprocedural)" \
  "(three-way-merge)" \
  "(legacy-ait)" \
  "(legacy-concurrent)"
#define GOTO_ANALYSER_OPTIONS_AI \ …
 
#define GOTO_ANALYSER_OPTIONS_HISTORY \
  "(ahistorical)" \
  "(call-stack):" \
  "(loop-unwind):" \
  "(branching):" \
  "(loop-unwind-and-branching):"
#define GOTO_ANALYSER_OPTIONS_HISTORY \ …
 
#define GOTO_ANALYSER_OPTIONS_DOMAIN \
  "(intervals)" \
  "(non-null)" \
  "(constants)" \
  "(dependence-graph)" \
  "(vsd)(variable-sensitivity)" \
  "(dependence-graph-vs)" \
 
#define GOTO_ANALYSER_OPTIONS_DOMAIN \ …
#define GOTO_ANALYSER_OPTIONS_STORAGE \
  "(one-domain-per-history)" \
  "(one-domain-per-location)"
#define GOTO_ANALYSER_OPTIONS_STORAGE \ …
 
#define GOTO_ANALYSER_OPTIONS_OUTPUT \
  "(json):(xml):" \
  "(text):(dot):"
#define GOTO_ANALYSER_OPTIONS_OUTPUT \ …
 
#define GOTO_ANALYSER_OPTIONS_SPECIFIC_ANALYSES \
  "(taint):(show-taint)" \
  "(show-local-may-alias)" \
  "(show-local-bitvector)"
#define GOTO_ANALYSER_OPTIONS_SPECIFIC_ANALYSES \ …
 
#define GOTO_ANALYSER_OPTIONS \
  OPT_FUNCTIONS \
  OPT_CONFIG_C_CPP \
  OPT_CONFIG_PLATFORM \
  OPT_SHOW_GOTO_FUNCTIONS \
  OPT_SHOW_PROPERTIES \
  OPT_GOTO_CHECK \
  OPT_CONFIG_LIBRARY \
  "(show-symbol-table)(show-parse-tree)" \
  "(property):" \
  "(verbosity):(version)" \
  OPT_FLUSH \
  OPT_TIMESTAMP \
  OPT_VALIDATE \
  GOTO_ANALYSER_OPTIONS_TASKS \
  "(no-simplify-slicing)" \
  "(show-intervals)(show-non-null)" \
  GOTO_ANALYSER_OPTIONS_AI \
  "(location-sensitive)(concurrent)" \
  GOTO_ANALYSER_OPTIONS_HISTORY \
  GOTO_ANALYSER_OPTIONS_DOMAIN \
  OPT_VSD \
  GOTO_ANALYSER_OPTIONS_STORAGE  \
  GOTO_ANALYSER_OPTIONS_OUTPUT \
  GOTO_ANALYSER_OPTIONS_SPECIFIC_ANALYSES \
// clang-format on
 
class goto_analyzer_parse_optionst: public parse_options_baset
{
public:
  virtual int doit() override;
  virtual void help() override;
 
  goto_analyzer_parse_optionst(int argc, const char **argv);
 
protected:
  goto_modelt goto_model;
 
  void register_languages() override;
 
  virtual void get_command_line_options(optionst &options);
 
  virtual bool process_goto_program(const optionst &options);
 
  virtual int perform_analysis(const optionst &options);
 
  // TODO: Add documentation
  static void set_default_analysis_flags(optionst &options, const bool enabled);
};
class goto_analyzer_parse_optionst: public parse_options_baset {…};
 
#endif // CPROVER_GOTO_ANALYZER_GOTO_ANALYZER_PARSE_OPTIONS_H