cprover
Loading...
Searching...
No Matches
link_to_library.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Library Linking
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
11
12#include "link_to_library.h"
13
16#include "goto_model.h"
17
26 goto_modelt &goto_model,
27 message_handlert &message_handler,
28 const std::function<
29 void(const std::set<irep_idt> &, symbol_tablet &, message_handlert &)>
30 &library)
31{
32 // this needs a fixedpoint, as library functions
33 // may depend on other library functions
34
35 std::set<irep_idt> added_functions;
36
37 while(true)
38 {
39 std::unordered_set<irep_idt> called_functions =
41
42 // eliminate those for which we already have a body
43
44 std::set<irep_idt> missing_functions;
45
46 for(const auto &id : called_functions)
47 {
48 goto_functionst::function_mapt::const_iterator f_it =
49 goto_model.goto_functions.function_map.find(id);
50
51 if(
52 f_it != goto_model.goto_functions.function_map.end() &&
53 f_it->second.body_available())
54 {
55 // it's overridden!
56 }
57 else if(added_functions.find(id) != added_functions.end())
58 {
59 // already added
60 }
61 else
62 missing_functions.insert(id);
63 }
64
65 // done?
66 if(missing_functions.empty())
67 break;
68
69 library(missing_functions, goto_model.symbol_table, message_handler);
70
71 // convert to CFG
72 for(const auto &id : missing_functions)
73 {
74 if(
75 goto_model.symbol_table.symbols.find(id) !=
76 goto_model.symbol_table.symbols.end())
77 {
79 id,
80 goto_model.symbol_table,
81 goto_model.goto_functions,
82 message_handler);
83 }
84
85 added_functions.insert(id);
86 }
87 }
88}
function_mapt function_map
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:30
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:33
const symbolst & symbols
Read-only field, used to look up symbols given their names.
The symbol table.
Definition: symbol_table.h:14
std::unordered_set< irep_idt > compute_called_functions(const goto_functionst &goto_functions)
computes the functions that are (potentially) called
Query Called Functions.
void goto_convert(const codet &code, symbol_table_baset &symbol_table, goto_programt &dest, message_handlert &message_handler, const irep_idt &mode)
Goto Programs with Functions.
Symbol Table + CFG.