Find highest loop count at any point in the program

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

src/crab_verifier.cpp

@@ -95,8 +95,10 @@ static checks_db generate_report(cfg_t& cfg, const crab::invariant_table_t& pre_
     }
 
     if (thread_local_options.check_termination) {
-        const auto last_inv = post_invariants.at(cfg.exit_label());
-        m_db.max_loop_count = last_inv.get_loop_count_upper_bound();
+        // Find the highest loop count of blocks that have a post-invariant.
+        for (const auto invariant : post_invariants){
+            m_db.max_loop_count = std::max(m_db.max_loop_count, invariant.second.get_loop_count_upper_bound());
+        }
     }
     return m_db;
 }

test-data/loop.yaml

@@ -266,3 +266,92 @@ post:
   - r4.uvalue-r2.svalue<=0
   - r4.uvalue-r2.uvalue<=0
   - r4.uvalue=[1, 255]
+
+---
+test-case: simple infinite loop, less than
+options: ["termination"]
+
+pre: []
+
+code:
+  <start>: |
+    r0 = 0
+    if r0 < 1 goto <start>
+    exit
+
+post: []
+
+messages:
+  - "1:2: Code is unreachable after 1:2"
+  - "Could not prove termination."
+---
+test-case: simple infinite loop, less than or equal
+options: ["termination"]
+
+pre: []
+
+code:
+  <start>: |
+    r0 = 0
+    if r0 <= 1 goto <start>
+    exit
+
+post: []
+
+messages:
+  - "1:2: Code is unreachable after 1:2"
+  - "Could not prove termination."
+
+---
+test-case: simple infinite loop, equal
+options: ["termination"]
+
+pre: []
+
+code:
+  <start>: |
+    r0 = 0
+    if r0 == 0 goto <start>
+    exit
+
+post: []
+
+messages:
+  - "1:2: Code is unreachable after 1:2"
+  - "Could not prove termination."
+
+---
+test-case: simple infinite loop, greater than
+options: ["termination"]
+
+pre: []
+
+code:
+  <start>: |
+    r0 = 1
+    if r0 > 0 goto <start>
+    exit
+
+post: []
+
+messages:
+  - "1:2: Code is unreachable after 1:2"
+  - "Could not prove termination."
+
+---
+test-case: simple infinite loop, greater than or equal
+options: ["termination"]
+
+pre: []
+
+code:
+  <start>: |
+    r0 = 1
+    if r0 >= 0 goto <start>
+    exit
+
+post: []
+
+messages:
+  - "1:2: Code is unreachable after 1:2"
+  - "Could not prove termination."