30 if(!ns.
lookup(gf_entry.first).is_macro && !gf_entry.second.body_available())
31 os << gf_entry.first <<
'\n';
39 for(
auto &ins : gf_entry.second.body.instructions)
41 if(!ins.is_function_call())
52 goto_functionst::function_mapt::const_iterator entry=
56 "called function must be in function_map");
58 if(entry->second.body_available())
62 ins.source_location.set_comment(
63 "'" +
id2string(
function) +
"' is undefined");
codet representation of a function call statement.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
const source_locationt & source_location() const
The Boolean constant false.
function_mapt function_map
symbol_tablet symbol_table
Symbol table.
goto_functionst goto_functions
GOTO functions.
static instructiont make_assumption(const exprt &g, const source_locationt &l=source_locationt::nil())
const irep_idt & id() const
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
const irep_idt & get_identifier() const
const std::string & id2string(const irep_idt &d)
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
const code_function_callt & to_code_function_call(const codet &code)
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
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.