replica
/
diffblue-cbmc
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

Remove redundant function name from goal descriptions

This commit is contained in:
Peter Schrammel 2017-08-31 17:08:31 +01:00
parent b85624e290
commit bbc99d9bef
2 changed files with 6 additions and 9 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
src/cbmc/bmc_cover.cpp
View File

@ -161,7 +161,8 @@ void bmc_covert::satisfying_assignment()
if(solver.l_get(cond).is_true())
{
status() << "Covered " << g.description << messaget::eom;
status() << "Covered function " << g.source_location.get_function()
<< " " << g.description << messaget::eom;
g.satisfied=true;
test.covered_goals.push_back(goal_pair.first);
break;

12
src/goto-instrument/cover.cpp
View File

@ -1327,8 +1327,7 @@ void instrument_cover_goals(
!source_location.is_built_in() &&
cover_curr_function)
{
std::string comment=
"function "+id2string(i_it->function)+" block "+b;
std::string comment="block "+b;
const irep_idt function=i_it->function;
goto_program.insert_before_swap(i_it);
i_it->make_assertion(false_exprt());
@ -1354,8 +1353,7 @@ void instrument_cover_goals(
{
// we want branch coverage to imply 'entry point of function'
// coverage
std::string comment=
"function "+id2string(i_it->function)+" entry point";
std::string comment="entry point";
source_locationt source_location=i_it->source_location;
@ -1374,10 +1372,8 @@ void instrument_cover_goals(
{
std::string b=
std::to_string(basic_blocks.block_of(i_it)+1); // start with 1
std::string true_comment=
"function "+id2string(i_it->function)+" block "+b+" branch true";
std::string false_comment=
"function "+id2string(i_it->function)+" block "+b+" branch false";
std::string true_comment="block "+b+" branch true";
std::string false_comment="block "+b+" branch false";
exprt guard=i_it->guard;
const irep_idt function=i_it->function;