Switch lack of termination to warning

Signed-off-by: Alan Jowett <[email protected]>
vbpf · Oct 22, 2024 · 56956d1 · 56956d1
1 parent 48d0043
commit 56956d1
Show file tree

Hide file tree

Showing 2 changed files with 6 additions and 5 deletions.
diff --git a/src/crab_verifier.cpp b/src/crab_verifier.cpp
@@ -102,6 +102,11 @@ static checks_db generate_report(cfg_t& cfg, const crab::invariant_table_t& pre_
         if (last_inv.is_bottom()) {
             m_db.add_warning(label_t::exit, "Exit is unreachable.");
         }
+
+        const crab::number_t max_loop_count{100000};
+        if (m_db.max_loop_count > max_loop_count) {
+            m_db.add_warning(label_t::exit, "Could not prove termination.");
+        }
     }
 
     return m_db;
@@ -133,10 +138,6 @@ static void print_report(std::ostream& os, const checks_db& db, const Instructio
         }
     }
     os << "\n";
-    const crab::number_t max_loop_count{100000};
-    if (db.max_loop_count > max_loop_count) {
-        os << "Could not prove termination.\n";
-    }
 }
 
 static checks_db get_analysis_report(std::ostream& s, cfg_t& cfg, const crab::invariant_table_t& pre_invariants,

diff --git a/test-data/loop.yaml b/test-data/loop.yaml
@@ -186,7 +186,7 @@ post:
   - "pc[1]=[1, +oo]"
 
 messages:
-  - "Could not prove termination."
+  - "exit: Could not prove termination."
 
 ---
 test-case: realistic forward loop