From 2534b8000c6b537630af30a4ab5485c9b0c98d59 Mon Sep 17 00:00:00 2001 From: Kurt Degiorgio Date: Thu, 15 Jun 2017 12:10:58 +0100 Subject: [PATCH] Handling incomplete traces. Code to instrument 'special' assert at the end of CPROVER_START. This will be used externally in-order to handle incomplete-traces. --- src/goto-instrument/cover.cpp | 27 +++++++++++++++++++++++++++ 1 file changed, 27 insertions(+) diff --git a/src/goto-instrument/cover.cpp b/src/goto-instrument/cover.cpp index a7c37f959ae..a48e6659f9a 100644 --- a/src/goto-instrument/cover.cpp +++ b/src/goto-instrument/cover.cpp @@ -1461,6 +1461,33 @@ bool instrument_cover_goals( cmdline.isset("no-trivial-tests")); } + if(cmdline.isset("cover-traces-must-terminate")) + { + // instrument an additional goal in CPROVER_START. This will rephrase + // the reachability problem by asking BMC to provide a solution that + // satisfies a goal while getting to the end of the program-under-test. + const auto sf_it= + goto_functions.function_map.find(goto_functions.entry_point()); + if(sf_it==goto_functions.function_map.end()) + { + msg.error() << "cover-traces-must-terminate: invalid entry point [" + << goto_functions.entry_point() << "]" + << messaget::eom; + return true; + } + auto if_it=sf_it->second.body.instructions.end(); + while(!if_it->is_function_call()) + if_it--; + if_it++; + const std::string &comment= + "additional goal to ensure complete trace coverage."; + sf_it->second.body.insert_before_swap(if_it); + if_it->make_assertion(false_exprt()); + if_it->source_location.set_comment(comment); + if_it->source_location.set_property_class("reachability_constraint"); + if_it->source_location.set_function(if_it->function); + } + goto_functions.update(); return false; }