cprover
Loading...
Searching...
No Matches
goto_model.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Symbol Table + CFG
4
5Author: 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{
27public:
34
35 void clear()
36 {
39 }
40
42 {
43 }
44
45 // Copying is normally too expensive
46 goto_modelt(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)),
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
99 const validation_modet vm = validation_modet::INVARIANT,
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{
119public:
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
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
170private:
173};
174
183{
184public:
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
237private:
242};
243
244#endif // CPROVER_GOTO_PROGRAMS_GOTO_MODEL_H
Abstract interface to eager or lazy GOTO models.
Abstract interface to eager or lazy GOTO models.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
A collection of goto functions.
void unload(const irep_idt &name)
Remove function from the function map.
function_mapt function_map
::goto_functiont goto_functiont
void compute_location_numbers()
void validate(const namespacet &, validation_modet) const
Check that the goto functions are well-formed.
Interface providing access to a single function in a GOTO model, plus its associated symbol table.
Definition: goto_model.h:183
journalling_symbol_tablet & symbol_table
Definition: goto_model.h:238
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
const irep_idt & get_function_id()
Get function id.
Definition: goto_model.h:232
goto_functionst::goto_functiont & goto_function
Definition: goto_model.h:241
goto_functionst::goto_functiont & get_goto_function()
Get GOTO function.
Definition: goto_model.h:225
void compute_location_numbers()
Re-number our goto_function.
Definition: goto_model.h:209
journalling_symbol_tablet & get_symbol_table()
Get symbol table.
Definition: goto_model.h:218
goto_functionst & goto_functions
Definition: goto_model.h:239
const symbol_tablet & get_symbol_table() const override
Accessor to get the symbol table.
Definition: goto_model.h:77
const goto_functionst & get_goto_functions() const override
Accessor to get a raw goto_functionst.
Definition: goto_model.h:72
void unload(const irep_idt &name)
Definition: goto_model.h:68
void clear()
Definition: goto_model.h:35
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
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
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:30
goto_modelt(const goto_modelt &)=delete
goto_modelt & operator=(goto_modelt &&other)
Definition: goto_model.h:61
goto_modelt(goto_modelt &&other)
Definition: goto_model.h:55
goto_modelt & operator=(const goto_modelt &)=delete
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
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:33
A symbol table wrapper that records which entries have been updated/removedA caller can pass a journa...
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
The symbol table.
Definition: symbol_table.h:14
virtual void clear() override
Wipe internal state of the symbol table.
Definition: symbol_table.h:101
void validate(const validation_modet vm=validation_modet::INVARIANT) const
Check that the symbol table is well-formed.
Class providing the abstract GOTO model interface onto an unrelated symbol table and goto_functionst.
Definition: goto_model.h:118
const symbol_tablet & get_symbol_table() const override
Accessor to get the symbol table.
Definition: goto_model.h:133
const symbol_tablet & symbol_table
Definition: goto_model.h:171
const goto_functionst & get_goto_functions() const override
Accessor to get a raw goto_functionst.
Definition: goto_model.h:128
const goto_functionst & goto_functions
Definition: goto_model.h:172
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
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
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:138
Goto Programs with Functions.
Author: Diffblue Ltd.
STL namespace.
Author: Diffblue Ltd.
void validate_goto_model(const goto_functionst &goto_functions, const validation_modet vm, const goto_model_validation_optionst validation_options)
validation_modet