replica
/
diffblue-cbmc
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

Remove the empty_data static field of sharing_node_innert/sharing_node_leaft 

A sharing node is now considered empty when its contained shared pointer is
empty.
This commit is contained in:
Daniel Poetzl 2019-03-20 16:41:03 +00:00
parent 2614c5bac9
commit 380028419e
1 changed files with 9 additions and 21 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

30
src/util/sharing_node.h
View File

@ -113,18 +113,18 @@ public:
typedef typename d_ct::leaft leaft;
typedef typename d_ct::leaf_listt leaf_listt;
sharing_node_innert() : data(empty_data)
sharing_node_innert()
{
}
bool empty() const
{
return data == empty_data;
return !data;
}
void clear()
{
data = empty_data;
data.reset();
}
bool shares_with(const sharing_node_innert &other) const
@ -153,7 +153,7 @@ public:
d_it &write_internal()
{
if(data == empty_data)
if(!data)
{
data = make_shared_derived_u<SN_PTR_TYPE_ARGS>();
}
@ -176,7 +176,7 @@ public:
d_ct &write_container()
{
if(data == empty_data)
if(!data)
{
data = make_shared_derived_v<SN_PTR_TYPE_ARGS>();
}
@ -339,13 +339,8 @@ public:
}
small_shared_two_way_ptrt<SN_PTR_TYPE_ARGS> data;
static small_shared_two_way_ptrt<SN_PTR_TYPE_ARGS> empty_data;
};
SN_TYPE_PAR_DEF small_shared_two_way_ptrt<SN_PTR_TYPE_ARGS>
sharing_node_innert<SN_TYPE_ARGS>::empty_data =
small_shared_two_way_ptrt<SN_PTR_TYPE_ARGS>();
// Leafs
SN_TYPE_PAR_DECL class d_leaft : public small_shared_pointeet<unsigned>
@ -364,7 +359,7 @@ SN_TYPE_PAR_DEF class sharing_node_leaft : public sharing_node_baset
public:
typedef d_leaft<SN_TYPE_ARGS> d_lt;
sharing_node_leaft(const keyT &k, const valueT &v) : data(empty_data)
sharing_node_leaft(const keyT &k, const valueT &v)
{
SN_ASSERT(empty());
@ -384,12 +379,12 @@ public:
bool empty() const
{
return data == empty_data;
return !data;
}
void clear()
{
data = empty_data;
data.reset();
}
bool shares_with(const sharing_node_leaft &other) const
@ -404,9 +399,7 @@ public:
d_lt &write()
{
SN_ASSERT(data.use_count() > 0);
if(data == empty_data)
if(!data)
{
data = make_small_shared_ptr<d_lt>();
}
@ -453,11 +446,6 @@ public:
}
small_shared_ptrt<SN_PTR_TYPE_ARG> data;
static small_shared_ptrt<SN_PTR_TYPE_ARG> empty_data;
};
SN_TYPE_PAR_DEF small_shared_ptrt<SN_PTR_TYPE_ARG>
sharing_node_leaft<SN_TYPE_ARGS>::empty_data =
make_small_shared_ptr<SN_PTR_TYPE_ARG>();
#endif