Skip to content

Commit e27070a

Browse files
committed
std::sort requires strict weak ordering
Two of our uses of `std::sort` failed to satisfy the "strict" part of "strict weak ordering." This resulted in iterators running out of bounds with LLVM's libc++. Fixes: #7949
1 parent a997e32 commit e27070a

File tree

2 files changed

+9
-3
lines changed

2 files changed

+9
-3
lines changed

Diff for: src/analyses/variable-sensitivity/value_set_abstract_object.cpp

+8-2
Original file line numberDiff line numberDiff line change
@@ -493,6 +493,7 @@ static abstract_object_sett compact_values(const abstract_object_sett &values)
493493
static exprt eval_expr(const exprt &e);
494494
static bool is_eq(const exprt &lhs, const exprt &rhs);
495495
static bool is_le(const exprt &lhs, const exprt &rhs);
496+
static bool is_lt(const exprt &lhs, const exprt &rhs);
496497
static abstract_object_sett collapse_values_in_intervals(
497498
const abstract_object_sett &values,
498499
const std::vector<constant_interval_exprt> &intervals);
@@ -525,8 +526,8 @@ void collapse_overlapping_intervals(
525526
intervals.end(),
526527
[](constant_interval_exprt const &lhs, constant_interval_exprt const &rhs) {
527528
if(is_eq(lhs.get_lower(), rhs.get_lower()))
528-
return is_le(lhs.get_upper(), rhs.get_upper());
529-
return is_le(lhs.get_lower(), rhs.get_lower());
529+
return is_lt(lhs.get_upper(), rhs.get_upper());
530+
return is_lt(lhs.get_lower(), rhs.get_lower());
530531
});
531532

532533
size_t index = 1;
@@ -646,6 +647,11 @@ static bool is_le(const exprt &lhs, const exprt &rhs)
646647
return constant_interval_exprt::less_than_or_equal(lhs, rhs);
647648
}
648649

650+
static bool is_lt(const exprt &lhs, const exprt &rhs)
651+
{
652+
return constant_interval_exprt::less_than(lhs, rhs);
653+
}
654+
649655
static abstract_object_sett widen_value_set(
650656
const abstract_object_sett &values,
651657
const constant_interval_exprt &lhs,

Diff for: src/cprover/generalization.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -45,7 +45,7 @@ class frequency_mapt
4545
result.begin(),
4646
result.end(),
4747
[](counterst::const_iterator a, counterst::const_iterator b) -> bool {
48-
return a->second >= b->second;
48+
return a->second > b->second;
4949
});
5050
return result;
5151
}

0 commit comments

Comments
 (0)