cprover
link_to_library.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Library Linking
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "link_to_library.h"
13 
15 #include "goto_convert_functions.h"
16 
25  goto_modelt &goto_model,
26  message_handlert &message_handler,
27  const std::function<
28  void(const std::set<irep_idt> &, symbol_tablet &, message_handlert &)>
29  &library)
30 {
32  goto_model.symbol_table,
33  goto_model.goto_functions,
34  message_handler,
35  library);
36 }
37 
48  symbol_tablet &symbol_table,
49  goto_functionst &goto_functions,
50  message_handlert &message_handler,
51  const std::function<
52  void(const std::set<irep_idt> &, symbol_tablet &, message_handlert &)>
53  &library)
54 {
55  // this needs a fixedpoint, as library functions
56  // may depend on other library functions
57 
58  std::set<irep_idt> added_functions;
59 
60  while(true)
61  {
62  std::unordered_set<irep_idt> called_functions =
63  compute_called_functions(goto_functions);
64 
65  // eliminate those for which we already have a body
66 
67  std::set<irep_idt> missing_functions;
68 
69  for(const auto &id : called_functions)
70  {
71  goto_functionst::function_mapt::const_iterator
72  f_it=goto_functions.function_map.find(id);
73 
74  if(f_it!=goto_functions.function_map.end() &&
75  f_it->second.body_available())
76  {
77  // it's overridden!
78  }
79  else if(added_functions.find(id)!=added_functions.end())
80  {
81  // already added
82  }
83  else
84  missing_functions.insert(id);
85  }
86 
87  // done?
88  if(missing_functions.empty())
89  break;
90 
91  library(missing_functions, symbol_table, message_handler);
92 
93  // convert to CFG
94  for(const auto &id : missing_functions)
95  {
96  if(symbol_table.symbols.find(id)!=symbol_table.symbols.end())
97  goto_convert(id, symbol_table, goto_functions, message_handler);
98 
99  added_functions.insert(id);
100  }
101  }
102 }
void goto_convert(const codet &code, symbol_table_baset &symbol_table, goto_programt &dest, message_handlert &message_handler, const irep_idt &mode)
std::unordered_set< irep_idt > compute_called_functions(const goto_functionst &goto_functions)
computes the functions that are (potentially) called
function_mapt function_map
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:29
The symbol table.
Definition: symbol_table.h:19
A collection of goto functions.
const symbolst & symbols
Query Called Functions.
Goto Programs with Functions.
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:32