From c2b5ee28d87107122e07ef74639fa5ab0eb852c9 Mon Sep 17 00:00:00 2001 From: Polgreen Date: Tue, 3 Jul 2018 12:00:36 +0200 Subject: [PATCH 1/2] Change "violated assumption" to "assumption" in trace Assumptions aren't violated, they are adhered to --- src/goto-programs/goto_trace.cpp | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/src/goto-programs/goto_trace.cpp b/src/goto-programs/goto_trace.cpp index 967b2dbc578..62d21ddf50a 100644 --- a/src/goto-programs/goto_trace.cpp +++ b/src/goto-programs/goto_trace.cpp @@ -524,8 +524,9 @@ void show_full_goto_trace( case goto_trace_stept::typet::ASSUME: if(!step.cond_value) { - out << '\n'; - out << "Violated assumption:" << '\n'; + out << "\n"; + out << "Assumption:\n"; + if(!step.pc->source_location.is_nil()) out << " " << step.pc->source_location << '\n'; From 8c1ffc9f55b1935a976000c6750109ba2e17d599 Mon Sep 17 00:00:00 2001 From: Polgreen Date: Tue, 3 Jul 2018 15:25:20 +0200 Subject: [PATCH 2/2] make assumption output in trace reachable Assumptions are never violated, instead they restrict the search space for non-det values --- regression/cbmc/multiple-goto-traces/test.desc | 2 +- src/goto-programs/goto_trace.cpp | 12 +++--------- 2 files changed, 4 insertions(+), 10 deletions(-) diff --git a/regression/cbmc/multiple-goto-traces/test.desc b/regression/cbmc/multiple-goto-traces/test.desc index 26037ab0f67..f5009b36556 100644 --- a/regression/cbmc/multiple-goto-traces/test.desc +++ b/regression/cbmc/multiple-goto-traces/test.desc @@ -5,7 +5,7 @@ activate-multi-line-match ^EXIT=10$ ^SIGNAL=0$ VERIFICATION FAILED -Trace for main\.assertion\.1:(\n.*){16} assertion 4 \!= argc(\n.*){5}Trace for main\.assertion\.3:(\n.*){30} assertion argc != 4(\n.*){5}Trace for main\.assertion\.4:(\n.*){44} assertion argc \+ 1 != 5 +Trace for main\.assertion\.1:(\n.*){22} assertion 4 \!= argc(\n.*){5}Trace for main\.assertion\.3:(\n.*){36} assertion argc != 4(\n.*){5}Trace for main\.assertion\.4:(\n.*){50} assertion argc \+ 1 != 5 \*\* 3 of 4 failed -- ^warning: ignoring diff --git a/src/goto-programs/goto_trace.cpp b/src/goto-programs/goto_trace.cpp index 62d21ddf50a..81705da4515 100644 --- a/src/goto-programs/goto_trace.cpp +++ b/src/goto-programs/goto_trace.cpp @@ -522,7 +522,7 @@ void show_full_goto_trace( break; case goto_trace_stept::typet::ASSUME: - if(!step.cond_value) + if(step.cond_value && step.pc->is_assume()) { out << "\n"; out << "Assumption:\n"; @@ -530,14 +530,8 @@ void show_full_goto_trace( if(!step.pc->source_location.is_nil()) out << " " << step.pc->source_location << '\n'; - if(step.pc->is_assume()) - { - out << " " - << from_expr(ns, step.function_id, step.pc->get_condition()) - << '\n'; - } - - out << '\n'; + out << " " << from_expr(ns, step.function_id, step.pc->get_condition()) + << '\n'; } break;