Skip to content

Commit 2d26bc6

Browse files
authored
Merge pull request #237 from diffblue/waveform-width
ebmc: fix for column width in waveform
2 parents 84a0482 + ce2157e commit 2d26bc6

File tree

3 files changed

+11
-8
lines changed

3 files changed

+11
-8
lines changed

regression/ebmc/traces/waveform1.desc

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -5,8 +5,9 @@ waveform1.smv
55
^SIGNAL=0$
66
^\[smv::main::spec1\] .* FAILURE$
77
^Counterexample:$
8-
^ 0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20$
9-
^smv::main::var::x 0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20$
10-
^smv::main::var::y 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0$
8+
^ 0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20$
9+
^smv::main::var::x 0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20$
10+
^smv::main::var::y 0 10 20 30 40 50 60 70 80 90 100 110 120 130 140 150 160 170 180 190 200$
11+
^smv::main::var::z 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0$
1112
--
1213
^warning: ignoring

regression/ebmc/traces/waveform1.smv

Lines changed: 5 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,12 +1,15 @@
11
MODULE main
22

33
VAR x: 0..20;
4-
VAR y: 0..20;
4+
VAR y: 0..200;
5+
VAR z: 0..20;
56

67
INIT x=0
78
INIT y=0
9+
INIT z=0
810

911
ASSIGN next(x):=x + 1;
10-
ASSIGN next(y):=y;
12+
ASSIGN next(y):=y + 10;
13+
ASSIGN next(z):=z;
1114

1215
SPEC AG x!=20

src/ebmc/waveform.cpp

Lines changed: 2 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -97,8 +97,7 @@ void show_waveform(const trans_tracet &trace, const namespacet &ns)
9797
value_map[std::make_pair(identifier, timeframe)] = as_string;
9898
auto &width = column_width[timeframe];
9999
width = std::max(width, as_string.size());
100-
if(width < 2)
101-
width = 2;
100+
width = std::max(width, std::size_t(2));
102101
}
103102
}
104103
}
@@ -141,7 +140,7 @@ void show_waveform(const trans_tracet &trace, const namespacet &ns)
141140
consolet::out() << ' ';
142141
if(consolet::is_terminal() && consolet::use_SGR())
143142
consolet::out() << ((x % 2) ? "\x1b[47m" : "");
144-
consolet::out().width(std::min(std::size_t(2), column_width[x]));
143+
consolet::out().width(column_width[x]);
145144
consolet::out() << value_map[std::make_pair(y, x)];
146145
consolet::out() << consolet::reset;
147146
}

0 commit comments

Comments
 (0)