From 78f5c2161c39338f5a1e61fd62e50379f9be99cf Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Sun, 26 Dec 2021 17:40:07 +0100
Subject: [PATCH] [aorai] don't forget to update loop invariant table when
 fixpoint is reached

... even if it already has an entry: said entry can come from another, unrelated
call.
---
 src/plugins/aorai/aorai_dataflow.ml           |  4 +--
 src/plugins/aorai/tests/ya/observed.i         |  4 ++-
 .../aorai/tests/ya/oracle/observed.res.oracle | 36 +++++++++++++++++++
 3 files changed, 40 insertions(+), 4 deletions(-)

diff --git a/src/plugins/aorai/aorai_dataflow.ml b/src/plugins/aorai/aorai_dataflow.ml
index 01e70eb8687..a4c41ea78df 100644
--- a/src/plugins/aorai/aorai_dataflow.ml
+++ b/src/plugins/aorai/aorai_dataflow.ml
@@ -416,9 +416,7 @@ module Computer(I: Init) = struct
       Data_for_aorai.pretty_state old Data_for_aorai.pretty_state cur;
     if Data_for_aorai.included_state cur old then begin
       Aorai_option.debug ~dkey:forward_dkey "Included";
-      if is_loop && Cil_datatype.Stmt.Set.mem stmt loops &&
-         Data_for_aorai.Aorai_state.Map.is_empty
-           (Data_for_aorai.get_loop_invariant_state stmt)
+      if is_loop && Cil_datatype.Stmt.Set.mem stmt loops
       then
         Data_for_aorai.set_loop_invariant_state stmt cur;
       None
diff --git a/src/plugins/aorai/tests/ya/observed.i b/src/plugins/aorai/tests/ya/observed.i
index 34cf1c5d371..28b40a8ed50 100644
--- a/src/plugins/aorai/tests/ya/observed.i
+++ b/src/plugins/aorai/tests/ya/observed.i
@@ -4,7 +4,9 @@
 
 void f(void) {}
 
-void g(void) {}
+void g(void) {
+  for (int i = 0; i < 1; i++) ;
+}
 
 void h(void) {
   g();
diff --git a/src/plugins/aorai/tests/ya/oracle/observed.res.oracle b/src/plugins/aorai/tests/ya/oracle/observed.res.oracle
index 4e5eac6d384..d02c3691359 100644
--- a/src/plugins/aorai/tests/ya/oracle/observed.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/observed.res.oracle
@@ -183,6 +183,42 @@ void f(void)
  */
 void g(void)
 {
+  /*@ ghost int aorai_Loop_Init_4; */
+  int i = 0;
+  /*@ ghost aorai_Loop_Init_4 = 1; */
+  aorai_loop_4:
+  /*@ loop invariant Aorai: 0 ≡ aorai_intermediate_state;
+      loop invariant
+        Aorai:
+          1 ≡ aorai_intermediate_state_0 ∨
+          0 ≡ aorai_intermediate_state_0;
+      loop invariant Aorai: 0 ≡ final;
+      loop invariant Aorai: 1 ≡ first_step ∨ 0 ≡ first_step;
+      loop invariant Aorai: 0 ≡ init;
+      loop invariant
+        Aorai: 1 ≡ aorai_intermediate_state_0 ∨ 1 ≡ first_step;
+      loop invariant
+        Aorai:
+          aorai_Loop_Init_4 ≢ 0 ⇒
+          \at(1 ≡ aorai_intermediate_state_0,Pre) ⇒ 0 ≡ first_step;
+      loop invariant
+        Aorai:
+          aorai_Loop_Init_4 ≢ 0 ⇒
+          \at(1 ≡ first_step,Pre) ⇒ 0 ≡ aorai_intermediate_state_0;
+      loop invariant
+        Aorai:
+          aorai_Loop_Init_4 ≡ 0 ⇒
+          \at(0 ≡ first_step,aorai_loop_4) ⇒ 0 ≡ first_step;
+      loop invariant
+        Aorai:
+          aorai_Loop_Init_4 ≡ 0 ⇒
+          \at(0 ≡ aorai_intermediate_state_0,aorai_loop_4) ⇒
+          0 ≡ aorai_intermediate_state_0;
+  */
+  while (i < 1) {
+    /*@ ghost aorai_Loop_Init_4 = 0; */
+    i ++;
+  }
   return;
 }
 
-- 
GitLab