CBMC
cover_instrument_condition.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Coverage Instrumentation
4 
5 Author: Daniel Kroening
6 
7 \*******************************************************************/
8 
11 
12 #include "cover_instrument.h"
13 
14 #include <langapi/language_util.h>
15 
16 #include "cover_util.h"
17 
19  const irep_idt &function_id,
20  goto_programt &goto_program,
22  const cover_blocks_baset &,
23  const assertion_factoryt &make_assertion) const
24 {
25  if(is_non_cover_assertion(i_it))
26  i_it->turn_into_skip();
27 
28  // Conditions are all atomic predicates in the programs.
29  if(!i_it->source_location().is_built_in())
30  {
31  const std::set<exprt> conditions = collect_conditions(i_it);
32 
33  source_locationt source_location = i_it->source_location();
34 
35  for(const auto &c : conditions)
36  {
37  const std::string c_string = from_expr(ns, function_id, c);
38 
39  const std::string comment_t = "condition '" + c_string + "' true";
40  goto_program.insert_before_swap(i_it);
41  initialize_source_location(source_location, comment_t, function_id);
42  *i_it = make_assertion(c, source_location);
43 
44  const std::string comment_f = "condition '" + c_string + "' false";
45  goto_program.insert_before_swap(i_it);
46  initialize_source_location(source_location, comment_f, function_id);
47  *i_it = make_assertion(not_exprt(c), source_location);
48  }
49 
50  for(std::size_t i = 0; i < conditions.size() * 2; i++)
51  i_it++;
52  }
53 }
void instrument(const irep_idt &function_id, goto_programt &, goto_programt::targett &, const cover_blocks_baset &, const assertion_factoryt &) const override
Override this method to implement an instrumenter.
bool is_non_cover_assertion(goto_programt::const_targett t) const
void initialize_source_location(source_locationt &source_location, const std::string &comment, const irep_idt &function_id) const
std::function< goto_programt::instructiont(const exprt &, const source_locationt &)> assertion_factoryt
The type of function used to make goto_program assertions.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
Definition: goto_program.h:643
instructionst::iterator targett
Definition: goto_program.h:614
Boolean negation.
Definition: std_expr.h:2327
Coverage Instrumentation.
std::set< exprt > collect_conditions(const exprt &src)
Definition: cover_util.cpp:42
Coverage Instrumentation Utilities.
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)