cprover
goto_model.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Symbol Table + CFG
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_GOTO_PROGRAMS_GOTO_MODEL_H
13 #define CPROVER_GOTO_PROGRAMS_GOTO_MODEL_H
14 
15 #include <util/symbol_table.h>
17 
18 #include "abstract_goto_model.h"
19 #include "goto_functions.h"
20 
21 // A model is a pair consisting of a symbol table
22 // and the CFGs for the functions.
23 
25 {
26 public:
33 
34  void clear()
35  {
38  }
39 
40  void output(std::ostream &out) const
41  {
43  goto_functions.output(ns, out);
44  }
45 
47  {
48  }
49 
50  // Copying is normally too expensive
51  goto_modelt(const goto_modelt &)=delete;
52  goto_modelt &operator=(const goto_modelt &)=delete;
53 
54  // Move operations need to be explicitly enabled as they are deleted with the
55  // copy operations
56  // default for move operations isn't available on Windows yet, so define
57  // explicitly (see https://msdn.microsoft.com/en-us/library/hh567368.aspx
58  // under "Defaulted and Deleted Functions")
59 
61  symbol_table(std::move(other.symbol_table)),
62  goto_functions(std::move(other.goto_functions))
63  {
64  }
65 
67  {
68  symbol_table=std::move(other.symbol_table);
69  goto_functions=std::move(other.goto_functions);
70  return *this;
71  }
72 
73  void unload(const irep_idt &name) { goto_functions.unload(name); }
74 
75  // Implement the abstract goto model interface:
76 
77  const goto_functionst &get_goto_functions() const override
78  {
79  return goto_functions;
80  }
81 
82  const symbol_tablet &get_symbol_table() const override
83  {
84  return symbol_table;
85  }
86 
88  const irep_idt &id) override
89  {
90  return goto_functions.function_map.at(id);
91  }
92 
93  bool can_produce_function(const irep_idt &id) const override
94  {
95  return goto_functions.function_map.find(id) !=
97  }
98 };
99 
103 {
104 public:
110  {
111  }
112 
113  const goto_functionst &get_goto_functions() const override
114  {
115  return goto_functions;
116  }
117 
118  const symbol_tablet &get_symbol_table() const override
119  {
120  return symbol_table;
121  }
122 
124  const irep_idt &id) override
125  {
126  return goto_functions.function_map.at(id);
127  }
128 
129  bool can_produce_function(const irep_idt &id) const override
130  {
131  return goto_functions.function_map.find(id) !=
133  }
134 
135 private:
138 };
139 
148 {
149 public:
156  journalling_symbol_tablet &symbol_table,
158  const irep_idt &function_id,
164  {
165  }
166 
171  {
173  }
174 
178  {
179  goto_function.update_instructions_function(function_id);
180  }
181 
186  journalling_symbol_tablet &get_symbol_table()
187  {
188  return symbol_table;
189  }
190 
194  {
195  return goto_function;
196  }
197 
201  {
202  return function_id;
203  }
204 
205 private:
206  journalling_symbol_tablet &symbol_table;
210 };
211 
212 #endif // CPROVER_GOTO_PROGRAMS_GOTO_MODEL_H
Abstract interface to eager or lazy GOTO models.
const irep_idt & get_function_id()
Get function id.
Definition: goto_model.h:200
void update_instructions_function()
Updates the empty function member of each instruction by setting them to function_id ...
Definition: goto_model.h:177
virtual void clear() override
Definition: symbol_table.h:97
goto_functionst::goto_functiont & goto_function
Definition: goto_model.h:209
Goto Programs with Functions.
function_mapt function_map
STL namespace.
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:29
journalling_symbol_tablet & symbol_table
Definition: goto_model.h:206
const goto_functionst & get_goto_functions() const override
Accessor to get a raw goto_functionst.
Definition: goto_model.h:77
bool can_produce_function(const irep_idt &id) const override
Determines if this model can produce a body for the given function.
Definition: goto_model.h:129
const symbol_tablet & get_symbol_table() const override
Accessor to get the symbol table.
Definition: goto_model.h:118
goto_modelt & operator=(goto_modelt &&other)
Definition: goto_model.h:66
goto_functionst::goto_functiont & get_goto_function()
Get GOTO function.
Definition: goto_model.h:193
Abstract interface to eager or lazy GOTO models.
journalling_symbol_tablet & get_symbol_table()
Get symbol table.
Definition: goto_model.h:186
void compute_location_numbers()
wrapper_goto_modelt(const symbol_tablet &symbol_table, const goto_functionst &goto_functions)
Definition: goto_model.h:105
const goto_functionst::goto_functiont & get_goto_function(const irep_idt &id) override
Get a GOTO function by name, or throw if no such function exists.
Definition: goto_model.h:87
void output(const namespacet &ns, std::ostream &out) const
const goto_functionst & get_goto_functions() const override
Accessor to get a raw goto_functionst.
Definition: goto_model.h:113
The symbol table.
Definition: symbol_table.h:19
TO_BE_DOCUMENTED.
Definition: namespace.h:74
::goto_functiont goto_functiont
const goto_functionst & goto_functions
Definition: goto_model.h:137
bool can_produce_function(const irep_idt &id) const override
Determines if this model can produce a body for the given function.
Definition: goto_model.h:93
Author: Diffblue Ltd.
goto_modelt & operator=(const goto_modelt &)=delete
void clear()
Definition: goto_model.h:34
const goto_functionst::goto_functiont & get_goto_function(const irep_idt &id) override
Get a GOTO function by name, or throw if no such function exists.
Definition: goto_model.h:123
const symbol_tablet & symbol_table
Definition: goto_model.h:136
void unload(const irep_idt &name)
Definition: goto_model.h:73
void unload(const irep_idt &name)
Class providing the abstract GOTO model interface onto an unrelated symbol table and goto_functionst...
Definition: goto_model.h:102
goto_model_functiont(journalling_symbol_tablet &symbol_table, goto_functionst &goto_functions, const irep_idt &function_id, goto_functionst::goto_functiont &goto_function)
Construct a function wrapper.
Definition: goto_model.h:155
goto_functionst & goto_functions
Definition: goto_model.h:207
Author: Diffblue Ltd.
const symbol_tablet & get_symbol_table() const override
Accessor to get the symbol table.
Definition: goto_model.h:82
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:32
void compute_location_numbers()
Re-number our goto_function.
Definition: goto_model.h:170
goto_modelt(goto_modelt &&other)
Definition: goto_model.h:60
void output(std::ostream &out) const
Definition: goto_model.h:40
Interface providing access to a single function in a GOTO model, plus its associated symbol table...
Definition: goto_model.h:147