CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
symbol_table_builder.h
Go to the documentation of this file.
1
2
3// \file Contains a symbol table wrapper that keeps track of suffixes
4// that have been used for their prefix
5
6#ifndef CPROVER_UTIL_SYMBOL_TABLE_BUILDER_H
7#define CPROVER_UTIL_SYMBOL_TABLE_BUILDER_H
8
9#include "symbol_table_base.h"
10
14{
15private:
17 mutable std::map<std::string, std::size_t> next_free_suffix_for_prefix;
18
19public:
28
37
41
46
47 const symbol_tablet &get_symbol_table() const override
48 {
50 }
51
52 void erase(const symbolst::const_iterator &entry) override
53 {
55 }
56
57 void clear() override
58 {
61 }
62
63 bool move(symbolt &symbol, symbolt *&new_symbol) override
64 {
65 return base_symbol_table.move(symbol, new_symbol);
66 }
67
68 symbolt *get_writeable(const irep_idt &identifier) override
69 {
70 return base_symbol_table.get_writeable(identifier);
71 }
72
73 std::pair<symbolt &, bool> insert(symbolt symbol) override
74 {
75 return base_symbol_table.insert(std::move(symbol));
76 }
77
78 iteratort begin() override
79 {
80 return base_symbol_table.begin();
81 }
82
83 iteratort end() override
84 {
85 return base_symbol_table.end();
86 }
87
90
92 const validation_modet vm = validation_modet::INVARIANT) const override
93 {
95 }
96
107 std::size_t next_unused_suffix(const std::string &prefix) const override
108 {
109 // Check if we have an entry for this particular suffix, if not,
110 // create baseline.
111 auto suffix_iter = next_free_suffix_for_prefix.insert({prefix, 0}).first;
112 std::size_t free_suffix =
114 suffix_iter->second = free_suffix + 1;
115 return free_suffix;
116 }
117};
118
119#endif // CPROVER_UTIL_SYMBOL_TABLE_BUILDER_H
virtual void clear()
Reset the abstract state.
Definition ai.h:265
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
The symbol table base class interface.
const symbol_base_mapt & symbol_base_map
Read-only field, used to look up symbol names given their base names.
virtual void clear()=0
virtual void validate(const validation_modet vm=validation_modet::INVARIANT) const =0
virtual bool move(symbolt &symbol, symbolt *&new_symbol)=0
virtual std::pair< symbolt &, bool > insert(symbolt symbol)=0
Move or copy a new symbol to the symbol table.
virtual symbolt * get_writeable(const irep_idt &name)=0
Find a symbol in the symbol table for read-write access.
virtual void erase(const symbolst::const_iterator &entry)=0
Remove a symbol from the symbol table.
const symbol_module_mapt & symbol_module_map
Read-only field, used to look up symbol names given their modules.
virtual iteratort begin()=0
std::size_t next_unused_suffix(const std::string &prefix, std::size_t start_number) const
Find smallest unused integer i so that prefix + std::to_string(i) does not exist in the list symbols.
const symbolst & symbols
Read-only field, used to look up symbols given their names.
virtual iteratort end()=0
virtual const symbol_tablet & get_symbol_table() const =0
Author: Diffblue Ltd.
symbol_table_buildert(symbol_table_baset &base_symbol_table)
iteratort end() override
symbol_table_buildert(const symbol_table_buildert &)=delete
symbol_table_baset & base_symbol_table
const symbol_tablet & get_symbol_table() const override
symbol_table_buildert & operator=(const symbol_table_buildert &)=delete
std::map< std::string, std::size_t > next_free_suffix_for_prefix
bool move(symbolt &symbol, symbolt *&new_symbol) override
void validate(const validation_modet vm=validation_modet::INVARIANT) const override
std::pair< symbolt &, bool > insert(symbolt symbol) override
Move or copy a new symbol to the symbol table.
std::size_t next_unused_suffix(const std::string &prefix) const override
Try to find the next free identity for the passed-in prefix in this symbol table.
symbolt * get_writeable(const irep_idt &identifier) override
Find a symbol in the symbol table for read-write access.
static symbol_table_buildert wrap(symbol_table_baset &base_symbol_table)
iteratort begin() override
symbol_table_buildert(symbol_table_buildert &&other)
symbol_table_buildert & operator=(symbol_table_buildert &&)=delete
void erase(const symbolst::const_iterator &entry) override
Remove a symbol from the symbol table.
The symbol table.
Symbol table entry.
Definition symbol.h:28
Author: Diffblue Ltd.
validation_modet