cprover
|
Program Transformation. More...
Go to the source code of this file.
Macros | |
#define | OPT_GOTO_CHECK |
#define | HELP_GOTO_CHECK |
#define | PARSE_OPTIONS_GOTO_CHECK(cmdline, options) |
Functions | |
void | goto_check (const namespacet &ns, const optionst &options, goto_functionst &goto_functions) |
void | goto_check (const namespacet &ns, const optionst &options, const irep_idt &mode, goto_functionst::goto_functiont &goto_function) |
void | goto_check (const optionst &options, goto_modelt &goto_model) |
Program Transformation.
Definition in file goto_check.h.
#define HELP_GOTO_CHECK |
Definition at line 42 of file goto_check.h.
Referenced by jdiff_parse_optionst::help(), clobber_parse_optionst::help(), goto_diff_parse_optionst::help(), cbmc_parse_optionst::help(), jbmc_parse_optionst::help(), goto_instrument_parse_optionst::help(), janalyzer_parse_optionst::help(), and goto_analyzer_parse_optionst::help().
#define OPT_GOTO_CHECK |
Definition at line 36 of file goto_check.h.
#define PARSE_OPTIONS_GOTO_CHECK | ( | cmdline, | |
options | |||
) |
Definition at line 56 of file goto_check.h.
Referenced by clobber_parse_optionst::get_command_line_options(), jdiff_parse_optionst::get_command_line_options(), goto_diff_parse_optionst::get_command_line_options(), cbmc_parse_optionst::get_command_line_options(), jbmc_parse_optionst::get_command_line_options(), and goto_instrument_parse_optionst::instrument_goto_program().
void goto_check | ( | const namespacet & | ns, |
const optionst & | options, | ||
goto_functionst & | goto_functions | ||
) |
Definition at line 1773 of file goto_check.cpp.
References Forall_goto_functions, goto_check(), and namespacet::lookup().
void goto_check | ( | const namespacet & | ns, |
const optionst & | options, | ||
const irep_idt & | mode, | ||
goto_functionst::goto_functiont & | goto_function | ||
) |
Definition at line 1763 of file goto_check.cpp.
References goto_check().
Referenced by goto_check(), goto_instrument_parse_optionst::instrument_goto_program(), jbmc_parse_optionst::process_goto_function(), clobber_parse_optionst::process_goto_program(), jdiff_parse_optionst::process_goto_program(), goto_diff_parse_optionst::process_goto_program(), cbmc_parse_optionst::process_goto_program(), janalyzer_parse_optionst::process_goto_program(), and goto_analyzer_parse_optionst::process_goto_program().
void goto_check | ( | const optionst & | options, |
goto_modelt & | goto_model | ||
) |
Definition at line 1789 of file goto_check.cpp.
References goto_check(), goto_modelt::goto_functions, and goto_modelt::symbol_table.