[logic] fix annotation table update same emitter adds multiple loop assigns

src/kernel_services/ast_data/annotations.ml

@@ -1151,16 +1151,18 @@ let add_code_annot emitter ?kf stmt ca =
            "trying to register a second variant for statement %a"
            Stmt.pretty stmt)
     | AAssigns (bhvs, assigns) ->
-      let filter ca =
+      let filter_ca ca =
         match ca.annot_content with
         | AAssigns (bhvs', _) -> is_same_behavior_set bhvs bhvs'
         | _ -> false
       in
-      let ca' = code_annot ~filter stmt in
+      let filter e ca = Emitter.equal e emitter && filter_ca ca in
+      let ca_e = code_annot_emitter ~filter stmt in
+      let ca_total = code_annot ~filter:filter_ca stmt in
       let new_a =
-        match ca' with
+        match ca_e with
         | [] -> a
-        | [ { annot_content = AAssigns(_, assigns') } as ca ] ->
+        | [ { annot_content = AAssigns(_, assigns') } as ca,_ ] ->
           remove_code_annot_internal emitter ~kf stmt ca;
           let merged =
             merge_assigns ~keep_empty:false assigns' assigns
@@ -1171,7 +1173,18 @@ let add_code_annot emitter ?kf stmt ca =
             "More than one loop assigns clause for a statement. \
              Annotations internal state broken."
       in
-      let ips = Property.ip_of_code_annot kf stmt new_a in
+      let ips =
+        match ca_total with
+        | [] -> Property.ip_of_code_annot kf stmt a
+        | [ { annot_content = AAssigns (_,assigns') } ] ->
+          let merged = merge_assigns ~keep_empty:false assigns' assigns in
+          Property.ip_of_code_annot
+            kf stmt { a with annot_content = AAssigns(bhvs,merged) }
+        | _ ->
+          Kernel.fatal
+            "More than one loop assigns clause for a statement. \
+             Annotations internal state broken."
+      in
       new_a, ips
     | AAllocation (bhvs, alloc) ->
       let filter ca =

tests/spec/loop_assigns_generated.ml

@@ -49,10 +49,12 @@ let main () =
   in
   let j = Cil.makeLocalVar def ~insert:true "j" Cil.intType in
   let k = Cil.makeLocalVar def ~insert:true "k" Cil.intType in
+  let l = Cil.makeLocalVar def ~insert:true "l" Cil.intType in
   let p = Cil.makeLocalVar def ~insert:true "p" Cil.intPtrType in
   let q = Cil.makeLocalVar def ~insert:true "q" Cil.intPtrType in
   add_assigns e1 kf s j;
   add_assigns e2 kf s k;
+  add_assigns e1 kf s l;
   add_allocates e1 kf s p;
   add_allocates e2 kf s q;
   Annotations.iter_code_annot (check_only_one Logic_utils.is_assigns) s;

tests/spec/oracle/loop_assigns_generated.res.oracle

@@ -4,10 +4,12 @@ void f(void)
 {
   int *q;
   int *p;
+  int l;
   int k;
   int j;
   int i = 0;
-  /*@ loop assigns i, (added_by_emitter1: j), (added_by_emitter2: k);
+  /*@ loop assigns i, (added_by_emitter1: j), (added_by_emitter1: l),
+                   (added_by_emitter2: k);
       loop allocates (added_by_emitter1: p), (added_by_emitter2: q);
   */
   while (i < 10) i ++;