diff --git a/regression/cbmc-cover/built-ins1/main.c b/regression/cbmc-cover/built-ins1/main.c new file mode 100644 index 00000000000..2822ea8e7b2 --- /dev/null +++ b/regression/cbmc-cover/built-ins1/main.c @@ -0,0 +1,17 @@ +int main() +{ + char a[10]; + __CPROVER_input("a[3]", a[3]); + + int len = strlen(a); + + if(len==3) + { + return 0; + } + else if(len==4) + { + return -1; + } + return 1; +} diff --git a/regression/cbmc-cover/built-ins1/test.desc b/regression/cbmc-cover/built-ins1/test.desc new file mode 100644 index 00000000000..49b517629f3 --- /dev/null +++ b/regression/cbmc-cover/built-ins1/test.desc @@ -0,0 +1,9 @@ +CORE +main.c +--cover location --unwind 1 +^EXIT=0$ +^SIGNAL=0$ +^\*\* 4 of 7 covered +-- +^warning: ignoring +^\[.* + +int main() +{ + const char *s="test"; + int ret=puts(s); //return value is nondet (internal to built-in, thus non-controllable) + + if(ret<0) + { + return 1; + } + + return 0; +} diff --git a/regression/cbmc-cover/built-ins3/test.desc b/regression/cbmc-cover/built-ins3/test.desc new file mode 100644 index 00000000000..bd3fc9fdaa3 --- /dev/null +++ b/regression/cbmc-cover/built-ins3/test.desc @@ -0,0 +1,9 @@ +CORE +main.c +--cover location --unwind 10 +^EXIT=0$ +^SIGNAL=0$ +^\*\* 4 of 4 covered +-- +^warning: ignoring +^\[.* &atomic_exprs, const exprt &src) @@ -1141,7 +1142,7 @@ void instrument_cover_goals( basic_blocks.source_location_map[block_nr]; if(!source_location.get_file().empty() && - source_location.get_file()[0]!='<') + !source_location.is_built_in()) { std::string comment="block "+b; goto_program.insert_before_swap(i_it); @@ -1179,7 +1180,8 @@ void instrument_cover_goals( t->source_location.set_property_class(property_class); } - if(i_it->is_goto() && !i_it->guard.is_true()) + if(i_it->is_goto() && !i_it->guard.is_true() && + !i_it->source_location.is_built_in()) { std::string b=std::to_string(basic_blocks[i_it]); std::string true_comment= @@ -1214,6 +1216,7 @@ void instrument_cover_goals( i_it->make_skip(); // Conditions are all atomic predicates in the programs. + if(!i_it->source_location.is_built_in()) { const std::set conditions=collect_conditions(i_it); @@ -1250,6 +1253,7 @@ void instrument_cover_goals( i_it->make_skip(); // Decisions are maximal Boolean combinations of conditions. + if(!i_it->source_location.is_built_in()) { const std::set decisions=collect_decisions(i_it); @@ -1290,6 +1294,7 @@ void instrument_cover_goals( // 3. Each condition in a decision takes every possible outcome // 4. Each condition in a decision is shown to independently // affect the outcome of the decision. + if(!i_it->source_location.is_built_in()) { const std::set conditions=collect_conditions(i_it); const std::set decisions=collect_decisions(i_it); @@ -1392,7 +1397,8 @@ void instrument_cover_goals( Forall_goto_functions(f_it, goto_functions) { if(f_it->first==goto_functions.entry_point() || - f_it->first=="__CPROVER_initialize") + f_it->first=="__CPROVER_initialize" || + f_it->second.is_hidden()) continue; instrument_cover_goals(symbol_table, f_it->second.body, criterion);