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

[wp] Fixes assumes normalization

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

src/plugins/wp/cfgAnnot.ml

@@ -75,13 +75,16 @@ let normalize_pre ~goal kf bhv ?assumes ip =
     let module L = NormAtLabels in
     let labels = L.labels_fct_pre in
     let id = WpPropId.mk_pre_id kf Kglobal bhv ip in
-    let p = L.preproc_annot labels ip.ip_content.tp_statement in
-    Some (id, implies ?assumes p)
+    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)
   else None
 
 let normalize_post ~goal kf bhv tk ?assumes (itk,ip) =
   if tk = itk && filter ~goal ip then
     let module L = NormAtLabels in
+    let at_pre e = Logic_const.pat (e, BuiltinLabel Pre) in
+    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
@@ -238,7 +241,8 @@ module CallContract = WpContext.StaticGenerator(Kernel_function)
         setup_preconditions kf ;
         List.iter
           begin fun bhv ->
-            let assumes = normalize_assumes (Ast_info.behavior_assumes bhv) in
+            (* Normalization of assumes is specific to each case *)
+            let assumes = Ast_info.behavior_assumes bhv in
             let mk_cond = normalize_pre ~goal:true kf bhv ~assumes in
             let mk_hpre = normalize_pre ~goal:false kf bhv ~assumes in
             let mk_post = normalize_post ~goal:false kf bhv ~assumes in

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

+int v ;
+
+/*@ assigns v ;
+    behavior b1:
+      assumes v == 1 ;
+      ensures v == 2 ;
+*/
+void foo(void){
+	if(v == 1) v = 2 ;
+}
+
+//@ requires v == 1 ;
+void bar(void){
+  foo();
+  //@ check v == 2 ;
+}

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

+# frama-c -wp [...]
+[kernel] Parsing tests/wp_acsl/assumes_labels.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Warning: Missing RTE guards
+------------------------------------------------------------
+  Function bar
+------------------------------------------------------------
+
+Goal Check (file tests/wp_acsl/assumes_labels.i, line 15):
+Prove: true.
+
+------------------------------------------------------------
+------------------------------------------------------------
+  Function foo
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_acsl/assumes_labels.i, line 3) in 'foo':
+Prove: true.
+
+------------------------------------------------------------
+------------------------------------------------------------
+  Function foo with behavior b1
+------------------------------------------------------------
+
+Goal Post-condition for 'b1' (file tests/wp_acsl/assumes_labels.i, line 6) in 'foo':
+Prove: true.
+
+------------------------------------------------------------

src/plugins/wp/tests/wp_acsl/oracle_qualif/assumes_labels.res.oracle

+# frama-c -wp [...]
+[kernel] Parsing tests/wp_acsl/assumes_labels.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Warning: Missing RTE guards
+[wp] 3 goals scheduled
+[wp] [Qed] Goal typed_foo_assigns : Valid
+[wp] [Qed] Goal typed_foo_b1_ensures : Valid
+[wp] [Qed] Goal typed_bar_check : Valid
+[wp] Proved goals:    3 / 3
+  Qed:             3
+------------------------------------------------------------
+ Functions                 WP     Alt-Ergo  Total   Success
+  foo                       2        -        2       100%
+  bar                       1        -        1       100%
+------------------------------------------------------------