Skip to content

Commit 8de0ea3

Browse files
committed
Fix iterator equality check bug in ai.h
1 parent 6297085 commit 8de0ea3

File tree

2 files changed

+14
-1
lines changed

2 files changed

+14
-1
lines changed

src/analyses/ai.h

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -409,7 +409,9 @@ class ait:public ai_baset
409409
}
410410

411411
protected:
412-
typedef std::unordered_map<locationt, domainT, const_target_hash> state_mapt;
412+
typedef std::
413+
unordered_map<locationt, domainT, const_target_hash, pointee_address_equalt>
414+
state_mapt;
413415
state_mapt state_map;
414416

415417
// this one creates states, if need be

src/goto-programs/goto_program_template.h

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -810,4 +810,15 @@ struct const_target_hash_templatet
810810
{ return t->location_number; }
811811
};
812812

813+
/// Functor to check whether iterators from different collections point at the
814+
/// same object.
815+
struct pointee_address_equalt
816+
{
817+
template <class A, class B>
818+
bool operator()(const A &a, const B &b) const
819+
{
820+
return &(*a) == &(*b);
821+
}
822+
};
823+
813824
#endif // CPROVER_GOTO_PROGRAMS_GOTO_PROGRAM_TEMPLATE_H

0 commit comments

Comments
 (0)