|
15 | 15 | #include <util/symbol_table.h>
|
16 | 16 | #include <util/journalling_symbol_table.h>
|
17 | 17 |
|
| 18 | +#include "abstract_goto_model.h" |
18 | 19 | #include "goto_functions.h"
|
19 | 20 |
|
20 | 21 | // A model is a pair consisting of a symbol table
|
21 | 22 | // and the CFGs for the functions.
|
22 | 23 |
|
23 |
| -class goto_modelt |
| 24 | +class goto_modelt : public abstract_goto_modelt |
24 | 25 | {
|
25 | 26 | public:
|
| 27 | + /// Symbol table. Direct access is deprecated; use the abstract_goto_modelt |
| 28 | + /// interface instead if possible. |
26 | 29 | symbol_tablet symbol_table;
|
| 30 | + /// GOTO functions. Direct access is deprecated; use the abstract_goto_modelt |
| 31 | + /// interface instead if possible. |
27 | 32 | goto_functionst goto_functions;
|
28 | 33 |
|
29 | 34 | void clear()
|
@@ -66,6 +71,68 @@ class goto_modelt
|
66 | 71 | }
|
67 | 72 |
|
68 | 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 | + |
| 87 | + const goto_functionst::goto_functiont &get_goto_function( |
| 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.count(id); |
| 96 | + } |
| 97 | +}; |
| 98 | + |
| 99 | +/// Class providing the abstract GOTO model interface onto an unrelated |
| 100 | +/// symbol table and goto_functionst. |
| 101 | +class wrapper_goto_modelt : public abstract_goto_modelt |
| 102 | +{ |
| 103 | +public: |
| 104 | + wrapper_goto_modelt( |
| 105 | + const symbol_tablet &symbol_table, |
| 106 | + const goto_functionst &goto_functions) : |
| 107 | + symbol_table(symbol_table), |
| 108 | + goto_functions(goto_functions) |
| 109 | + { |
| 110 | + } |
| 111 | + |
| 112 | + const goto_functionst &get_goto_functions() const override |
| 113 | + { |
| 114 | + return goto_functions; |
| 115 | + } |
| 116 | + |
| 117 | + const symbol_tablet &get_symbol_table() const override |
| 118 | + { |
| 119 | + return symbol_table; |
| 120 | + } |
| 121 | + |
| 122 | + const goto_functionst::goto_functiont &get_goto_function( |
| 123 | + const irep_idt &id) override |
| 124 | + { |
| 125 | + return goto_functions.function_map.at(id); |
| 126 | + } |
| 127 | + |
| 128 | + bool can_produce_function(const irep_idt &id) const override |
| 129 | + { |
| 130 | + return goto_functions.function_map.count(id); |
| 131 | + } |
| 132 | + |
| 133 | +private: |
| 134 | + const symbol_tablet &symbol_table; |
| 135 | + const goto_functionst &goto_functions; |
69 | 136 | };
|
70 | 137 |
|
71 | 138 | /// Interface providing access to a single function in a GOTO model, plus its
|
|
0 commit comments