Skip to content

Commit

Permalink
Make verbose output format for invariants more readable
Browse files Browse the repository at this point in the history
Use separate lines for each set of invariants related to the same
category (e.g., each register).

Signed-off-by: Dave Thaler <[email protected]>
  • Loading branch information
dthaler authored and elazarg committed Oct 23, 2021
1 parent 292f063 commit 73d8f93
Showing 1 changed file with 9 additions and 1 deletion.
10 changes: 9 additions & 1 deletion src/string_constraints.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -127,11 +127,19 @@ std::ostream& operator<<(std::ostream& o, const string_invariant& inv) {
// Intervals
bool first = true;
o << "[";
for (const auto& item : inv.maybe_inv.value()) {
auto& set = inv.maybe_inv.value();
std::string lastbase;
for (const auto& item : set) {
if (first)
first = false;
else
o << ", ";
size_t pos = item.find_first_of(".=[");
std::string base = item.substr(0, pos);
if (base != lastbase) {
o << "\n ";
lastbase = base;
}
o << item;
}
o << "]";
Expand Down

0 comments on commit 73d8f93

Please sign in to comment.