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 
14 #include <util/config.h>
15 
16 #include <ansi-c/cprover_library.h>
17 
19 #include "goto_convert_functions.h"
20 
22  goto_modelt &goto_model,
23  message_handlert &message_handler)
24 {
26  goto_model.symbol_table,
27  goto_model.goto_functions,
28  message_handler);
29 }
30 
32  symbol_tablet &symbol_table,
33  goto_functionst &goto_functions,
34  message_handlert &message_handler)
35 {
36  // this needs a fixedpoint, as library functions
37  // may depend on other library functions
38 
39  messaget message(message_handler);
40 
41  message.status() << "Adding CPROVER library ("
42  << config.ansi_c.arch << ")" << messaget::eom;
43 
44  std::set<irep_idt> added_functions;
45 
46  while(true)
47  {
48  std::set<irep_idt> called_functions;
49  compute_called_functions(goto_functions, called_functions);
50 
51  // eliminate those for which we already have a body
52 
53  std::set<irep_idt> missing_functions;
54 
55  for(const auto &id : called_functions)
56  {
57  goto_functionst::function_mapt::const_iterator
58  f_it=goto_functions.function_map.find(id);
59 
60  if(f_it!=goto_functions.function_map.end() &&
61  f_it->second.body_available())
62  {
63  // it's overridden!
64  }
65  else if(added_functions.find(id)!=added_functions.end())
66  {
67  // already added
68  }
69  else
70  missing_functions.insert(id);
71  }
72 
73  // done?
74  if(missing_functions.empty())
75  break;
76 
77  add_cprover_library(missing_functions, symbol_table, message_handler);
78 
79  // convert to CFG
80  for(const auto &id : missing_functions)
81  {
82  if(symbol_table.symbols.find(id)!=symbol_table.symbols.end())
83  goto_convert(id, symbol_table, goto_functions, message_handler);
84 
85  added_functions.insert(id);
86  }
87  }
88 }
struct configt::ansi_ct ansi_c
void goto_convert(const codet &code, symbol_tablet &symbol_table, goto_programt &dest, message_handlert &message_handler)
mstreamt & status()
Definition: message.h:238
symbol_tablet symbol_table
Definition: goto_model.h:25
static mstreamt & eom(mstreamt &m)
Definition: message.h:193
configt config
Definition: config.cpp:21
symbolst symbols
Definition: symbol_table.h:57
The symbol table.
Definition: symbol_table.h:52
irep_idt arch
Definition: config.h:83
Query Called Functions.
Goto Programs with Functions.
void compute_called_functions(const goto_functionst &goto_functions, std::set< irep_idt > &functions)
computes the functions that are (potentially) called
void add_cprover_library(const std::set< irep_idt > &functions, symbol_tablet &symbol_table, message_handlert &message_handler)
goto_functionst goto_functions
Definition: goto_model.h:26