Skip to content

Commit 701c331

Browse files
author
Daniel Kroening
committed
further work on --cover
1 parent 7d4e004 commit 701c331

File tree

11 files changed

+74
-58
lines changed

11 files changed

+74
-58
lines changed

‎regression/cbmc-cover/assertion1/main.c

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
int main()
2+
{
3+
int input1, input2;
4+
5+
__CPROVER_assert(!input1, "");
6+
7+
if(input1)
8+
{
9+
__CPROVER_assert(!input1, ""); // will work, we ignore the assertion
10+
}
11+
}

‎regression/cbmc-cover/assertion1/test.desc

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
CORE
2+
main.c
3+
--cover assertion
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^\[main.assertion.1\] file main.c line 5 function main: SATISFIED$
7+
^\[main.assertion.2\] file main.c line 9 function main: SATISFIED$
8+
--
9+
^warning: ignoring

‎regression/cbmc-cover/cover1/main.c

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
int main()
2+
{
3+
int input1, input2;
4+
5+
__CPROVER_cover(input1);
6+
__CPROVER_cover(!input1);
7+
8+
if(input1)
9+
{
10+
__CPROVER_cover(!input1); // won't work
11+
}
12+
}

‎regression/cbmc-cover/cover1/test.desc

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
CORE
2+
main.c
3+
--cover cover
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^\[main.1] file main.c line 5 function main condition .*: SATISFIED$
7+
^\[main.2] file main.c line 6 function main condition .*: SATISFIED$
8+
^\[main.3] file main.c line 10 function main condition .*: FAILED$
9+
--
10+
^warning: ignoring

‎src/cbmc/bmc_cover.cpp

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -385,7 +385,8 @@ bool bmc_covert::operator()()
385385
status() << "** " << goals_covered
386386
<< " of " << goal_map.size() << " covered ("
387387
<< std::fixed << std::setw(1) << std::setprecision(1)
388-
<< 100.0*goals_covered/goal_map.size() << "%), using "
388+
<< (goal_map.empty()?0.0:100.0*goals_covered/goal_map.size())
389+
<< "%), using "
389390
<< cover_goals.iterations() << " iteration"
390391
<< (cover_goals.iterations()==1?"":"s")
391392
<< eom;

