Skip to content

Commit a097f26

Browse files
committed
switch show_goto_trace to use trace_configurationt
In this commit: - switches goto_trace to use trace_configurationt - rewrites trace_value to avoid passing 4 different members of the same struct goto_trace_stept by reference - moves the code that displays source code into show_state_header - modernises the for loops used in case INPUT and case OUTPUT
1 parent 235bb01 commit a097f26

File tree

4 files changed

+153
-186
lines changed

4 files changed

+153
-186
lines changed

src/cbmc/all_properties.cpp

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -175,9 +175,7 @@ void bmc_all_propertiest::report(const cover_goalst &cover_goals)
175175
if(g.second.status==goalt::statust::FAILURE)
176176
{
177177
result() << "\n" << "Trace for " << g.first << ":" << "\n";
178-
show_goto_trace(result(), bmc.ns, g.second.goto_trace,
179-
bmc.options.get_signed_int_option("trace-verbosity"),
180-
bmc.options.get_bool_option("hex"));
178+
show_goto_trace(result(), bmc.ns, g.second.goto_trace);
181179
}
182180
}
183181
result() << eom;

src/cbmc/bmc.cpp

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -56,9 +56,7 @@ void bmct::error_trace()
5656
{
5757
case ui_message_handlert::uit::PLAIN:
5858
result() << "Counterexample:" << eom;
59-
show_goto_trace(result(), ns, goto_trace,
60-
options.get_signed_int_option("trace-verbosity"),
61-
options.get_bool_option("hex"));
59+
show_goto_trace(result(), ns, goto_trace);
6260
result() << eom;
6361
break;
6462

0 commit comments

Comments
 (0)