29 if(!ns.
lookup(it->first).is_macro &&
30 !it->second.body_available())
31 os << it->first <<
'\n';
52 goto_functionst::function_mapt::const_iterator entry=
56 "called function must be in function_map");
58 if(entry->second.body_available())
63 "`"+
id2string(
function)+
"' is undefined");
void undefined_function_abort_path(goto_modelt &goto_model)
const std::string & id2string(const irep_idt &d)
void make_assumption(const exprt &g)
void list_undefined_functions(const goto_modelt &goto_model, std::ostream &os)
bool is_function_call() const
void set_comment(const irep_idt &comment)
function_mapt function_map
symbol_tablet symbol_table
Symbol table.
This class represents an instruction in the GOTO intermediate representation.
const irep_idt & id() const
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
The boolean constant false.
source_locationt source_location
The location of the instruction in the source file.
#define Forall_goto_functions(it, functions)
Handling of functions without body.
#define Forall_goto_program_instructions(it, program)
#define DATA_INVARIANT(CONDITION, REASON)
#define forall_goto_functions(it, functions)
goto_functionst goto_functions
GOTO functions.
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See namespace_baset::lookup().
const code_function_callt & to_code_function_call(const codet &code)