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 
41  {
42  }
43 
44  // Copying is normally too expensive
45  goto_modelt(const goto_modelt &)=delete;
46  goto_modelt &operator=(const goto_modelt &)=delete;
47 
48  // Move operations need to be explicitly enabled as they are deleted with the
49  // copy operations
50  // default for move operations isn't available on Windows yet, so define
51  // explicitly (see https://msdn.microsoft.com/en-us/library/hh567368.aspx
52  // under "Defaulted and Deleted Functions")
53 
55  symbol_table(std::move(other.symbol_table)),
56  goto_functions(std::move(other.goto_functions))
57  {
58  }
59 
61  {
62  symbol_table=std::move(other.symbol_table);
63  goto_functions=std::move(other.goto_functions);
64  return *this;
65  }
66 
67  void unload(const irep_idt &name) { goto_functions.unload(name); }
68 
69  // Implement the abstract goto model interface:
70 
71  const goto_functionst &get_goto_functions() const override
72  {
73  return goto_functions;
74  }
75 
76  const symbol_tablet &get_symbol_table() const override
77  {
78  return symbol_table;
79  }
80 
82  const irep_idt &id) override
83  {
84  return goto_functions.function_map.at(id);
85  }
86 
87  bool can_produce_function(const irep_idt &id) const override
88  {
89  return goto_functions.function_map.find(id) !=
91  }
92 
97  void validate(const validation_modet vm) const override
98  {
100 
101  const namespacet ns(symbol_table);
102  goto_functions.validate(ns, vm);
103  }
104 };
105 
109 {
110 public:
116  {
117  }
118 
119  const goto_functionst &get_goto_functions() const override
120  {
121  return goto_functions;
122  }
123 
124  const symbol_tablet &get_symbol_table() const override
125  {
126  return symbol_table;
127  }
128 
130  const irep_idt &id) override
131  {
132  return goto_functions.function_map.at(id);
133  }
134 
135  bool can_produce_function(const irep_idt &id) const override
136  {
137  return goto_functions.function_map.find(id) !=
139  }
140 
145  void validate(const validation_modet vm) const override
146  {
148 
149  const namespacet ns(symbol_table);
150  goto_functions.validate(ns, vm);
151  }
152 
153 private:
156 };
157 
166 {
167 public:
180  const irep_idt &function_id,
186  {
187  }
188 
193  {
195  }
196 
200  {
201  goto_function.update_instructions_function(function_id);
202  }
203 
209  {
210  return symbol_table;
211  }
212 
216  {
217  return goto_function;
218  }
219 
223  {
224  return function_id;
225  }
226 
227 private:
232 };
233 
234 #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:222
void update_instructions_function()
Updates the empty function member of each instruction by setting them to function_id ...
Definition: goto_model.h:199
virtual void clear() override
Wipe internal state of the symbol table.
Definition: symbol_table.h:104
goto_functionst::goto_functiont & goto_function
Definition: goto_model.h:231
void validate(const namespacet &ns, const validation_modet vm) const
Check that the goto functions are well-formed.
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:228
const goto_functionst & get_goto_functions() const override
Accessor to get a raw goto_functionst.
Definition: goto_model.h:71
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:135
const symbol_tablet & get_symbol_table() const override
Accessor to get the symbol table.
Definition: goto_model.h:124
goto_modelt & operator=(goto_modelt &&other)
Definition: goto_model.h:60
goto_functionst::goto_functiont & get_goto_function()
Get GOTO function.
Definition: goto_model.h:215
Abstract interface to eager or lazy GOTO models.
journalling_symbol_tablet & get_symbol_table()
Get symbol table.
Definition: goto_model.h:208
A symbol table wrapper that records which entries have been updated/removedA caller can pass a journa...
void compute_location_numbers()
wrapper_goto_modelt(const symbol_tablet &symbol_table, const goto_functionst &goto_functions)
Definition: goto_model.h:111
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:81
const goto_functionst & get_goto_functions() const override
Accessor to get a raw goto_functionst.
Definition: goto_model.h:119
The symbol table.
Definition: symbol_table.h:19
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
void validate(const validation_modet vm=validation_modet::INVARIANT) const
Check that the symbol table is well-formed.
::goto_functiont goto_functiont
const goto_functionst & goto_functions
Definition: goto_model.h:155
A collection of goto functions.
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:87
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:35
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:129
const symbol_tablet & symbol_table
Definition: goto_model.h:154
void unload(const irep_idt &name)
Definition: goto_model.h:67
void unload(const irep_idt &name)
Remove function from the function map.
Class providing the abstract GOTO model interface onto an unrelated symbol table and goto_functionst...
Definition: goto_model.h:108
void validate(const validation_modet vm) const override
Check that the goto model is well-formed.
Definition: goto_model.h:97
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:177
goto_functionst & goto_functions
Definition: goto_model.h:229
validation_modet
Author: Diffblue Ltd.
const symbol_tablet & get_symbol_table() const override
Accessor to get the symbol table.
Definition: goto_model.h:76
void validate(const validation_modet vm) const override
Check that the goto model is well-formed.
Definition: goto_model.h:145
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:32
void compute_location_numbers()
Re-number our goto_function.
Definition: goto_model.h:192
goto_modelt(goto_modelt &&other)
Definition: goto_model.h:54
Interface providing access to a single function in a GOTO model, plus its associated symbol table...
Definition: goto_model.h:165