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 #include "validate_goto_model.h"
21 
22 // A model is a pair consisting of a symbol table
23 // and the CFGs for the functions.
24 
26 {
27 public:
34 
35  void clear()
36  {
39  }
40 
42  {
43  }
44 
45  // Copying is normally too expensive
46  goto_modelt(const goto_modelt &)=delete;
47  goto_modelt &operator=(const goto_modelt &)=delete;
48 
49  // Move operations need to be explicitly enabled as they are deleted with the
50  // copy operations
51  // default for move operations isn't available on Windows yet, so define
52  // explicitly (see https://msdn.microsoft.com/en-us/library/hh567368.aspx
53  // under "Defaulted and Deleted Functions")
54 
56  symbol_table(std::move(other.symbol_table)),
57  goto_functions(std::move(other.goto_functions))
58  {
59  }
60 
62  {
63  symbol_table=std::move(other.symbol_table);
64  goto_functions=std::move(other.goto_functions);
65  return *this;
66  }
67 
68  void unload(const irep_idt &name) { goto_functions.unload(name); }
69 
70  // Implement the abstract goto model interface:
71 
72  const goto_functionst &get_goto_functions() const override
73  {
74  return goto_functions;
75  }
76 
77  const symbol_tablet &get_symbol_table() const override
78  {
79  return symbol_table;
80  }
81 
83  const irep_idt &id) override
84  {
85  return goto_functions.function_map.at(id);
86  }
87 
88  bool can_produce_function(const irep_idt &id) const override
89  {
90  return goto_functions.function_map.find(id) !=
92  }
93 
98  void validate(
100  const goto_model_validation_optionst &goto_model_validation_options =
101  goto_model_validation_optionst{}) const override
102  {
104 
105  // Does a number of checks at the function_mapt level to ensure the
106  // goto_program is well formed. Does not call any validate methods
107  // (at the goto_functiont level or below)
108  validate_goto_model(goto_functions, vm, goto_model_validation_options);
109 
110  const namespacet ns(symbol_table);
111  goto_functions.validate(ns, vm);
112  }
113 };
114 
118 {
119 public:
125  {
126  }
127 
128  const goto_functionst &get_goto_functions() const override
129  {
130  return goto_functions;
131  }
132 
133  const symbol_tablet &get_symbol_table() const override
134  {
135  return symbol_table;
136  }
137 
139  const irep_idt &id) override
140  {
141  return goto_functions.function_map.at(id);
142  }
143 
144  bool can_produce_function(const irep_idt &id) const override
145  {
146  return goto_functions.function_map.find(id) !=
148  }
149 
154  void validate(
155  const validation_modet vm,
156  const goto_model_validation_optionst &goto_model_validation_options)
157  const override
158  {
160 
161  // Does a number of checks at the function_mapt level to ensure the
162  // goto_program is well formed. Does not call any validate methods
163  // (at the goto_functiont level or below)
164  validate_goto_model(goto_functions, vm, goto_model_validation_options);
165 
166  const namespacet ns(symbol_table);
167  goto_functions.validate(ns, vm);
168  }
169 
170 private:
173 };
174 
183 {
184 public:
197  const irep_idt &function_id,
203  {
204  }
205 
210  {
212  }
213 
219  {
220  return symbol_table;
221  }
222 
226  {
227  return goto_function;
228  }
229 
233  {
234  return function_id;
235  }
236 
237 private:
242 };
243 
244 #endif // CPROVER_GOTO_PROGRAMS_GOTO_MODEL_H
void validate(const validation_modet vm=validation_modet::INVARIANT, const goto_model_validation_optionst &goto_model_validation_options=goto_model_validation_optionst{}) const override
Check that the goto model is well-formed.
Definition: goto_model.h:98
Abstract interface to eager or lazy GOTO models.
void validate(const validation_modet vm, const goto_model_validation_optionst &goto_model_validation_options) const override
Check that the goto model is well-formed.
Definition: goto_model.h:154
const irep_idt & get_function_id()
Get function id.
Definition: goto_model.h:232
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:241
Goto Programs with Functions.
function_mapt function_map
STL namespace.
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:30
journalling_symbol_tablet & symbol_table
Definition: goto_model.h:238
const goto_functionst & get_goto_functions() const override
Accessor to get a raw goto_functionst.
Definition: goto_model.h:72
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:144
const symbol_tablet & get_symbol_table() const override
Accessor to get the symbol table.
Definition: goto_model.h:133
goto_modelt & operator=(goto_modelt &&other)
Definition: goto_model.h:61
goto_functionst::goto_functiont & get_goto_function()
Get GOTO function.
Definition: goto_model.h:225
Abstract interface to eager or lazy GOTO models.
journalling_symbol_tablet & get_symbol_table()
Get symbol table.
Definition: goto_model.h:218
A symbol table wrapper that records which entries have been updated/removedA caller can pass a journa...
void validate_goto_model(const goto_functionst &goto_functions, const validation_modet vm, const goto_model_validation_optionst validation_options)
void compute_location_numbers()
wrapper_goto_modelt(const symbol_tablet &symbol_table, const goto_functionst &goto_functions)
Definition: goto_model.h:120
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:82
const goto_functionst & get_goto_functions() const override
Accessor to get a raw goto_functionst.
Definition: goto_model.h:128
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:91
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:172
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:88
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:36
Author: Diffblue Ltd.
goto_modelt & operator=(const goto_modelt &)=delete
void clear()
Definition: goto_model.h:35
void validate(const namespacet &, validation_modet) const
Check that the goto functions are well-formed.
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:138
const symbol_tablet & symbol_table
Definition: goto_model.h:171
void unload(const irep_idt &name)
Definition: goto_model.h:68
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:117
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:194
goto_functionst & goto_functions
Definition: goto_model.h:239
validation_modet
Author: Diffblue Ltd.
const symbol_tablet & get_symbol_table() const override
Accessor to get the symbol table.
Definition: goto_model.h:77
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:33
void compute_location_numbers()
Re-number our goto_function.
Definition: goto_model.h:209
goto_modelt(goto_modelt &&other)
Definition: goto_model.h:55
Interface providing access to a single function in a GOTO model, plus its associated symbol table...
Definition: goto_model.h:182