[wp] Collect code annots in GUI's order

- annots order for multiple emitters is unspecified,
- use the order used in the Printer

src/plugins/wp/cfgAnnot.ml

@@ -415,7 +415,7 @@ type code_assertion = {
   code_verified: WpPropId.pred_info option ;
 }
 
-(* Note: generated in REVERSE order *)
+(* Note: collected in REVERSE order *)
 module CodeAssertions = WpContext.StaticGenerator(CodeKey)
     (struct
       type key = CodeKey.t
@@ -424,8 +424,13 @@ module CodeAssertions = WpContext.StaticGenerator(CodeKey)
       let compile (kf,stmt) =
         let labels = NormAtLabels.labels_assert ~kf stmt in
         let normalize_pred p = NormAtLabels.preproc_annot labels p in
-        Annotations.fold_code_annot
-          begin fun _emitter ca l ->
+        let all_annot = (* ensures that the order is the one displayed in GUI *)
+          List.sort
+            Cil_datatype.Code_annotation.compare
+            (Annotations.code_annot stmt)
+        in
+        List.fold_left
+          begin fun l ca ->
             match ca.annot_content with
             | AStmtSpec _ when not @@ is_assembly stmt ->
                 let source = fst (Cil_datatype.Stmt.loc stmt) in
@@ -447,7 +452,7 @@ module CodeAssertions = WpContext.StaticGenerator(CodeKey)
                   code_verified = use verif p ;
                 } :: l
             | _ -> l
-          end stmt []
+          end [] all_annot
     end)
 
 let get_code_assertions ?(smoking=false) kf stmt =
@@ -538,9 +543,14 @@ module LoopContract = WpContext.StaticGenerator(CodeKey)
           { loop_pred = p ;
             loop_hyp = NoHyp ; loop_est = None ; loop_ind = Some i }
         in
+        let all_annot = (* ensures that the order is the one displayed in GUI *)
+          List.rev @@ List.sort
+            Cil_datatype.Code_annotation.compare
+            (Annotations.code_annot stmt)
+        in
         default_assigns stmt @@
-        Annotations.fold_code_annot
-          begin fun _emitter ca l ->
+        List.fold_left
+          begin fun l ca ->
             match ca.annot_content with
             | AInvariant(_,true,inv) ->
                 let g_hyp = WpPropId.mk_inv_hyp_id kf stmt ca in
@@ -580,12 +590,13 @@ module LoopContract = WpContext.StaticGenerator(CodeKey)
                       { l with loop_assigns = asgn :: l.loop_assigns }
                 end
             | _ -> l
-          end stmt {
-          loop_terminates = Some Logic_const.pfalse ;
-          loop_invariants = [] ;
-          loop_smoke = [] ;
-          loop_assigns = [] ;
-        }
+          end
+          { loop_terminates = Some Logic_const.pfalse ;
+            loop_invariants = [] ;
+            loop_smoke = [] ;
+            loop_assigns = [] ;
+          }
+          all_annot
     end)
 
 let get_loop_contract ?(smoking=false) ?terminates kf stmt =

src/plugins/wp/tests/wp/oracle/bug_rte.res.oracle

@@ -7,17 +7,17 @@
 ------------------------------------------------------------
 
 Goal Assertion 'rte,signed_overflow' (file bug_rte.i, line 7):
-Assume {
-  Type: is_sint32(i) /\ is_sint32(j).
-  (* Assertion 'rte,signed_overflow' *)
-  Have: i <= (2147483647 + (if (j = 1) then 1 else 0)).
-}
+Assume { Type: is_sint32(i) /\ is_sint32(j). }
 Prove: if (j = 1) then ((-2147483647) <= i) else ((-2147483648) <= i).
 
 ------------------------------------------------------------
 
 Goal Assertion 'rte,signed_overflow' (file bug_rte.i, line 7):
-Assume { Type: is_sint32(i) /\ is_sint32(j). }
+Assume {
+  Type: is_sint32(i) /\ is_sint32(j).
+  (* Assertion 'rte,signed_overflow' *)
+  Have: if (j = 1) then ((-2147483647) <= i) else ((-2147483648) <= i).
+}
 Prove: i <= (2147483647 + (if (j = 1) then 1 else 0)).
 
 ------------------------------------------------------------

src/plugins/wp/tests/wp_plugin/oracle_qualif/rte.res.oracle

@@ -6,16 +6,16 @@
 [rte:annot] annotating function job3
 [wp] 6 goals scheduled
 [wp] [Alt-Ergo] Goal typed_job_assert_rte_mem_access : Unsuccess
-[wp] [Alt-Ergo] Goal typed_job_assert_rte_mem_access_2 : Unsuccess
+[wp] [Alt-Ergo] Goal typed_job_assert_rte_mem_access_2 : Valid
 [wp] [Alt-Ergo] Goal typed_job_assert_rte_signed_overflow : Unsuccess
 [wp] [Alt-Ergo] Goal typed_job_assert_rte_signed_overflow_2 : Unsuccess
 [wp] [Qed] Goal typed_job_assert_rte_mem_access_3 : Valid
 [wp] [Alt-Ergo] Goal typed_job3_assert_rte_bool_value : Valid
-[wp] Proved goals:    2 / 6
+[wp] Proved goals:    3 / 6
   Qed:             1 
-  Alt-Ergo:        1  (unsuccess: 4)
+  Alt-Ergo:        2  (unsuccess: 3)
 ------------------------------------------------------------
  Functions                 WP     Alt-Ergo  Total   Success
-  job                       1        -        5      20.0%
+  job                       1        1        5      40.0%
   job3                      -        1        1       100%
 ------------------------------------------------------------