From 22941f450bea7471ed03a7aff4bebfe3f764c2ea Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sun, 30 Nov 2025 13:14:15 +0000 Subject: [PATCH] Refactor basic block detection into standalone utility module This PR refactors the basic block detection functionality from the coverage goal instrumenter into a standalone utility module in the `src/analyses/` directory. The new utility provides a generic, reusable interface for basic block detection across different parts of the codebase, similar to how `natural_loops_templatet` handles loop detection. Fixes: #1686 --- src/analyses/basic_blocks.h | 267 +++++++++++++++++++++ src/analyses/basic_blocks_impl.h | 199 +++++++++++++++ src/goto-instrument/cover_basic_blocks.cpp | 172 +++++-------- src/goto-instrument/cover_basic_blocks.h | 71 +++--- 4 files changed, 562 insertions(+), 147 deletions(-) create mode 100644 src/analyses/basic_blocks.h create mode 100644 src/analyses/basic_blocks_impl.h diff --git a/src/analyses/basic_blocks.h b/src/analyses/basic_blocks.h new file mode 100644 index 00000000000..167691671ca --- /dev/null +++ b/src/analyses/basic_blocks.h @@ -0,0 +1,267 @@ +/*******************************************************************\ + +Module: Basic Blocks Detection for Goto Programs + +Author: Refactored from cover_basic_blocks.h + +\*******************************************************************/ + +/// \file +/// Generic basic block detection for goto programs +/// +/// This module provides a generic basic block detection utility that can +/// be used across different parts of the codebase. It supports pluggable +/// strategies for language-specific behavior and configurable options for +/// how basic blocks are detected (e.g., whether assume statements delimit +/// blocks). + +#ifndef CPROVER_ANALYSES_BASIC_BLOCKS_H +#define CPROVER_ANALYSES_BASIC_BLOCKS_H + +#include + +#include + +#include +#include +#include +#include +#include + +class source_locationt; + +/// Configuration options for basic block detection +struct basic_block_configt +{ + /// If true, assume statements delimit basic blocks + /// (i.e., assumptions terminate blocks as subsequent instructions may be + /// unreachable). However, multiple consecutive assumes with the same source + /// location are treated as part of the same block. + bool assume_delimit_blocks = true; + + basic_block_configt() = default; + explicit basic_block_configt(bool _assume_delimit_blocks) + : assume_delimit_blocks(_assume_delimit_blocks) + { + } +}; + +/// Abstract policy interface for language-specific basic block detection +/// behavior. This enables different detection strategies for different +/// languages (e.g., Java bytecode uses java_bytecode_index for blocks) +template +class basic_block_policy_baset +{ +public: + virtual ~basic_block_policy_baset() = default; + + /// Information about a basic block + struct block_infot + { + /// Program location representative of this block (for instrumentation) + std::optional representative_inst; + /// Source location representative of this block + source_locationt source_location; + /// Additional policy-specific data can be stored in derived classes + }; + + /// Compute basic blocks for the given program + /// \param program: The goto program to analyze + /// \param config: Configuration options for block detection + virtual void + compute_blocks(const P &program, const basic_block_configt &config) = 0; + + /// Get the block number for a given instruction + /// \param t: An instruction in the program + /// \return The block number containing this instruction + virtual std::size_t block_of(T t) const = 0; + + /// Get the representative instruction for a block + /// \param block_nr: Block number + /// \return The representative instruction, or empty if none + virtual std::optional instruction_of(std::size_t block_nr) const = 0; + + /// Get the source location for a block + /// \param block_nr: Block number + /// \return Reference to the source location + virtual const source_locationt & + source_location_of(std::size_t block_nr) const = 0; + + /// Get the number of blocks detected + virtual std::size_t size() const = 0; +}; + +/// Default basic block detection policy for C/C++ +/// This implements standard control-flow-based basic block detection +template +class default_basic_block_policyt : public basic_block_policy_baset +{ +public: + using block_infot = typename basic_block_policy_baset::block_infot; + + void + compute_blocks(const P &program, const basic_block_configt &config) override; + std::size_t block_of(T t) const override; + std::optional instruction_of(std::size_t block_nr) const override; + const source_locationt & + source_location_of(std::size_t block_nr) const override; + std::size_t size() const override + { + return block_infos.size(); + } + +protected: + using block_mapt = std::map; + + /// Map program locations to block numbers + block_mapt block_map; + /// Information about each block + std::vector block_infos; + + /// Check if instruction is a continuation of a previous block through + /// unconditional forward gotos + static std::optional + continuation_of_block(T instruction, block_mapt &block_map); +}; + +/// Java-specific basic block detection policy +/// Uses Java bytecode index to determine blocks +template +class java_basic_block_policyt : public basic_block_policy_baset +{ +public: + using block_infot = typename basic_block_policy_baset::block_infot; + + void + compute_blocks(const P &program, const basic_block_configt &config) override; + std::size_t block_of(T t) const override; + std::optional instruction_of(std::size_t block_nr) const override; + const source_locationt & + source_location_of(std::size_t block_nr) const override; + std::size_t size() const override + { + return block_infos.size(); + } + +protected: + /// Information about each block (indexed by block number) + std::vector block_infos; + /// Map Java bytecode index to block number + std::unordered_map index_to_block; +}; + +/// Main template for basic block detection +/// Similar to natural_loops_templatet, this provides a generic interface +/// for detecting basic blocks in goto programs with pluggable policies. +/// +/// \tparam P: Program type (e.g., goto_programt) +/// \tparam T: Iterator type (e.g., goto_programt::const_targett) +/// \tparam C: Comparison functor for iterators +template +class basic_blocks_templatet +{ +public: + /// Create a basic block detector with default policy + basic_blocks_templatet() + : policy(std::make_unique>()), config() + { + } + + /// Create with a specific configuration + explicit basic_blocks_templatet(const basic_block_configt &_config) + : policy(std::make_unique>()), + config(_config) + { + } + + /// Create with a custom policy + explicit basic_blocks_templatet( + std::unique_ptr> _policy) + : policy(std::move(_policy)), config() + { + } + + /// Create with custom policy and configuration + basic_blocks_templatet( + std::unique_ptr> _policy, + const basic_block_configt &_config) + : policy(std::move(_policy)), config(_config) + { + } + + /// Compute basic blocks for a program + /// \param program: The goto program to analyze + void operator()(const P &program) + { + compute(program); + } + + /// Compute basic blocks for a program + /// \param program: The goto program to analyze + void compute(const P &program) + { + PRECONDITION(policy); + policy->compute_blocks(program, config); + } + + /// Get the block number for a given instruction + std::size_t block_of(T t) const + { + PRECONDITION(policy); + return policy->block_of(t); + } + + /// Get the representative instruction for a block + std::optional instruction_of(std::size_t block_nr) const + { + PRECONDITION(policy); + return policy->instruction_of(block_nr); + } + + /// Get the source location for a block + const source_locationt &source_location_of(std::size_t block_nr) const + { + PRECONDITION(policy); + return policy->source_location_of(block_nr); + } + + /// Get the number of blocks detected + std::size_t size() const + { + PRECONDITION(policy); + return policy->size(); + } + + /// Get the configuration + const basic_block_configt &get_config() const + { + return config; + } + + /// Set the configuration + void set_config(const basic_block_configt &_config) + { + config = _config; + } + +protected: + std::unique_ptr> policy; + basic_block_configt config; +}; + +/// Concrete type for basic block detection on const goto programs +using basic_blockst = basic_blocks_templatet< + const goto_programt, + goto_programt::const_targett, + goto_programt::target_less_than>; + +/// Concrete type for basic block detection on mutable goto programs +using basic_blocks_mutablet = basic_blocks_templatet< + goto_programt, + goto_programt::targett, + goto_programt::target_less_than>; + +// Include template implementations +#include "basic_blocks_impl.h" + +#endif // CPROVER_ANALYSES_BASIC_BLOCKS_H diff --git a/src/analyses/basic_blocks_impl.h b/src/analyses/basic_blocks_impl.h new file mode 100644 index 00000000000..78ef2b3a420 --- /dev/null +++ b/src/analyses/basic_blocks_impl.h @@ -0,0 +1,199 @@ +/*******************************************************************\ + +Module: Basic Blocks Detection - Template Implementations + +Author: Refactored from cover_basic_blocks.cpp + +\*******************************************************************/ + +/// \file +/// Template implementations for basic block detection + +#ifndef CPROVER_ANALYSES_BASIC_BLOCKS_IMPL_H +#define CPROVER_ANALYSES_BASIC_BLOCKS_IMPL_H + +#include +#include + +/// Check if two source locations are on the same source line +static inline bool +same_source_line(const source_locationt &a, const source_locationt &b) +{ + return a.get_file() == b.get_file() && a.get_line() == b.get_line(); +} + +// ============================================================================ +// Default basic block policy implementation +// ============================================================================ + +template +std::optional +default_basic_block_policyt::continuation_of_block( + T instruction, + block_mapt &block_map) +{ + if(instruction->incoming_edges.size() != 1) + return {}; + + const auto in_t = *instruction->incoming_edges.cbegin(); + if( + in_t->is_goto() && !in_t->is_backwards_goto() && + in_t->condition().is_true()) + return block_map[in_t]; + + return {}; +} + +template +void default_basic_block_policyt::compute_blocks( + const P &program, + const basic_block_configt &config) +{ + block_map.clear(); + block_infos.clear(); + + bool next_is_target = true; + const typename P::instructiont *preceding_assume = nullptr; + std::size_t current_block = 0; + + forall_goto_program_instructions(it, program) + { + // For the purposes of coverage blocks, multiple consecutive assume + // instructions with the same source location are considered to be part of + // the same block. Assumptions should terminate a block (if configured), + // as subsequent instructions may be unreachable. However check + // instrumentation passes may insert multiple assertions in the same + // program location. Therefore these are combined for reasons of + // readability of the coverage output. + bool end_of_assume_group = false; + if(config.assume_delimit_blocks) + { + end_of_assume_group = + preceding_assume && + !(it->is_assume() && + same_source_line( + preceding_assume->source_location(), it->source_location())); + } + + // Is it a potential beginning of a block? + if(next_is_target || it->is_target() || end_of_assume_group) + { + if(auto block_number = continuation_of_block(it, block_map)) + { + current_block = *block_number; + } + else + { + block_infos.emplace_back(); + block_infos.back().representative_inst = it; + block_infos.back().source_location = source_locationt::nil(); + current_block = block_infos.size() - 1; + } + } + + INVARIANT( + current_block < block_infos.size(), "current block number out of range"); + block_infot &block_info = block_infos.at(current_block); + + block_map[it] = current_block; + + // Set representative program location to instrument + if( + !it->source_location().is_nil() && + !it->source_location().get_file().empty() && + !it->source_location().get_line().empty() && + !it->source_location().is_built_in() && + block_info.source_location.is_nil()) + { + block_info.representative_inst = it; // update + block_info.source_location = it->source_location(); + } + + next_is_target = it->is_goto() || it->is_function_call(); + + if(config.assume_delimit_blocks) + preceding_assume = it->is_assume() ? &*it : nullptr; + } +} + +template +std::size_t default_basic_block_policyt::block_of(T t) const +{ + const auto it = block_map.find(t); + INVARIANT(it != block_map.end(), "instruction must be part of a block"); + return it->second; +} + +template +std::optional default_basic_block_policyt::instruction_of( + const std::size_t block_nr) const +{ + INVARIANT(block_nr < block_infos.size(), "block number out of range"); + return block_infos[block_nr].representative_inst; +} + +template +const source_locationt & +default_basic_block_policyt::source_location_of( + const std::size_t block_nr) const +{ + INVARIANT(block_nr < block_infos.size(), "block number out of range"); + return block_infos[block_nr].source_location; +} + +// ============================================================================ +// Java basic block policy implementation +// ============================================================================ + +template +void java_basic_block_policyt::compute_blocks( + const P &program, + const basic_block_configt &config) +{ + // Note: config is not used for Java blocks as they're determined by bytecode + // index + (void)config; + + block_infos.clear(); + index_to_block.clear(); + + forall_goto_program_instructions(it, program) + { + const auto &location = it->source_location(); + const auto &bytecode_index = location.get_java_bytecode_index(); + auto entry = index_to_block.emplace(bytecode_index, block_infos.size()); + if(entry.second) + { + block_infos.emplace_back(); + block_infos.back().representative_inst = it; + block_infos.back().source_location = location; + } + } +} + +template +std::size_t java_basic_block_policyt::block_of(T t) const +{ + const auto &bytecode_index = t->source_location().get_java_bytecode_index(); + const auto it = index_to_block.find(bytecode_index); + INVARIANT(it != index_to_block.end(), "instruction must be part of a block"); + return it->second; +} + +template +std::optional java_basic_block_policyt::instruction_of( + const std::size_t block_nr) const +{ + PRECONDITION(block_nr < block_infos.size()); + return block_infos[block_nr].representative_inst; +} + +template +const source_locationt &java_basic_block_policyt::source_location_of( + const std::size_t block_nr) const +{ + PRECONDITION(block_nr < block_infos.size()); + return block_infos[block_nr].source_location; +} + +#endif // CPROVER_ANALYSES_BASIC_BLOCKS_IMPL_H diff --git a/src/goto-instrument/cover_basic_blocks.cpp b/src/goto-instrument/cover_basic_blocks.cpp index 23df805b4dc..8bd03f77306 100644 --- a/src/goto-instrument/cover_basic_blocks.cpp +++ b/src/goto-instrument/cover_basic_blocks.cpp @@ -8,111 +8,55 @@ Author: Peter Schrammel /// \file /// Basic blocks detection for Coverage Instrumentation +/// This file adapts the generic basic block detection utility from +/// src/analyses/basic_blocks.h for use in coverage instrumentation. #include "cover_basic_blocks.h" #include -std::optional cover_basic_blockst::continuation_of_block( - const goto_programt::const_targett &instruction, - cover_basic_blockst::block_mapt &block_map) -{ - if(instruction->incoming_edges.size() != 1) - return {}; - - const goto_programt::targett in_t = *instruction->incoming_edges.cbegin(); - if(in_t->is_goto() && !in_t->is_backwards_goto() && in_t->condition() == true) - return block_map[in_t]; +#include - return {}; -} +// ============================================================================ +// cover_basic_blockst implementation (default C/C++ behavior) +// ============================================================================ -static bool -same_source_line(const source_locationt &a, const source_locationt &b) +cover_basic_blockst::cover_basic_blockst( + const goto_programt &goto_program, + const basic_block_configt &config) + : blocks() { - return a.get_file() == b.get_file() && a.get_line() == b.get_line(); -} + // Compute basic blocks using the generic utility + blocks.set_config(config); + blocks.compute(goto_program); -cover_basic_blockst::cover_basic_blockst(const goto_programt &goto_program) -{ - bool next_is_target = true; - const goto_programt::instructiont *preceding_assume = nullptr; - std::size_t current_block = 0; + // Initialize extended information for each block (source lines) + block_infos.resize(blocks.size()); + // Collect source lines for each instruction forall_goto_program_instructions(it, goto_program) { - // For the purposes of coverage blocks, multiple consecutive assume - // instructions with the same source location are considered to be part of - // the same block. Assumptions should terminate a block, as subsequent - // instructions may be unreachable. However check instrumentation passes - // may insert multiple assertions in the same program location. Therefore - // these are combined for reasons of readability of the coverage output. - bool end_of_assume_group = - preceding_assume && - !(it->is_assume() && - same_source_line( - preceding_assume->source_location(), it->source_location())); - - // Is it a potential beginning of a block? - if(next_is_target || it->is_target() || end_of_assume_group) - { - if(auto block_number = continuation_of_block(it, block_map)) - { - current_block = *block_number; - } - else - { - block_infos.emplace_back(); - block_infos.back().representative_inst = it; - block_infos.back().source_location = source_locationt::nil(); - current_block = block_infos.size() - 1; - } - } - - INVARIANT( - current_block < block_infos.size(), "current block number out of range"); - block_infot &block_info = block_infos.at(current_block); - - block_map[it] = current_block; - - add_block_lines(block_info, *it); - - // set representative program location to instrument - if( - !it->source_location().is_nil() && - !it->source_location().get_file().empty() && - !it->source_location().get_line().empty() && - !it->source_location().is_built_in() && - block_info.source_location.is_nil()) - { - block_info.representative_inst = it; // update - block_info.source_location = it->source_location(); - } - - next_is_target = it->is_goto() || it->is_function_call(); - preceding_assume = it->is_assume() ? &*it : nullptr; + const std::size_t block_nr = blocks.block_of(it); + INVARIANT(block_nr < block_infos.size(), "block number out of range"); + add_block_lines(block_infos[block_nr], *it); } } std::size_t cover_basic_blockst::block_of(goto_programt::const_targett t) const { - const auto it = block_map.find(t); - INVARIANT(it != block_map.end(), "instruction must be part of a block"); - return it->second; + return blocks.block_of(t); } std::optional cover_basic_blockst::instruction_of(const std::size_t block_nr) const { - INVARIANT(block_nr < block_infos.size(), "block number out of range"); - return block_infos[block_nr].representative_inst; + return blocks.instruction_of(block_nr); } const source_locationt & cover_basic_blockst::source_location_of(const std::size_t block_nr) const { - INVARIANT(block_nr < block_infos.size(), "block number out of range"); - return block_infos[block_nr].source_location; + return blocks.source_location_of(block_nr); } const source_linest & @@ -131,21 +75,20 @@ void cover_basic_blockst::report_block_anomalies( std::set blocks_seen; forall_goto_program_instructions(it, goto_program) { - const std::size_t block_nr = block_of(it); - const block_infot &block_info = block_infos.at(block_nr); + const std::size_t block_nr = blocks.block_of(it); + const auto representative_inst = blocks.instruction_of(block_nr); + const auto &source_location = blocks.source_location_of(block_nr); if( blocks_seen.insert(block_nr).second && - block_info.representative_inst == goto_program.instructions.end()) + representative_inst == goto_program.instructions.end()) { msg.warning() << "Ignoring block " << (block_nr + 1) << " location " << it->location_number << " " << it->source_location() << " (bytecode-index already instrumented)" << messaget::eom; } - else if( - block_info.representative_inst == it && - block_info.source_location.is_nil()) + else if(representative_inst == it && source_location.is_nil()) { msg.warning() << "Ignoring block " << (block_nr + 1) << " location " << it->location_number << " " << function_id @@ -158,9 +101,12 @@ void cover_basic_blockst::report_block_anomalies( void cover_basic_blockst::output(std::ostream &out) const { - for(const auto &block_pair : block_map) - out << block_pair.first->source_location() << " -> " << block_pair.second - << '\n'; + // Output block mappings + for(std::size_t i = 0; i < blocks.size(); ++i) + { + if(auto inst = blocks.instruction_of(i)) + out << (*inst)->source_location() << " -> " << i << '\n'; + } } void cover_basic_blockst::add_block_lines( @@ -182,59 +128,61 @@ void cover_basic_blockst::add_block_lines( }); } +// ============================================================================ +// cover_basic_blocks_javat implementation (Java-specific behavior) +// ============================================================================ + cover_basic_blocks_javat::cover_basic_blocks_javat( - const goto_programt &_goto_program) + const goto_programt &goto_program) + : blocks(std::make_unique>()) { - forall_goto_program_instructions(it, _goto_program) + // Compute basic blocks using Java policy + blocks.compute(goto_program); + + // Initialize source lines for each block + block_source_lines.resize(blocks.size()); + + // Collect source lines for each instruction + forall_goto_program_instructions(it, goto_program) { + const std::size_t block_nr = blocks.block_of(it); + INVARIANT( + block_nr < block_source_lines.size(), "block number out of range"); const auto &location = it->source_location(); - const auto &bytecode_index = location.get_java_bytecode_index(); - auto entry = index_to_block.emplace(bytecode_index, block_infos.size()); - if(entry.second) - { - block_infos.push_back(it); - block_locations.push_back(location); - block_source_lines.emplace_back(location); - } - else - { - block_source_lines[entry.first->second].insert(location); - } + block_source_lines[block_nr].insert(location); } } std::size_t cover_basic_blocks_javat::block_of(goto_programt::const_targett t) const { - const auto &bytecode_index = t->source_location().get_java_bytecode_index(); - const auto it = index_to_block.find(bytecode_index); - INVARIANT(it != index_to_block.end(), "instruction must be part of a block"); - return it->second; + return blocks.block_of(t); } std::optional cover_basic_blocks_javat::instruction_of(const std::size_t block_nr) const { - PRECONDITION(block_nr < block_infos.size()); - return block_infos[block_nr]; + return blocks.instruction_of(block_nr); } const source_locationt & cover_basic_blocks_javat::source_location_of(const std::size_t block_nr) const { - PRECONDITION(block_nr < block_locations.size()); - return block_locations[block_nr]; + return blocks.source_location_of(block_nr); } const source_linest & cover_basic_blocks_javat::source_lines_of(const std::size_t block_nr) const { - PRECONDITION(block_nr < block_locations.size()); + PRECONDITION(block_nr < block_source_lines.size()); return block_source_lines[block_nr]; } void cover_basic_blocks_javat::output(std::ostream &out) const { - for(std::size_t i = 0; i < block_locations.size(); ++i) - out << block_locations[i] << " -> " << i << '\n'; + for(std::size_t i = 0; i < blocks.size(); ++i) + out << blocks.source_location_of(i) << " -> " << i << '\n'; } diff --git a/src/goto-instrument/cover_basic_blocks.h b/src/goto-instrument/cover_basic_blocks.h index 8c9bd2c2a89..b0d439fa89f 100644 --- a/src/goto-instrument/cover_basic_blocks.h +++ b/src/goto-instrument/cover_basic_blocks.h @@ -8,12 +8,19 @@ Author: Daniel Kroening /// \file /// Basic blocks detection for Coverage Instrumentation +/// +/// This module provides an adapter layer between the generic basic block +/// detection utility in src/analyses/basic_blocks.h and the coverage +/// instrumentation system. It extends the basic block detection with +/// source line tracking needed for coverage reporting. #ifndef CPROVER_GOTO_INSTRUMENT_COVER_BASIC_BLOCKS_H #define CPROVER_GOTO_INSTRUMENT_COVER_BASIC_BLOCKS_H #include +#include + #include "source_lines.h" class message_handlert; @@ -62,10 +69,18 @@ class cover_blocks_baset } }; +/// Default basic block detection for C/C++ with source line tracking +/// This adapter extends the generic basic_blockst with source line +/// information needed for coverage reporting. class cover_basic_blockst final : public cover_blocks_baset { public: - explicit cover_basic_blockst(const goto_programt &goto_program); + /// Create basic block detector for the given program + /// \param goto_program: The program to analyze + /// \param config: Configuration for block detection (optional) + explicit cover_basic_blockst( + const goto_programt &goto_program, + const basic_block_configt &config = basic_block_configt()); /// \param t: a goto instruction /// \return the block number of the block @@ -101,57 +116,32 @@ class cover_basic_blockst final : public cover_blocks_baset void output(std::ostream &out) const override; private: - typedef std::map< - goto_programt::const_targett, - std::size_t, - goto_programt::target_less_than> - block_mapt; + /// The underlying basic block detector + basic_blockst blocks; + /// Extended block information with source lines struct block_infot { - /// the program location to instrument for this block - std::optional representative_inst; - - /// the source location representative for this block - /// (we need a separate copy of source locations because we attach - /// the line number ranges to them) - source_locationt source_location; - /// the set of source code lines belonging to this block source_linest source_lines; }; - /// map program locations to block numbers - block_mapt block_map; - /// map block numbers to block information + /// Extended information for each block std::vector block_infos; /// Adds the lines which \p instruction spans to \p block. static void add_block_lines( - cover_basic_blockst::block_infot &block, + block_infot &block, const goto_programt::instructiont &instruction); - - /// If this block is a continuation of a previous block through unconditional - /// forward gotos, return this blocks number. - static std::optional continuation_of_block( - const goto_programt::const_targett &instruction, - block_mapt &block_map); }; +/// Java-specific basic block detection with source line tracking class cover_basic_blocks_javat final : public cover_blocks_baset { -private: - // map block number to first instruction of the block - std::vector block_infos; - // map block number to its location - std::vector block_locations; - // map java indexes to block indexes - std::unordered_map index_to_block; - // map block number to its source lines - std::vector block_source_lines; - public: - explicit cover_basic_blocks_javat(const goto_programt &_goto_program); + /// Create basic block detector for Java programs + /// \param goto_program: The program to analyze + explicit cover_basic_blocks_javat(const goto_programt &goto_program); /// \param t: a goto instruction /// \return block number the given goto instruction is part of @@ -173,6 +163,17 @@ class cover_basic_blocks_javat final : public cover_blocks_baset /// Outputs the list of blocks void output(std::ostream &out) const override; + +private: + /// The underlying basic block detector with Java policy + basic_blocks_templatet< + const goto_programt, + goto_programt::const_targett, + goto_programt::target_less_than> + blocks; + + /// Source lines for each block + std::vector block_source_lines; }; #endif // CPROVER_GOTO_INSTRUMENT_COVER_BASIC_BLOCKS_H