Skip to content

Commit 5d75f2e

Browse files
Merge pull request diffblue#223 from diffblue/feature/test-symbol_tablet
Updates to recording_symbol_tablet
2 parents 7494ca0 + 4d1ee5e commit 5d75f2e

File tree

2 files changed

+352
-6
lines changed

2 files changed

+352
-6
lines changed

cbmc/src/util/recording_symbol_table.h

Lines changed: 24 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -20,12 +20,16 @@ class recording_symbol_tablet:public symbol_tablet
2020
typedef std::unordered_set<irep_idt, irep_id_hash> changesett;
2121
private:
2222
symbol_tablet &base_symbol_table;
23+
// Symbols originally in the table will never be marked inserted
24+
changesett inserted;
25+
// get_writeable marks an existing symbol updated
26+
// Inserted symbols are marked updated, removed ones aren't
2327
changesett updated;
28+
// Symbols not originally in the table will never be marked removed
2429
changesett removed;
2530

26-
public:
27-
// NOLINTNEXTLINE(runtime/explicit) - No information is lost in conversion
28-
recording_symbol_tablet(symbol_tablet &base_symbol_table)
31+
private:
32+
explicit recording_symbol_tablet(symbol_tablet &base_symbol_table)
2933
: symbol_tablet(
3034
base_symbol_table.symbols,
3135
base_symbol_table.symbol_base_map,
@@ -34,6 +38,7 @@ class recording_symbol_tablet:public symbol_tablet
3438
{
3539
}
3640

41+
public:
3742
recording_symbol_tablet(const recording_symbol_tablet &other)
3843
: symbol_tablet(
3944
other.base_symbol_table.symbols,
@@ -43,6 +48,11 @@ class recording_symbol_tablet:public symbol_tablet
4348
{
4449
}
4550

51+
static recording_symbol_tablet wrap(symbol_tablet &base_symbol_table)
52+
{
53+
return recording_symbol_tablet(base_symbol_table);
54+
}
55+
4656
virtual opt_symbol_reft get_writeable(const irep_idt &identifier) override
4757
{
4858
opt_symbol_reft result=base_symbol_table.get_writeable(identifier);
@@ -56,7 +66,7 @@ class recording_symbol_tablet:public symbol_tablet
5666
std::pair<symbolt &, bool> result=
5767
base_symbol_table.insert(std::move(symbol));
5868
if(result.second)
59-
on_update(result.first.name);
69+
on_insert(result.first.name);
6070
return result;
6171
}
6272

@@ -73,19 +83,27 @@ class recording_symbol_tablet:public symbol_tablet
7383
base_symbol_table.clear();
7484
}
7585

86+
const changesett &get_inserted() const { return inserted; }
7687
const changesett &get_updated() const { return updated; }
7788
const changesett &get_removed() const { return removed; }
7889

7990
private:
91+
void on_insert(const irep_idt &id)
92+
{
93+
if(removed.erase(id)==0)
94+
inserted.insert(id);
95+
updated.insert(id);
96+
}
97+
8098
void on_update(const irep_idt &id)
8199
{
82100
updated.insert(id);
83-
removed.erase(id);
84101
}
85102

86103
void on_remove(const irep_idt &id)
87104
{
88-
removed.insert(id);
105+
if(inserted.erase(id)==0)
106+
removed.insert(id);
89107
updated.erase(id);
90108
}
91109
};

0 commit comments

Comments
 (0)