From 77f3dc9cbc12ff91f4d40f0eff35666104efc356 Mon Sep 17 00:00:00 2001 From: Alan Jowett Date: Tue, 5 Nov 2024 12:50:55 -0800 Subject: [PATCH] PR feedback Signed-off-by: Alan Jowett --- src/crab/cfg.hpp | 1 - src/crab/fwd_analyzer.cpp | 10 +++++----- 2 files changed, 5 insertions(+), 6 deletions(-) diff --git a/src/crab/cfg.hpp b/src/crab/cfg.hpp index bdebe0960..f72ee4672 100644 --- a/src/crab/cfg.hpp +++ b/src/crab/cfg.hpp @@ -267,7 +267,6 @@ class cfg_t final { private: basic_block_map_t m_blocks; - std::optional> m_potential_loop_headers; using visited_t = std::set; diff --git a/src/crab/fwd_analyzer.cpp b/src/crab/fwd_analyzer.cpp index af30f6c92..b54b90186 100644 --- a/src/crab/fwd_analyzer.cpp +++ b/src/crab/fwd_analyzer.cpp @@ -125,11 +125,11 @@ std::pair run_forward_analyzer(const cfg_t if (thread_local_options.check_termination) { // For every potential loop header, initialize the loop counter to 0. for (const auto& label : cfg.potential_loop_headers()) { - // The initial path adds labels in the form of (from, to) where - // where from is the PC and to is -1. When the CFG is expanded to be non-deterministic - // branches with actual to labels are added, but these will not have loop counters as - // loop counters are only added to the deterministic cfg. - // Ignore labels added by the non-deterministic expansion. + // See prepare_cfg() in src/asm_cfg.cpp. + // It adds IncrementLoopCounter to blocks that are possible loops, but only + // on the first pass, where all labels are in the form from::-1. After the cfg is converted to its + // non-deterministic form there will be additional labels in the form of from::to where to will be != -1. + // Only initialize the loop counter for the original labels. if (label.to != -1) { continue; }