cprover
|
Handling of functions without body. More...
#include "undefined_functions.h"
#include <ostream>
#include <util/invariant.h>
#include <goto-programs/goto_model.h>
Go to the source code of this file.
Functions | |
void | list_undefined_functions (const goto_modelt &goto_model, std::ostream &os) |
void | undefined_function_abort_path (goto_modelt &goto_model) |
Handling of functions without body.
Definition in file undefined_functions.cpp.
void list_undefined_functions | ( | const goto_modelt & | goto_model, |
std::ostream & | os | ||
) |
Definition at line 22 of file undefined_functions.cpp.
References forall_goto_functions, goto_modelt::goto_functions, namespacet::lookup(), and goto_modelt::symbol_table.
Referenced by goto_instrument_parse_optionst::doit().
void undefined_function_abort_path | ( | goto_modelt & | goto_model | ) |
Definition at line 34 of file undefined_functions.cpp.
References goto_programt::instructiont::code, DATA_INVARIANT, Forall_goto_functions, Forall_goto_program_instructions, code_function_callt::function(), goto_functionst::function_map, goto_modelt::goto_functions, irept::id(), id2string(), goto_programt::instructiont::is_function_call(), goto_programt::instructiont::make_assumption(), source_locationt::set_comment(), goto_programt::instructiont::source_location, to_code_function_call(), and to_symbol_expr().
Referenced by goto_instrument_parse_optionst::doit().