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
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 
141 private:
144 };
145 
154 {
155 public:
168  const irep_idt &function_id,
174  {
175  }
176 
181  {
183  }
184 
188  {
189  goto_function.update_instructions_function(function_id);
190  }
191 
197  {
198  return symbol_table;
199  }
200 
204  {
205  return goto_function;
206  }
207 
211  {
212  return function_id;
213  }
214 
215 private:
220 };
221 
222 #endif // CPROVER_GOTO_PROGRAMS_GOTO_MODEL_H
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
symbol_tablet
The symbol table.
Definition: symbol_table.h:19
goto_model_functiont::function_id
irep_idt function_id
Definition: goto_model.h:218
goto_modelt::unload
void unload(const irep_idt &name)
Definition: goto_model.h:67
goto_model_functiont::symbol_table
journalling_symbol_tablet & symbol_table
Definition: goto_model.h:216
wrapper_goto_modelt::wrapper_goto_modelt
wrapper_goto_modelt(const symbol_tablet &symbol_table, const goto_functionst &goto_functions)
Definition: goto_model.h:111
goto_modelt::clear
void clear()
Definition: goto_model.h:34
goto_modelt::goto_modelt
goto_modelt()
Definition: goto_model.h:40
wrapper_goto_modelt::goto_functions
const goto_functionst & goto_functions
Definition: goto_model.h:143
goto_model_functiont::goto_functions
goto_functionst & goto_functions
Definition: goto_model.h:217
goto_model_functiont::get_function_id
const irep_idt & get_function_id()
Get function id.
Definition: goto_model.h:210
goto_functionst::compute_location_numbers
void compute_location_numbers()
Definition: goto_functions.cpp:18
goto_modelt::goto_modelt
goto_modelt(goto_modelt &&other)
Definition: goto_model.h:54
goto_modelt
Definition: goto_model.h:24
journalling_symbol_table.h
Author: Diffblue Ltd.
goto_model_functiont::goto_model_functiont
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:165
symbol_tablet::validate
void validate(const validation_modet vm=validation_modet::INVARIANT) const
Check that the symbol table is well-formed.
Definition: symbol_table.cpp:123
wrapper_goto_modelt::get_goto_function
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
goto_functionst::function_map
function_mapt function_map
Definition: goto_functions.h:27
goto_modelt::validate
void validate(const validation_modet vm) const
Check that the goto model is well-formed.
Definition: goto_model.h:97
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
goto_modelt::get_goto_functions
const goto_functionst & get_goto_functions() const override
Accessor to get a raw goto_functionst.
Definition: goto_model.h:71
goto_functionst::clear
void clear()
Definition: goto_functions.h:70
abstract_goto_model.h
validation_modet
validation_modet
Definition: validation_mode.h:12
goto_model_functiont::get_symbol_table
journalling_symbol_tablet & get_symbol_table()
Get symbol table.
Definition: goto_model.h:196
goto_model_functiont::compute_location_numbers
void compute_location_numbers()
Re-number our goto_function.
Definition: goto_model.h:180
goto_model_functiont::goto_function
goto_functionst::goto_functiont & goto_function
Definition: goto_model.h:219
goto_modelt::operator=
goto_modelt & operator=(goto_modelt &&other)
Definition: goto_model.h:60
symbol_tablet::clear
virtual void clear() override
Wipe internal state of the symbol table.
Definition: symbol_table.h:104
goto_modelt::get_goto_function
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
goto_functionst::unload
void unload(const irep_idt &name)
Remove function from the function map.
Definition: goto_functions.h:68
goto_functionst::goto_functiont
::goto_functiont goto_functiont
Definition: goto_functions.h:25
goto_modelt::can_produce_function
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
goto_modelt::operator=
goto_modelt & operator=(const goto_modelt &)=delete
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:22
goto_functionst::validate
void validate(const namespacet &ns, const validation_modet vm) const
Check that the goto functions are well-formed.
Definition: goto_functions.h:125
wrapper_goto_modelt
Class providing the abstract GOTO model interface onto an unrelated symbol table and goto_functionst.
Definition: goto_model.h:108
wrapper_goto_modelt::get_symbol_table
const symbol_tablet & get_symbol_table() const override
Accessor to get the symbol table.
Definition: goto_model.h:124
goto_modelt::goto_functions
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:32
goto_modelt::get_symbol_table
const symbol_tablet & get_symbol_table() const override
Accessor to get the symbol table.
Definition: goto_model.h:76
goto_functions.h
abstract_goto_modelt
Abstract interface to eager or lazy GOTO models.
Definition: abstract_goto_model.h:19
wrapper_goto_modelt::get_goto_functions
const goto_functionst & get_goto_functions() const override
Accessor to get a raw goto_functionst.
Definition: goto_model.h:119
goto_model_functiont::get_goto_function
goto_functionst::goto_functiont & get_goto_function()
Get GOTO function.
Definition: goto_model.h:203
symbol_table.h
Author: Diffblue Ltd.
journalling_symbol_tablet
A symbol table wrapper that records which entries have been updated/removed.
Definition: journalling_symbol_table.h:35
goto_modelt::symbol_table
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:29
goto_model_functiont::update_instructions_function
void update_instructions_function()
Updates the empty function member of each instruction by setting them to function_id
Definition: goto_model.h:187
wrapper_goto_modelt::can_produce_function
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
goto_model_functiont
Interface providing access to a single function in a GOTO model, plus its associated symbol table.
Definition: goto_model.h:153
wrapper_goto_modelt::symbol_table
const symbol_tablet & symbol_table
Definition: goto_model.h:142