‎src/cbmc/cbmc_parse_options.cpp

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -937,10 +937,12 @@ bool cbmc_parse_optionst::process_goto_program(
937937
c=coverage_criteriont::CONDITION;
938938
else if(criterion=="mcdc")
939939
c=coverage_criteriont::MCDC;
940+
else if(criterion=="cover")
941+
c=coverage_criteriont::COVER;
940942
else
941943
{
942944
error() << "unknown coverage criterion" << eom;
943-
return false;
945+
return true;
944946
}
945947

946948
status() << "Instrumenting coverge goals" << eom;

‎src/goto-instrument/cover.cpp

Lines changed: 24 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -73,6 +73,7 @@ const char *as_string(coverage_criteriont c)
7373
case coverage_criteriont::PATH: return "path";
7474
case coverage_criteriont::MCDC: return "MC/DC";
7575
case coverage_criteriont::ASSERTION: return "assertion";
76+
case coverage_criteriont::COVER: return "cover instructions";
7677
default: return "";
7778
}
7879
}
@@ -285,7 +286,29 @@ void instrument_cover_goals(
285286
{
286287
case coverage_criteriont::ASSERTION:
287288
// turn into 'assert(false)' to avoid simplification
288-
i_it->guard=false_exprt();
289+
if(i_it->is_assert())
290+
i_it->guard=false_exprt();
291+
break;
292+
293+
case coverage_criteriont::COVER:
294+
// turn __CPROVER_cover(x) into 'assert(!x)'
295+
if(i_it->is_function_call())
296+
{
297+
const code_function_callt &code_function_call=
298+
to_code_function_call(i_it->code);
299+
if(code_function_call.function().id()==ID_symbol &&
300+
to_symbol_expr(code_function_call.function()).get_identifier()==
301+
"__CPROVER_cover" &&
302+
code_function_call.arguments().size()==1)
303+
{
304+
const exprt c=code_function_call.arguments()[0];
305+
std::string comment="condition `"+from_expr(ns, "", c)+"'";
306+
i_it->guard=not_exprt(c);
307+
i_it->type=ASSERT;
308+
i_it->code.clear();
309+
i_it->source_location.set_comment(comment);
310+
}
311+
}
289312
break;
290313

291314
case coverage_criteriont::LOCATION:

‎src/goto-instrument/cover.h

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -15,7 +15,7 @@ Date: May 2016
1515

1616
enum class coverage_criteriont {
1717
LOCATION, BRANCH, DECISION, CONDITION,
18-
PATH, MCDC, ASSERTION };
18+
PATH, MCDC, ASSERTION, COVER };
1919

2020
void instrument_cover_goals(
2121
const symbol_tablet &symbol_table,

‎src/goto-programs/builtin_functions.cpp

Lines changed: 0 additions & 52 deletions
Original file line numberDiff line numberDiff line change
@@ -270,53 +270,6 @@ void goto_convertt::do_input(
270270

271271
/*******************************************************************\
272272
273-
Function: goto_convertt::do_cover
274-
275-
Inputs:
276-
277-
Outputs:
278-
279-
Purpose:
280-
281-
\*******************************************************************/
282-
283-
void goto_convertt::do_cover(
284-
const exprt &lhs,
285-
const exprt &function,
286-
const exprt::operandst &arguments,
287-
goto_programt &dest)
288-
{
289-
codet output_code;
290-
output_code.set_statement(ID_output);
291-
output_code.add_source_location()=function.source_location();
292-
293-
if(arguments.size()!=1)
294-
{
295-
err_location(function);
296-
throw "cover takes one argument";
297-
}
298-
299-
// build string constant
300-
exprt string_constant(ID_string_constant);
301-
string_constant.type()=array_typet();
302-
string_constant.type().subtype()=char_type();
303-
string_constant.set(ID_value, ID_cover);
304-
305-
index_exprt index_expr;
306-
index_expr.type()=char_type();
307-
index_expr.array()=string_constant;
308-
index_expr.index()=gen_zero(index_type());
309-
310-
output_code.copy_to_operands(address_of_exprt(index_expr));
311-
312-
forall_expr(it, arguments)
313-
output_code.copy_to_operands(*it);
314-
315-
copy(output_code, OTHER, dest);
316-
}
317-
318-
/*******************************************************************\
319-
320273
Function: goto_convertt::do_output
321274
322275
Inputs:
@@ -1154,11 +1107,6 @@ void goto_convertt::do_function_call_symbol(
11541107
{
11551108
do_input(lhs, function, arguments, dest);
11561109
}
1157-
else if(identifier==CPROVER_PREFIX "cover" ||
1158-
identifier=="__CPROVER::cover")
1159-
{
1160-
do_cover(lhs, function, arguments, dest);
1161-
}
11621110
else if(identifier==CPROVER_PREFIX "output" ||
11631111
identifier=="__CPROVER::output")
11641112
{

‎src/goto-programs/goto_convert_class.h

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -466,7 +466,6 @@ class goto_convertt:public message_streamt
466466
void do_printf (const exprt &lhs, const exprt &rhs, const exprt::operandst &arguments, goto_programt &dest);
467467
void do_input (const exprt &lhs, const exprt &rhs, const exprt::operandst &arguments, goto_programt &dest);
468468
void do_output (const exprt &lhs, const exprt &rhs, const exprt::operandst &arguments, goto_programt &dest);
469-
void do_cover (const exprt &lhs, const exprt &rhs, const exprt::operandst &arguments, goto_programt &dest);
470469
void do_prob_coin (const exprt &lhs, const exprt &rhs, const exprt::operandst &arguments, goto_programt &dest);
471470
void do_prob_uniform (const exprt &lhs, const exprt &rhs, const exprt::operandst &arguments, goto_programt &dest);
472471

‎src/goto-programs/goto_inline.cpp

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -414,7 +414,8 @@ void goto_inlinet::expand_function_call(
414414
identifier=="__CPROVER_set_must" ||
415415
identifier=="__CPROVER_set_may" ||
416416
identifier=="__CPROVER_clear_must" ||
417-
identifier=="__CPROVER_clear_may")
417+
identifier=="__CPROVER_clear_may" ||
418+
identifier=="__CPROVER_cover")
418419
{
419420
target++;
420421
return; // ignore

0 commit comments

Comments
 (0)