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 
19 
21  const goto_functionst &goto_functions,
22  const namespacet &ns,
23  std::ostream &os)
24 {
25  forall_goto_functions(it, goto_functions)
26  if(!ns.lookup(it->first).is_macro &&
27  !it->second.body_available())
28  os << it->first << '\n';
29 }
30 
32 {
33  Forall_goto_functions(it, goto_functions)
34  Forall_goto_program_instructions(iit, it->second.body)
35  {
36  goto_programt::instructiont &ins=*iit;
37 
38  if(!ins.is_function_call())
39  continue;
40 
41  const code_function_callt &call=to_code_function_call(ins.code);
42 
43  if(call.function().id()!=ID_symbol)
44  continue;
45 
46  const irep_idt &function=
47  to_symbol_expr(call.function()).get_identifier();
48 
49  goto_functionst::function_mapt::const_iterator entry=
50  goto_functions.function_map.find(function);
51  assert(entry!=goto_functions.function_map.end());
52 
53  if(entry->second.body_available())
54  continue;
55 
56  ins.make_assumption(false_exprt());
57  ins.source_location.set_comment(
58  "`"+id2string(function)+"' is undefined");
59  }
60 }
virtual bool lookup(const irep_idt &name, const symbolt *&symbol) const
Definition: namespace.cpp:139
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
Goto Programs with Functions.
void undefined_function_abort_path(goto_functionst &goto_functions)
void list_undefined_functions(const goto_functionst &goto_functions, const namespacet &ns, std::ostream &os)
const irep_idt & id() const
Definition: irep.h:189
TO_BE_DOCUMENTED.
Definition: namespace.h:62
A function call.
Definition: std_code.h:657
The boolean constant false.
Definition: std_expr.h:3753
exprt & function()
Definition: std_code.h:677
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
Definition: std_expr.h:202
#define Forall_goto_functions(it, functions)
Handling of functions without body.
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:73
#define forall_goto_functions(it, functions)
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:700