cprover
goto_functions.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Goto Programs with Functions
4 
5 Author: Daniel Kroening
6 
7 Date: June 2003
8 
9 \*******************************************************************/
10 
13 
14 #include "goto_functions.h"
15 
17  const namespacet &ns,
18  std::ostream &out) const
19 {
20  for(const auto &fun : function_map)
21  {
22  if(fun.second.body_available())
23  {
24  out << "^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\n\n";
25 
26  const symbolt &symbol=ns.lookup(fun.first);
27  out << symbol.display_name() << " /* " << symbol.name << " */\n";
28  fun.second.body.output(ns, symbol.name, out);
29 
30  out << std::flush;
31  }
32  }
33 }
34 
36 {
38  for(auto &func : function_map)
39  {
40  // Side-effect: bumps unused_location_number.
41  func.second.body.compute_location_numbers(unused_location_number);
42  }
43 }
44 
46  goto_programt &program)
47 {
48  // Renumber just this single function. Use fresh numbers in case it has
49  // grown since it was last numbered.
51 }
52 
54 {
55  for(auto &func : function_map)
56  {
57  func.second.body.compute_incoming_edges();
58  }
59 }
60 
62 {
63  for(auto &func : function_map)
64  {
65  func.second.body.compute_target_numbers();
66  }
67 }
68 
70 {
71  for(auto &func : function_map)
72  {
73  func.second.body.compute_loop_numbers();
74  }
75 }
irep_idt name
The unique identifier.
Definition: symbol.h:43
void compute_location_numbers(unsigned &nr)
Compute location numbers.
Definition: goto_program.h:542
void compute_loop_numbers()
void compute_target_numbers()
Goto Programs with Functions.
unsigned unused_location_number
A location number such that numbers in the interval [unused_location_number, MAX_UINT] are all unused...
function_mapt function_map
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:30
void compute_location_numbers()
void output(const namespacet &ns, std::ostream &out) const
TO_BE_DOCUMENTED.
Definition: namespace.h:74
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:70
const irep_idt & display_name() const
Definition: symbol.h:57
void compute_incoming_edges()
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See namespace_baset::lookup().
Definition: namespace.cpp:130