PR feedback

Signed-off-by: Alan Jowett <[email protected]>
vbpf · Oct 18, 2024 · b55897e · b55897e
1 parent 0bc118d
commit b55897e
Show file tree

Hide file tree

Showing 2 changed files with 6 additions and 6 deletions.
diff --git a/src/crab_verifier.cpp b/src/crab_verifier.cpp
@@ -98,7 +98,7 @@ static checks_db generate_report(cfg_t& cfg, const crab::invariant_table_t& pre_
         const auto last_inv = post_invariants.at(cfg.exit_label());
         m_db.max_loop_count = last_inv.get_loop_count_upper_bound();
 
-        // Test for the case where the exit is unreachable.
+         // Check if the exit is unreachable, which could indicate an infinite loop
         if (last_inv.is_bottom()) {
             m_db.add_unreachable(label_t::exit, "Exit is unreachable.");
         }

diff --git a/test-data/loop.yaml b/test-data/loop.yaml
@@ -283,7 +283,7 @@ post: []
 
 messages:
   - "1:2: Code is unreachable after 1:2"
-  - "exit: Exit is unreachable"
+  - "exit: Exit is unreachable."
 ---
 test-case: simple infinite loop, less than or equal
 options: ["termination"]
@@ -300,7 +300,7 @@ post: []
 
 messages:
   - "1:2: Code is unreachable after 1:2"
-  - "exit: Exit is unreachable"
+  - "exit: Exit is unreachable."
 
 ---
 test-case: simple infinite loop, equal
@@ -318,7 +318,7 @@ post: []
 
 messages:
   - "1:2: Code is unreachable after 1:2"
-  - "exit: Exit is unreachable"
+  - "exit: Exit is unreachable."
 
 ---
 test-case: simple infinite loop, greater than
@@ -336,7 +336,7 @@ post: []
 
 messages:
   - "1:2: Code is unreachable after 1:2"
-  - "exit: Exit is unreachable"
+  - "exit: Exit is unreachable."
 
 ---
 test-case: simple infinite loop, greater than or equal
@@ -354,4 +354,4 @@ post: []
 
 messages:
   - "1:2: Code is unreachable after 1:2"
-  - "exit: Exit is unreachable"
+  - "exit: Exit is unreachable."