Go to the documentation of this file.
22 if(instruction->incoming_edges.size() != 1)
26 if(in_t->is_goto() && !in_t->is_backwards_goto() && in_t->guard.is_true())
34 bool next_is_target =
true;
35 std::size_t current_block = 0;
40 if(next_is_target || it->is_target())
44 current_block = *block_number;
56 current_block <
block_infos.size(),
"current block number out of range");
65 !it->source_location.is_nil() &&
66 !it->source_location.get_file().empty() &&
67 !it->source_location.get_line().empty() &&
77 it->is_goto() || it->is_function_call() || it->is_assume();
79 it->is_goto() || it->is_function_call();
117 std::set<std::size_t> blocks_seen;
120 const std::size_t block_nr =
block_of(it);
124 blocks_seen.insert(block_nr).second &&
127 msg.
warning() <<
"Ignoring block " << (block_nr + 1) <<
" location "
129 <<
" (bytecode-index already instrumented)"
136 msg.
warning() <<
"Ignoring block " << (block_nr + 1) <<
" location "
137 << it->location_number <<
" " << function_id
148 out << block_pair.first->source_location <<
" -> " << block_pair.second
157 const irep_idt &line = location.get_line();
174 const auto &cover_set = block_info.
lines;
175 INVARIANT(!cover_set.empty(),
"covered lines set must not be empty");
176 std::vector<unsigned> line_list(cover_set.begin(), cover_set.end());
188 std::string str = source_lines.
to_string();
189 INVARIANT(!str.empty(),
"source lines set must not be empty");
196 std::set<std::size_t> source_lines_requiring_update;
200 const auto &location = it->source_location;
201 const auto &bytecode_index = location.get_java_bytecode_index();
207 block_locations.back().set_basic_block_covered_lines(location.get_line());
209 source_lines_requiring_update.insert(entry.first->second);
214 source_lines_requiring_update.insert(entry.first->second);
218 for(std::size_t i : source_lines_requiring_update)
228 const auto &bytecode_index = t->source_location.get_java_bytecode_index();
Class that provides messages with a built-in verbosity 'level'.
optionalt< goto_programt::const_targett > instruction_of(std::size_t block_nr) const override
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
std::unordered_map< irep_idt, std::size_t > index_to_block
source_locationt source_location
The location of the instruction in the source file.
static void add_block_lines(cover_basic_blockst::block_infot &block, const goto_programt::instructiont &instruction)
Adds the lines which.
cover_basic_blocks_javat(const goto_programt &_goto_program)
static const source_locationt & nil()
source_locationt source_location
the source location representative for this block (we need a separate copy of source locations becaus...
std::vector< source_linest > block_source_lines
Base class for all expressions.
void set_basic_block_source_lines(const irep_idt &source_lines)
void report_block_anomalies(const irep_idt &function_id, const goto_programt &goto_program, message_handlert &message_handler) override
Output warnings about ignored blocks.
std::string to_string() const
Construct a string representing the set of lines.
source_linest source_lines
the set of source code lines belonging to this block
std::size_t block_of(goto_programt::const_targett t) const override
void insert(const source_locationt &loc)
Insert a line (a source location) into the set of lines.
block_mapt block_map
map program locations to block numbers
const std::string & id2string(const irep_idt &d)
codet code
Do not read or modify directly – use get_X() instead.
source_locationt source_location
static optionalt< std::size_t > continuation_of_block(const goto_programt::const_targett &instruction, block_mapt &block_map)
If this block is a continuation of a previous block through unconditional forward gotos,...
std::vector< block_infot > block_infos
map block numbers to block information
#define PRECONDITION(CONDITION)
const source_locationt & source_location_of(std::size_t block_nr) const override
std::size_t block_of(goto_programt::const_targett t) const override
static void update_source_lines(block_infot &block_info)
create a string representing source lines and set as a property of source location of basic block
std::vector< source_locationt > block_locations
std::vector< goto_programt::const_targett > block_infos
nonstd::optional< T > optionalt
instructionst instructions
The list of instructions in the goto program.
const source_locationt & source_location_of(std::size_t block_number) const override
optionalt< goto_programt::const_targett > instruction_of(std::size_t block_number) const override
std::map< goto_programt::const_targett, std::size_t > block_mapt
std::unordered_set< std::size_t > lines
the set of lines belonging to this block
void output(std::ostream &out) const override
Outputs the list of blocks.
unsigned unsafe_string2unsigned(const std::string &str, int base)
void output(std::ostream &out) const override
Outputs the list of blocks.
void visit_pre(std::function< void(exprt &)>)
Basic blocks detection for Coverage Instrumentation.
A generic container class for the GOTO intermediate representation of one function.
instructionst::const_iterator const_targett
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
void set_basic_block_covered_lines(const irep_idt &covered_lines)
mstreamt & warning() const
This class represents an instruction in the GOTO intermediate representation.
const source_locationt & source_location() const
static void update_covered_lines(block_infot &block_info)
create list of covered lines as CSV string and set as property of source location of basic block,...
optionalt< goto_programt::const_targett > representative_inst
the program location to instrument for this block
instructionst::iterator targett
#define forall_goto_program_instructions(it, program)
cover_basic_blockst(const goto_programt &goto_program)