Merge branch 'fix/wp/double-assumes-normalization' into 'master'

Fix/wp/double assumes normalization

See merge request frama-c/frama-c!4181

src/plugins/wp/cfgAnnot.ml

@@ -59,8 +59,7 @@ type behavior = {
 
 let normalize_assumes h =
   let module L = NormAtLabels in
-  let labels = L.labels_fct_pre in
-  L.preproc_annot labels h
+  L.preproc_annot L.labels_fct_pre h
 
 let implies ?assumes p =
   match assumes with None -> p | Some h -> Logic_const.pimplies (h,p)
@@ -77,7 +76,8 @@ let normalize_pre ~goal kf bhv ?assumes ip =
     let id = WpPropId.mk_pre_id kf Kglobal bhv ip in
     let pre = ip.ip_content.tp_statement in
     let assumes = Option.map normalize_assumes assumes in
-    Some (id, L.preproc_annot labels @@ implies ?assumes pre)
+    let precond = L.preproc_annot labels pre in
+    Some (id, implies ?assumes precond)
   else None
 
 let normalize_post ~goal kf bhv tk ?assumes (itk,ip) =
@@ -87,8 +87,8 @@ let normalize_post ~goal kf bhv tk ?assumes (itk,ip) =
     let assumes = Option.map (fun p -> normalize_assumes @@ at_pre p) assumes in
     let labels = L.labels_fct_post ~exit:(tk=Exits) in
     let id = WpPropId.mk_post_id kf Kglobal bhv (tk,ip) in
-    let p = L.preproc_annot labels ip.ip_content.tp_statement in
-    Some (id , implies ?assumes p)
+    let post = L.preproc_annot labels ip.ip_content.tp_statement in
+    Some (id , implies ?assumes post)
   else None
 
 let normalize_decreases (d, li) =

src/plugins/wp/tests/wp_acsl/label.i

+/* run.config_qualif
+   DONTRUN:
+*/
+
+int *p;
+
+/*@
+  axiomatic Observer {
+    predicate H{S}(int x) reads *p;
+    predicate P{S}(int x) reads *p;
+    predicate Q{S}(int x) reads *p;
+    predicate W{S}(int x) reads *p;
+  }
+*/
+
+/*@
+  assigns *s,*p;
+  behavior A:
+  assumes  H(*s);
+  requires P(*s);
+  ensures  Q(*s);
+*/
+int f(int *s);
+
+int g(int *s) {
+  int r = f(s);
+  /*@ assert W(*s); */
+  return r;
+}

src/plugins/wp/tests/wp_acsl/oracle/label.res.oracle

+# frama-c -wp [...]
+[kernel] Parsing label.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Warning: Missing RTE guards
+------------------------------------------------------------
+  Function g
+------------------------------------------------------------
+
+Goal Assertion (file label.i, line 27):
+Let x = Mint_0[s].
+Let m = Mint_0[p <- v][s <- v_1].
+Assume {
+  Type: is_sint32(v_1) /\ is_sint32(x).
+  (* Heap *)
+  Type: (region(p.base) <= 0) /\ (region(s.base) <= 0).
+  (* Call 'f' *)
+  Have: ((P_H(Mint_0, p, x) -> P_P(Mint_0, p, x))) /\
+      ((P_H(Mint_0, p, x) -> P_Q(m, p, v_1))).
+}
+Prove: P_W(m, p, v_1).
+
+------------------------------------------------------------
+
+Goal Instance of 'Pre-condition for 'A' (file label.i, line 20) in 'f'' in 'g' at initialization of 'r' (file label.i, line 26)
+:
+Let x = Mint_0[s].
+Assume {
+  Type: is_sint32(x).
+  (* Heap *)
+  Type: (region(p.base) <= 0) /\ (region(s.base) <= 0).
+  (* Goal *)
+  When: P_H(Mint_0, p, x).
+}
+Prove: P_P(Mint_0, p, x).
+
+------------------------------------------------------------
+[wp] label.i:23: Warning: 
+  Memory model hypotheses for function 'f':
+  /*@ behavior wp_typed:
+        requires \separated(p, &p);
+        requires \separated(s, &p); */
+  int f(int *s);
+[wp] label.i:25: Warning: 
+  Memory model hypotheses for function 'g':
+  /*@ behavior wp_typed:
+        requires \separated(s, &p); */
+  int g(int *s);