PR feedback

Signed-off-by: Alan Jowett <[email protected]>

src/asm_cfg.cpp

@@ -365,7 +365,9 @@ cfg_t prepare_cfg(const InstructionSeq& prog, const program_info& info, const bo
     cfg_t det_cfg = instruction_seq_to_cfg(prog, must_have_exit);
 
     if (check_for_termination) {
-        // Add IncrementLoopCounter to blocks that are possible loops.
+        // Insert loop counter instructions at potential loop entry points to enforce
+        // an upper bound on iterations. The IncrementLoopCounter instruction will
+        // trigger a verification failure if the loop count exceeds the defined limit.
         for (auto const& this_label : det_cfg.potential_loop_headers()) {
             basic_block_t& bb = det_cfg.get_node(this_label);
             bb.insert_front(IncrementLoopCounter{this_label});

src/crab/cfg.hpp

@@ -67,10 +67,16 @@ class basic_block_t final {
 
     template <typename T, typename... Args>
     void insert_front(Args&&... args) {
+        assert(label() != label_t::entry);
+        assert(label() != label_t::exit);
         m_ts.insert(m_ts.begin(), T{std::forward<Args>(args)...});
     }
 
-    void insert_front(const Instruction& arg) { m_ts.insert(m_ts.begin(), arg); }
+    void insert_front(const Instruction& arg) {
+        assert(label() != label_t::entry);
+        assert(label() != label_t::exit);
+        m_ts.insert(m_ts.begin(), arg);
+    }
 
     explicit basic_block_t(label_t _label) : m_label(_label) {}