CBMC
Loading...
Searching...
No Matches
undefined_functions.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Handling of functions without body
4
5Author: Michael Tautschnig
6
7Date: July 2016
8
9\*******************************************************************/
10
13
14#include "undefined_functions.h"
15
16#include <ostream>
17
18#include <util/invariant.h>
19
21
23 const goto_modelt &goto_model,
24 std::ostream &os)
25{
26 const namespacet ns(goto_model.symbol_table);
27
28 for(const auto &gf_entry : goto_model.goto_functions.function_map)
29 {
30 if(!ns.lookup(gf_entry.first).is_macro && !gf_entry.second.body_available())
31 os << gf_entry.first << '\n';
32 }
33}
34
36{
37 for(auto &gf_entry : goto_model.goto_functions.function_map)
38 {
39 for(auto &ins : gf_entry.second.body.instructions)
40 {
41 if(!ins.is_function_call())
42 continue;
43
44 const auto &function = ins.call_function();
45
46 if(function.id() != ID_symbol)
47 continue;
48
49 const irep_idt &function_identifier =
50 to_symbol_expr(function).get_identifier();
51
52 goto_functionst::function_mapt::const_iterator entry =
53 goto_model.goto_functions.function_map.find(function_identifier);
55 entry!=goto_model.goto_functions.function_map.end(),
56 "called function must be in function_map");
57
58 if(entry->second.body_available())
59 continue;
60
61 source_locationt annotated_location = ins.source_location();
62 annotated_location.set_comment(
63 "'" + id2string(function_identifier) + "' is undefined");
65 }
66 }
67}
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
The Boolean constant false.
Definition std_expr.h:3199
function_mapt function_map
symbol_tablet symbol_table
Symbol table.
Definition goto_model.h:31
goto_functionst goto_functions
GOTO functions.
Definition goto_model.h:34
static instructiont make_assumption(const exprt &g, const source_locationt &l=source_locationt::nil())
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Symbol Table + CFG.
const std::string & id2string(const irep_idt &d)
Definition irep.h:44
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition invariant.h:534
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:272
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.