File tree Expand file tree Collapse file tree 3 files changed +5
-25
lines changed
regression/cbmc-incr-oneloop/alarm2 Expand file tree Collapse file tree 3 files changed +5
-25
lines changed Original file line number Diff line number Diff line change 4
4
^EXIT=10$
5
5
^SIGNAL=0$
6
6
"messageText": "VERIFICATION FAILED"
7
- "currentUnwinding ": 1
7
+ "current-unwinding ": "1"
8
8
--
9
9
^warning: ignoring
Original file line number Diff line number Diff line change 1
1
CORE
2
2
main.c
3
3
--incremental-loop main.0 --unwind-min 5 --unwind-max 10
4
- Current unwinding: 1
4
+ current- unwinding: 1
5
5
^EXIT=10$
6
6
^SIGNAL=0$
7
7
^VERIFICATION FAILED$
Original file line number Diff line number Diff line change @@ -137,27 +137,7 @@ bool symex_bmc_incremental_one_loopt::resume(
137
137
}
138
138
void symex_bmc_incremental_one_loopt::log_unwinding (unsigned unwind)
139
139
{
140
- const std::string unwind_num = std::to_string (unwind);
141
- switch (output_ui)
142
- {
143
- case ui_message_handlert::uit::PLAIN:
144
- {
145
- log.statistics () << " Current unwinding: " << unwind_num << messaget::eom;
146
- break ;
147
- }
148
- case ui_message_handlert::uit::XML_UI:
149
- {
150
- xmlt xml (" current-unwinding" );
151
- xml.data = unwind_num;
152
- log.statistics () << xml << messaget::eom;
153
- break ;
154
- }
155
- case ui_message_handlert::uit::JSON_UI:
156
- {
157
- json_objectt json;
158
- json[" currentUnwinding" ] = json_numbert (unwind_num);
159
- log.statistics () << json << messaget::eom;
160
- break ;
161
- }
162
- }
140
+ xmlt data{" current-unwinding" };
141
+ data.data = std::to_string (unwind);
142
+ log.statistics () << data;
163
143
}
You can’t perform that action at this time.
0 commit comments