cprover
|
GOTO Programs. More...
#include "goto_check.h"
#include <algorithm>
#include <util/simplify_expr.h>
#include <util/array_name.h>
#include <util/ieee_float.h>
#include <util/arith_tools.h>
#include <util/expr_util.h>
#include <util/find_symbols.h>
#include <util/std_expr.h>
#include <util/std_types.h>
#include <util/guard.h>
#include <util/base_type.h>
#include <util/pointer_offset_size.h>
#include <util/pointer_predicates.h>
#include <util/cprover_prefix.h>
#include <util/options.h>
#include "local_bitvector_analysis.h"
Go to the source code of this file.
Classes | |
class | goto_checkt |
Functions | |
void | goto_check (const namespacet &ns, const optionst &options, goto_functionst::goto_functiont &goto_function) |
void | goto_check (const namespacet &ns, const optionst &options, goto_functionst &goto_functions) |
void | goto_check (const optionst &options, goto_modelt &goto_model) |
GOTO Programs.
Definition in file goto_check.cpp.
void goto_check | ( | const namespacet & | ns, |
const optionst & | options, | ||
goto_functionst::goto_functiont & | goto_function | ||
) |
Definition at line 1722 of file goto_check.cpp.
References goto_checkt::goto_check().
Referenced by goto_instrument_parse_optionst::instrument_goto_program(), clobber_parse_optionst::process_goto_program(), symex_parse_optionst::process_goto_program(), goto_analyzer_parse_optionst::process_goto_program(), and cbmc_parse_optionst::process_goto_program().
void goto_check | ( | const namespacet & | ns, |
const optionst & | options, | ||
goto_functionst & | goto_functions | ||
) |
Definition at line 1731 of file goto_check.cpp.
References goto_checkt::collect_allocations(), Forall_goto_functions, goto_checkt::goto_check(), and namespacet::lookup().
void goto_check | ( | const optionst & | options, |
goto_modelt & | goto_model | ||
) |
Definition at line 1747 of file goto_check.cpp.
References goto_checkt::goto_check(), goto_modelt::goto_functions, goto_checkt::ns, and goto_modelt::symbol_table.