cprover
undefined_functions.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Handling of functions without body
4 
5 Author: Michael Tautschnig
6 
7 Date: 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 
29  if(!ns.lookup(it->first).is_macro &&
30  !it->second.body_available())
31  os << it->first << '\n';
32 }
33 
35 {
37  Forall_goto_program_instructions(iit, it->second.body)
38  {
40 
41  if(!ins.is_function_call())
42  continue;
43 
45 
46  if(call.function().id()!=ID_symbol)
47  continue;
48 
49  const irep_idt &function=
51 
52  goto_functionst::function_mapt::const_iterator entry=
53  goto_model.goto_functions.function_map.find(function);
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 
63  "'" + id2string(function) + "' is undefined");
64  }
65 }
Forall_goto_program_instructions
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:1201
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
goto_programt::instructiont::source_location
source_locationt source_location
The location of the instruction in the source file.
Definition: goto_program.h:269
source_locationt::set_comment
void set_comment(const irep_idt &comment)
Definition: source_location.h:141
invariant.h
goto_model.h
Symbol Table + CFG.
goto_modelt
Definition: goto_model.h:26
goto_functionst::function_map
function_mapt function_map
Definition: goto_functions.h:27
list_undefined_functions
void list_undefined_functions(const goto_modelt &goto_model, std::ostream &os)
Definition: undefined_functions.cpp:22
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
namespacet::lookup
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:140
code_function_callt
codet representation of a function call statement.
Definition: std_code.h:1183
DATA_INVARIANT
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:511
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
goto_programt::instructiont::code
codet code
Do not read or modify directly – use get_X() instead.
Definition: goto_program.h:182
undefined_function_abort_path
void undefined_function_abort_path(goto_modelt &goto_model)
Definition: undefined_functions.cpp:34
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:111
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:177
irept::id
const irep_idt & id() const
Definition: irep.h:418
to_code_function_call
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:1294
false_exprt
The Boolean constant false.
Definition: std_expr.h:3964
Forall_goto_functions
#define Forall_goto_functions(it, functions)
Definition: goto_functions.h:117
undefined_functions.h
Handling of functions without body.
goto_modelt::goto_functions
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:33
forall_goto_functions
#define forall_goto_functions(it, functions)
Definition: goto_functions.h:122
goto_programt::make_assumption
static instructiont make_assumption(const exprt &g, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:905
goto_programt::instructiont::is_function_call
bool is_function_call() const
Definition: goto_program.h:461
goto_programt::instructiont
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:179
goto_modelt::symbol_table
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:30
code_function_callt::function
exprt & function()
Definition: std_code.h:1218