janalyzer_parse_options.h

Go to the documentation of this file.

/*******************************************************************\
 
Module: JANALYZER Command Line Option Processing
 
Author: Daniel Kroening, kroening@kroening.com
 
\*******************************************************************/

 
#ifndef CPROVER_JANALYZER_JANALYZER_PARSE_OPTIONS_H
#define CPROVER_JANALYZER_JANALYZER_PARSE_OPTIONS_H
 
#include <util/parse_options.h>
#include <util/timestamper.h>
 
#include <langapi/language.h>
 
#include <goto-programs/show_goto_functions.h>
#include <goto-programs/show_properties.h>
 
#include <java_bytecode/java_bytecode_language.h>
 
class abstract_goto_modelt;
class ai_baset;
class goto_functiont;
class goto_model_functiont;
class optionst;
 
// clang-format off
#define JANALYZER_OPTIONS \
  OPT_FUNCTIONS \
  "(classpath):(cp):" \
  OPT_JAVA_JAR \
  "(main-class):" \
  OPT_JAVA_GOTO_BINARY \
  "(16)(32)(64)(LP64)(ILP64)(LLP64)(ILP32)(LP32)" \
  "(little-endian)(big-endian)" \
  OPT_SHOW_GOTO_FUNCTIONS \
  OPT_SHOW_PROPERTIES \
  "(no-assertions)(no-assumptions)" \
  "(show-symbol-table)(show-parse-tree)" \
  "(property):" \
  "(verbosity):(version)" \
  "(arch):" \
  "(taint):(show-taint)" \
  "(show-local-may-alias)" \
  "(json):(xml):" \
  "(text):(dot):" \
  OPT_TIMESTAMP \
  "(unreachable-instructions)(unreachable-functions)" \
  "(reachable-functions)" \
  "(intervals)(show-intervals)" \
  "(non-null)(show-non-null)" \
  "(constants)" \
  "(dependence-graph)" \
  "(show)(verify)(simplify):" \
  "(location-sensitive)(concurrent)" \
  "(no-simplify-slicing)" \
  JAVA_BYTECODE_LANGUAGE_OPTIONS
// clang-format on
 
class janalyzer_parse_optionst : public parse_options_baset
{
public:
  int doit() override;
  void help() override;
 
  janalyzer_parse_optionst(int argc, const char **argv);
 
  bool process_goto_functions(goto_modelt &goto_model, const optionst &options);
 
  void process_goto_function(
    goto_model_functiont &function,
    const abstract_goto_modelt &model,
    const optionst &options);
 
  bool can_generate_function_body(const irep_idt &name);
 
  bool generate_function_body(
    const irep_idt &function_name,
    symbol_table_baset &symbol_table,
    goto_functiont &function,
    bool body_available);
 
protected:
  std::unique_ptr<class_hierarchyt> class_hierarchy;
 
  void register_languages() override;
 
  void get_command_line_options(optionst &options);
 
  virtual int
  perform_analysis(goto_modelt &goto_model, const optionst &options);
 
  ai_baset *build_analyzer(
    goto_modelt &goto_model,
    const optionst &,
    const namespacet &ns);
};
 
#endif // CPROVER_JANALYZER_JANALYZER_PARSE_OPTIONS_H