@@ -12,9 +12,9 @@ Author: Daniel Poetzl
12
12
#ifndef CPROVER_UTIL_SHARING_MAP_H
13
13
#define CPROVER_UTIL_SHARING_MAP_H
14
14
15
- // #define DEBUG
15
+ // #define SM_DEBUG
16
16
17
- #ifdef DEBUG
17
+ #ifdef SM_DEBUG
18
18
#include < iostream>
19
19
#endif
20
20
@@ -31,14 +31,14 @@ Author: Daniel Poetzl
31
31
#include " sharing_node.h"
32
32
#include " threeval.h"
33
33
34
- // #define SHARING_MAP_INTERNAL_CHECKS
34
+ // #define SM_INTERNAL_CHECKS
35
35
36
- #ifdef SHARING_MAP_INTERNAL_CHECKS
37
- #define _sm_assert (b ) INVARIANT(b, " Sharing map internal invariant" )
38
- #define _sm_assert_use (v, b ) _sm_assert (b)
36
+ #ifdef SM_INTERNAL_CHECKS
37
+ #define SM_ASSERT (b ) INVARIANT(b, " Sharing map internal invariant" )
38
+ #define SM_ASSERT_USE (v, b ) SM_ASSERT (b)
39
39
#else
40
- #define _sm_assert (b )
41
- #define _sm_assert_use (v, b ) v = v;
40
+ #define SM_ASSERT (b )
41
+ #define SM_ASSERT_USE (v, b ) v = v;
42
42
#endif
43
43
44
44
#define SHARING_MAPT (R ) \
@@ -355,7 +355,7 @@ ::iterate(
355
355
{
356
356
const innert *ip = static_cast <const innert *>(bp);
357
357
const to_mapt &m = ip->get_to_map ();
358
- _sm_assert (!m.empty ());
358
+ SM_ASSERT (!m.empty ());
359
359
360
360
for (const auto &item : m)
361
361
{
@@ -365,11 +365,11 @@ ::iterate(
365
365
}
366
366
else // container
367
367
{
368
- _sm_assert (depth == steps);
368
+ SM_ASSERT (depth == steps);
369
369
370
370
const innert *cp = static_cast <const innert *>(bp);
371
371
const leaf_listt &ll = cp->get_container ();
372
- _sm_assert (!ll.empty ());
372
+ SM_ASSERT (!ll.empty ());
373
373
374
374
for (const auto &l : ll)
375
375
{
@@ -391,7 +391,7 @@ ::iterate(
391
391
// / \param[out] view: Empty view
392
392
SHARING_MAPT (void )::get_view(viewt &view) const
393
393
{
394
- _sm_assert (view.empty ());
394
+ SM_ASSERT (view.empty ());
395
395
396
396
if (empty ())
397
397
return ;
@@ -452,7 +452,7 @@ ::get_delta_view(
452
452
delta_viewt &delta_view,
453
453
const bool only_common) const
454
454
{
455
- _sm_assert (delta_view.empty ());
455
+ SM_ASSERT (delta_view.empty ());
456
456
457
457
if (empty ())
458
458
return ;
@@ -509,7 +509,7 @@ ::get_delta_view(
509
509
}
510
510
else // container
511
511
{
512
- _sm_assert (depth == steps);
512
+ SM_ASSERT (depth == steps);
513
513
514
514
const innert *cp1 = static_cast <const innert *>(bp1);
515
515
const innert *cp2 = static_cast <const innert *>(bp2);
@@ -606,8 +606,8 @@ SHARING_MAPT2(const, leaft *)::get_leaf_node(const key_type &k) const
606
606
// / (possible values `unknown` or` true`)
607
607
SHARING_MAPT2 (, size_type)::erase(const key_type &k, const tvt &key_exists)
608
608
{
609
- _sm_assert (!key_exists.is_false ());
610
- _sm_assert (!key_exists.is_true () || has_key (k));
609
+ SM_ASSERT (!key_exists.is_false ());
610
+ SM_ASSERT (!key_exists.is_true () || has_key (k));
611
611
612
612
// check if key exists
613
613
if (key_exists.is_unknown () && !has_key (k))
@@ -651,15 +651,15 @@ SHARING_MAPT2(, size_type)::erase(const key_type &k, const tvt &key_exists)
651
651
}
652
652
else
653
653
{
654
- _sm_assert (del_level == steps - 1 );
654
+ SM_ASSERT (del_level == steps - 1 );
655
655
del->remove_child (del_bit);
656
656
}
657
657
658
658
num--;
659
659
return 1 ;
660
660
}
661
661
662
- _sm_assert (!ll.empty ());
662
+ SM_ASSERT (!ll.empty ());
663
663
664
664
ip->remove_leaf (k);
665
665
num--;
@@ -706,8 +706,8 @@ ::erase_all(const keyst &ks, const tvt &key_exists)
706
706
SHARING_MAPT2 (const , const_find_type)
707
707
::insert(const key_type &k, const mapped_type &m, const tvt &key_exists)
708
708
{
709
- _sm_assert (!key_exists.is_true ());
710
- _sm_assert (!key_exists.is_false () || !has_key (k));
709
+ SM_ASSERT (!key_exists.is_true ());
710
+ SM_ASSERT (!key_exists.is_false () || !has_key (k));
711
711
712
712
if (key_exists.is_unknown ())
713
713
{
@@ -717,7 +717,7 @@ ::insert(const key_type &k, const mapped_type &m, const tvt &key_exists)
717
717
}
718
718
719
719
innert *cp = get_container_node (k);
720
- _sm_assert (cp != nullptr );
720
+ SM_ASSERT (cp != nullptr );
721
721
722
722
const leaft *lp = cp->place_leaf (k, m);
723
723
num++;
@@ -745,7 +745,7 @@ ::insert(const value_type &p, const tvt &key_exists)
745
745
SHARING_MAPT2 (const , find_type)::place(const key_type &k, const mapped_type &m)
746
746
{
747
747
innert *cp = get_container_node (k);
748
- _sm_assert (cp != nullptr );
748
+ SM_ASSERT (cp != nullptr );
749
749
750
750
leaft *lp = cp->find_leaf (k);
751
751
@@ -777,17 +777,17 @@ SHARING_MAPT2(const, find_type)::place(const value_type &p)
777
777
// / boolean indicating if element was found.
778
778
SHARING_MAPT2 (const , find_type)::find(const key_type &k, const tvt &key_exists)
779
779
{
780
- _sm_assert (!key_exists.is_false ());
781
- _sm_assert (!key_exists.is_true () || has_key (k));
780
+ SM_ASSERT (!key_exists.is_false ());
781
+ SM_ASSERT (!key_exists.is_true () || has_key (k));
782
782
783
783
if (key_exists.is_unknown () && !has_key (k))
784
784
return find_type (dummy, false );
785
785
786
786
innert *cp = get_container_node (k);
787
- _sm_assert (cp != nullptr );
787
+ SM_ASSERT (cp != nullptr );
788
788
789
789
leaft *lp = cp->find_leaf (k);
790
- _sm_assert (lp != nullptr );
790
+ SM_ASSERT (lp != nullptr );
791
791
792
792
return find_type (lp->get_value (), true );
793
793
}
0 commit comments