From b27ceb9897dda5cd527e886cd58f70fea586ef0b Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Fri, 24 May 2019 14:26:09 +0100 Subject: [PATCH] Use read() for value_sett::object_mapt equality The explicit definition of object_mapt equality was removed recently in pull request diffblue/cbmc#4694 but it seems necessary when compiling with clang which would complain about it not being defined. Should fix https://github.com/diffblue/cbmc/issues/4699 --- src/pointer-analysis/value_set.h | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/src/pointer-analysis/value_set.h b/src/pointer-analysis/value_set.h index 23af996dab3..8328237a809 100644 --- a/src/pointer-analysis/value_set.h +++ b/src/pointer-analysis/value_set.h @@ -221,10 +221,12 @@ class value_sett bool operator==(const entryt &other) const { - return - identifier==other.identifier && - suffix==other.suffix && - object_map==other.object_map; + // Note that the object_map comparison below is duplicating the code of + // operator== defined in reference_counting.h because old versions of + // clang (3.7 and 3.8) do not resolve the template instantiation correctly + return identifier == other.identifier && suffix == other.suffix && + (object_map.get_d() == other.object_map.get_d() || + object_map.read() == other.object_map.read()); } bool operator!=(const entryt &other) const {