Merge branch 'bugfix/wp/pub-issue-11' into test

src/plugins/wp/Factory.ml

@@ -129,13 +129,7 @@ struct
     if S.mem x.vname (get_vars ()) then ByValue else
       V.param x
 
-  let hypotheses () =
-    let kf,init = match WpContext.get_scope () with
-      | WpContext.Global -> None,false
-      | WpContext.Kf f -> Some f, WpStrategy.is_main_init f in
-    let w = ref MemoryContext.empty in
-    V.iter ?kf ~init (fun vi -> w := MemoryContext.set vi (param vi) !w) ;
-    MemoryContext.requires !w
+  let iter = V.iter
 
 end
 

src/plugins/wp/Makefile.in

@@ -67,7 +67,7 @@ PLUGIN_CMO:= \
 	LogicUsage RefUsage \
 	Layout Region \
 	RegionAnnot RegionAccess RegionDump RegionAnalysis \
-	cil2cfg normAtLabels wpPropId mcfg \
+	cil2cfg normAtLabels wpPropId wpStrategy mcfg \
 	Lang Repr Matrix Passive Splitter \
 	LogicBuiltins Definitions \
 	Cmath Cint Cfloat Vset Vlist Cstring Cvalues \
@@ -81,7 +81,7 @@ PLUGIN_CMO:= \
 	Sigma MemLoader \
 	MemEmpty MemZeroAlias MemVar \
 	MemMemory MemTyped MemRegion \
-	wpReached wpStrategy wpRTE wpAnnot \
+	wpReached wpRTE wpAnnot \
 	CfgCompiler StmtSemantics \
 	VCS script proof wpo wpReport \
 	Footprint Tactical Strategy \

src/plugins/wp/MemVar.ml

@@ -37,7 +37,7 @@ module type VarUsage =
 sig
   val datatype : string
   val param : varinfo -> MemoryContext.param
-  val hypotheses : unit -> MemoryContext.clause list
+  val iter: ?kf:kernel_function -> init:bool -> (varinfo -> unit) -> unit
 end
 
 module Make(V : VarUsage)(M : Sigs.Model) =
@@ -52,7 +52,27 @@ struct
   let no_binder = { bind = fun _ f v -> f v }
   let configure_ia _ = no_binder
 
-  let hypotheses () = V.hypotheses () @ M.hypotheses ()
+  let hypotheses () =
+    let kf,init = match WpContext.get_scope () with
+      | WpContext.Global -> None,false
+      | WpContext.Kf f -> Some f, WpStrategy.is_main_init f in
+    let w = ref MemoryContext.empty in
+    V.iter ?kf ~init (fun vi -> w := MemoryContext.set vi (V.param vi) !w) ;
+    let add_assign kf _emitter  = function
+      | WritesAny ->
+          Wp_parameters.warning
+            ~wkey:Wp_parameters.wkey_imprecise_hypotheses_assigns
+            "No assigns for function '%a', %s hypotheses will be imprecise"
+            Kernel_function.pretty kf datatype
+      | Writes l ->
+          List.iter (fun (e,_ds) -> w := MemoryContext.assigned e !w) l
+    in
+    begin match kf with
+      | None -> ()
+      | Some kf ->
+          Annotations.iter_assigns (add_assign kf) kf Cil.default_behavior_name
+    end ;
+    MemoryContext.requires !w @ M.hypotheses ()
 
   (* -------------------------------------------------------------------------- *)
   (* ---  Chunk                                                             --- *)

src/plugins/wp/MemVar.mli

@@ -30,8 +30,8 @@ module type VarUsage =
 sig
   val datatype : string
   val param : varinfo -> MemoryContext.param
-  (** Memory Model Hypotheses *)
-  val hypotheses : unit -> MemoryContext.clause list
+  val iter: ?kf:kernel_function -> init:bool -> (varinfo -> unit) -> unit
+
 end
 
 module Make(V : VarUsage)(M : Sigs.Model) : Sigs.Model

src/plugins/wp/MemoryContext.ml

@@ -46,11 +46,13 @@ type zone =
   | Var of varinfo   (* &x     - the cell x *)
   | Ptr of varinfo   (* p      - the cell pointed by p *)
   | Arr of varinfo   (* p+(..) - the cell and its neighbors pointed by p *)
+  | Term of term     (* use the ACSL term as is *)
 
 type partition = {
   globals : zone list ; (* [ &G , G[...], ... ] *)
   to_heap : zone list ; (* [ p, ... ] *)
   context : zone list ; (* [ p+(..), ... ] *)
+  assigned: identified_term list (* Must refer to pointed locations *)
 }
 
 type clause = Valid of zone | Separated of zone list list
@@ -64,6 +66,7 @@ let pp_zone fmt = function
   | Arr vi -> Format.fprintf fmt "%a+(..)" Varinfo.pretty vi
   | Ptr vi -> Varinfo.pretty fmt vi
   | Var vi -> Format.fprintf fmt "&%a" Varinfo.pretty vi
+  | Term t -> Format.fprintf fmt "%a" Cil_printer.pp_term t
 
 let pp_region fmt = function
   | [] -> Format.pp_print_string fmt "\\empty"
@@ -87,21 +90,70 @@ let pp_clause fmt = function
 (* -------------------------------------------------------------------------- *)
 (* --- Memory Context                                                     --- *)
 (* -------------------------------------------------------------------------- *)
+
+let rec ptr_of = function
+  | Ctype t -> Ctype (TPtr(t, []))
+  | t when Logic_typing.is_set_type t ->
+      let t = Logic_typing.type_of_set_elem t in
+      Logic_const.make_set_type (ptr_of t)
+  | _ -> assert false
+
+let rec addr_of_lval ?loc term =
+  let typ = ptr_of term.term_type in
+  match term.term_node with
+  | TLval lv ->
+      Logic_utils.mk_logic_AddrOf ?loc lv typ
+  | TCastE (_, t) | TLogic_coerce (_, t) ->
+      addr_of_lval ?loc t
+  | Tif(c, t, e) ->
+      let t = addr_of_lval ?loc t in
+      let e = addr_of_lval ?loc e in
+      Logic_const.term ?loc (Tif(c, t, e)) typ
+  | Tat( _, _) ->
+      term
+  | Tunion l ->
+      let l = List.map (addr_of_lval ?loc) l in
+      Logic_const.term ?loc (Tunion l) typ
+  | Tinter l ->
+      let l = List.map (addr_of_lval ?loc) l in
+      Logic_const.term ?loc (Tinter l) typ
+  | Tcomprehension (t, qs, p) ->
+      let t = addr_of_lval ?loc t in
+      Logic_const.term ?loc (Tcomprehension (t,qs,p)) typ
+  | _ -> term
+
 let add_region r s = if r = [] then s else r::s
 
-let separated partition =
-  List.rev @@
-  add_region (List.rev partition.to_heap) @@
-  add_region (List.rev partition.globals) @@
-  List.map (fun z -> [z]) partition.context
+let main_separation partition =
+  let separated =
+    List.rev @@
+    add_region (List.rev partition.to_heap) @@
+    add_region (List.rev partition.globals) @@
+    List.map (fun z -> [z]) partition.context
+  in
+  Separated separated
+
+let assigns_separation partition =
+  if partition.globals = [] then []
+  else
+    let assign_zone t = Term (addr_of_lval t.it_content) in
+    List.map
+      (fun t -> Separated ([[assign_zone t]] @ [ partition.globals ]))
+      partition.assigned
 
 let validity partition =
   List.rev @@ List.map (fun z -> Valid z) partition.context
 
 let requires partition =
-  let s = separated partition in
+  let ms = main_separation partition in
+  let ass_sep = assigns_separation partition in
+  let not_trivial_separation = function
+    | Separated s -> not (is_separated_true s)
+    | Valid _ -> false
+  in
+  let s = List.filter not_trivial_separation (ms :: ass_sep) in
   let v = validity partition in
-  if not (is_separated_true s) then Separated s :: v else v
+  s @ v
 
 (* -------------------------------------------------------------------------- *)
 (* --- Partition                                                          --- *)
@@ -111,6 +163,7 @@ let empty = {
   globals = [] ;
   context = [] ;
   to_heap = [] ;
+  assigned = [] ;
 }
 
 let set x p w =
@@ -135,4 +188,25 @@ let set x p w =
         { w with to_heap = z :: w.to_heap }
       else w
 
+let assigned t w =
+  let rec assigned_via_pointer t =
+    match t.term_node with
+    | TLval (TMem _, _) ->
+        true
+    | TCastE (_, t) | TLogic_coerce (_, t)
+    | Tcomprehension(t, _, _) | Tat (t, _) ->
+        assigned_via_pointer t
+    | Tunion l | Tinter l ->
+        List.exists assigned_via_pointer l
+    | Tif (_, t1, t2) ->
+        assigned_via_pointer t1 || assigned_via_pointer t2
+    | _ ->
+        false
+  in
+  let assigned =
+    if assigned_via_pointer t.it_content then t :: w.assigned
+    else w.assigned
+  in
+  { w with assigned = assigned }
+
 (* -------------------------------------------------------------------------- *)

src/plugins/wp/MemoryContext.mli

@@ -30,11 +30,9 @@ type partition
 
 val empty : partition
 val set : varinfo -> param -> partition -> partition
+val assigned : identified_term -> partition -> partition
 
-type zone =
-  | Var of varinfo   (** [&x] the cell x *)
-  | Ptr of varinfo   (** [p] the cell pointed by p *)
-  | Arr of varinfo   (** [p+(..)] the cell and its neighbors pointed by p *)
+type zone
 
 type clause =
   | Valid of zone

src/plugins/wp/tests/wp_bts/oracle/bts0843.res.oracle

@@ -53,3 +53,6 @@ Goal Instance of 'Pre-condition (file tests/wp_bts/bts0843.i, line 12) in 'f3''
 Prove: true.
 
 ------------------------------------------------------------
+[wp] Warning: Memory model hypotheses for function 'f3':
+  /*@ behavior typed: requires \separated(&p->a,&p); */
+  void f3(void);

src/plugins/wp/tests/wp_bts/oracle_qualif/bts0843.res.oracle

@@ -16,3 +16,6 @@
   f3                        1        -        1       100%
   g3                        1        2        3       100%
 ------------------------------------------------------------
+[wp] Warning: Memory model hypotheses for function 'f3':
+  /*@ behavior typed: requires \separated(&p->a,&p); */
+  void f3(void);

src/plugins/wp/tests/wp_hoare/alias_assigns_hypotheses.i

+/* run.config_qualif
+	 DONT_RUN:
+*/
+
+int global[1];
+int *g_alias;
+
+/*@ requires \valid(g_alias);
+    assigns *g_alias;
+    ensures *g_alias == 1;
+    ensures \old(global[0]) == global[0]; */
+void global_alias(void) {
+	*g_alias = 1;
+}
+
+/*@ requires \valid(g_alias);
+    assigns *g_alias;
+    ensures *g_alias == 1; */
+void global_no_alias(void) {
+	*g_alias = 1;
+}
+
+/*@ requires \valid(f_alias);
+    assigns *f_alias;
+    ensures *f_alias == 1;
+    ensures \old(global[0]) == global[0]; */
+void formal_alias(int* f_alias) {
+	*f_alias = 1;
+}
+
+/*@ requires \valid(f_alias);
+    assigns *f_alias;
+    ensures *f_alias == 1; */
+void formal_no_alias(int* f_alias) {
+	*f_alias = 1;
+}
+
+/*@ requires \valid(alias_array);
+    assigns (*alias_array)[0 .. 1];
+    ensures (*alias_array)[0] == 1;
+    ensures (*alias_array)[1] == 1;
+    ensures \old(global[0]) == global[0]; */
+void formal_alias_array(int (*alias_array)[2]){
+  (*alias_array)[0] = 1;
+  (*alias_array)[1] = 1;
+}
+
+// With field
+
+struct X { int x; };
+
+/*@ requires \valid(x);
+    assigns x->x ;
+    ensures x->x == 1;
+    ensures \old(global[0]) == global[0]; */
+void field_alias(struct X* x){
+  x->x = 1 ;
+}
+
+// With field, via set
+
+// Through set:
+
+/*@ requires \valid(x);
+    assigns x[0..3].x ;
+    ensures x->x == 1;
+    ensures \old(global[0]) == global[0]; */
+void field_range_alias(struct X* x){
+  x->x = 1 ;
+}
+
+/*@ requires \valid(g_alias);
+    assigns { *g_alias, *f_alias } ;
+    ensures *g_alias == 1;
+    ensures \old(global[0]) == global[0]; */
+void set_alias(int *f_alias) {
+  *g_alias = 1;
+}
+
+
+// Through comprehension:
+
+/*@ requires \valid(g_alias);
+    assigns { *alias | int* alias ; alias == \at(g_alias, Pre) } ;
+    ensures *g_alias == 1;
+    ensures \old(global[0]) == global[0]; */
+void comprehension_alias(void) {
+  *g_alias = 1;
+}
+
+// Through union:
+
+/*@ requires \valid(g_alias);
+    assigns \union(*g_alias, *f_alias) ;
+    ensures *g_alias == 1;
+    ensures \old(global[0]) == global[0]; */
+void union_alias(int *f_alias) {
+  *g_alias = 1;
+}

src/plugins/wp/tests/wp_hoare/oracle/alias_assigns_hypotheses.res.oracle

+# frama-c -wp [...]
+[kernel] Parsing tests/wp_hoare/alias_assigns_hypotheses.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Loading driver 'share/wp.driver'
+[wp] Warning: Missing RTE guards
+------------------------------------------------------------
+  Function comprehension_alias
+------------------------------------------------------------
+
+Goal Post-condition (file tests/wp_hoare/alias_assigns_hypotheses.i, line 85) in 'comprehension_alias':
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Post-condition (file tests/wp_hoare/alias_assigns_hypotheses.i, line 86) in 'comprehension_alias':
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_hoare/alias_assigns_hypotheses.i, line 84) in 'comprehension_alias':
+Effect at line 88
+Prove: true.
+
+------------------------------------------------------------
+------------------------------------------------------------
+  Function field_alias
+------------------------------------------------------------
+
+Goal Post-condition (file tests/wp_hoare/alias_assigns_hypotheses.i, line 54) in 'field_alias':
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Post-condition (file tests/wp_hoare/alias_assigns_hypotheses.i, line 55) in 'field_alias':
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_hoare/alias_assigns_hypotheses.i, line 53) in 'field_alias':
+Effect at line 57
+Prove: true.
+
+------------------------------------------------------------
+------------------------------------------------------------
+  Function field_range_alias
+------------------------------------------------------------
+
+Goal Post-condition (file tests/wp_hoare/alias_assigns_hypotheses.i, line 66) in 'field_range_alias':
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Post-condition (file tests/wp_hoare/alias_assigns_hypotheses.i, line 67) in 'field_range_alias':
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_hoare/alias_assigns_hypotheses.i, line 65) in 'field_range_alias':
+Effect at line 69
+Prove: true.
+
+------------------------------------------------------------
+------------------------------------------------------------
+  Function formal_alias
+------------------------------------------------------------
+
+Goal Post-condition (file tests/wp_hoare/alias_assigns_hypotheses.i, line 25) in 'formal_alias':
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Post-condition (file tests/wp_hoare/alias_assigns_hypotheses.i, line 26) in 'formal_alias':
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_hoare/alias_assigns_hypotheses.i, line 24) in 'formal_alias':
+Effect at line 28
+Prove: true.
+
+------------------------------------------------------------
+------------------------------------------------------------
+  Function formal_alias_array
+------------------------------------------------------------
+
+Goal Post-condition (file tests/wp_hoare/alias_assigns_hypotheses.i, line 40) in 'formal_alias_array':
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Post-condition (file tests/wp_hoare/alias_assigns_hypotheses.i, line 41) in 'formal_alias_array':
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Post-condition (file tests/wp_hoare/alias_assigns_hypotheses.i, line 42) in 'formal_alias_array':
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_hoare/alias_assigns_hypotheses.i, line 39) in 'formal_alias_array' (1/2):
+Effect at line 44
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_hoare/alias_assigns_hypotheses.i, line 39) in 'formal_alias_array' (2/2):
+Effect at line 45
+Prove: true.
+
+------------------------------------------------------------
+------------------------------------------------------------
+  Function formal_no_alias
+------------------------------------------------------------
+
+Goal Post-condition (file tests/wp_hoare/alias_assigns_hypotheses.i, line 33) in 'formal_no_alias':
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_hoare/alias_assigns_hypotheses.i, line 32) in 'formal_no_alias':
+Effect at line 35
+Prove: true.
+
+------------------------------------------------------------
+------------------------------------------------------------
+  Function global_alias
+------------------------------------------------------------
+
+Goal Post-condition (file tests/wp_hoare/alias_assigns_hypotheses.i, line 10) in 'global_alias':
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Post-condition (file tests/wp_hoare/alias_assigns_hypotheses.i, line 11) in 'global_alias':
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_hoare/alias_assigns_hypotheses.i, line 9) in 'global_alias':
+Effect at line 13
+Prove: true.
+
+------------------------------------------------------------
+------------------------------------------------------------
+  Function global_no_alias
+------------------------------------------------------------
+
+Goal Post-condition (file tests/wp_hoare/alias_assigns_hypotheses.i, line 18) in 'global_no_alias':
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_hoare/alias_assigns_hypotheses.i, line 17) in 'global_no_alias':
+Effect at line 20
+Prove: true.
+
+------------------------------------------------------------
+------------------------------------------------------------
+  Function set_alias
+------------------------------------------------------------
+
+Goal Post-condition (file tests/wp_hoare/alias_assigns_hypotheses.i, line 74) in 'set_alias':
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Post-condition (file tests/wp_hoare/alias_assigns_hypotheses.i, line 75) in 'set_alias':
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_hoare/alias_assigns_hypotheses.i, line 73) in 'set_alias':
+Effect at line 77
+Prove: true.
+
+------------------------------------------------------------
+------------------------------------------------------------
+  Function union_alias
+------------------------------------------------------------
+
+Goal Post-condition (file tests/wp_hoare/alias_assigns_hypotheses.i, line 95) in 'union_alias':
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Post-condition (file tests/wp_hoare/alias_assigns_hypotheses.i, line 96) in 'union_alias':
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_hoare/alias_assigns_hypotheses.i, line 94) in 'union_alias':
+Effect at line 98
+Prove: true.
+
+------------------------------------------------------------
+[wp] Warning: Memory model hypotheses for function 'global_alias':
+  /*@
+     behavior typed:
+     requires \separated(g_alias,\union(&g_alias,global+(..)));
+     */
+  void global_alias(void);
+[wp] Warning: Memory model hypotheses for function 'global_no_alias':
+  /*@ behavior typed: requires \separated(g_alias,&g_alias); */
+  void global_no_alias(void);
+[wp] Warning: Memory model hypotheses for function 'formal_alias':
+  /*@
+     behavior typed:
+     requires \separated(global+(..),f_alias);
+     requires \separated(f_alias,global+(..));
+     */
+  void formal_alias(int *f_alias);
+[wp] Warning: Memory model hypotheses for function 'formal_alias_array':
+  /*@
+     behavior typed:
+     requires \separated(global+(..),alias_array+(..));
+     requires \separated(&(*alias_array)[0 .. 1],global+(..));
+     */
+  void formal_alias_array(int (*alias_array)[2]);
+[wp] Warning: Memory model hypotheses for function 'field_alias':
+  /*@
+     behavior typed:
+     requires \separated(global+(..),x);
+     requires \separated(&x->x,global+(..));
+     */
+  void field_alias(struct X *x);
+[wp] Warning: Memory model hypotheses for function 'field_range_alias':
+  /*@
+     behavior typed:
+     requires \separated(global+(..),x+(..));
+     requires \separated(&(x + (0 .. 3))->x,global+(..));
+     */
+  void field_range_alias(struct X *x);
+[wp] Warning: Memory model hypotheses for function 'set_alias':
+  /*@
+     behavior typed:
+     requires \separated(\union(global+(..),&g_alias),f_alias);
+     requires \separated({g_alias, f_alias},\union(&g_alias,global+(..)));
+     */
+  void set_alias(int *f_alias);
+[wp] Warning: Memory model hypotheses for function 'comprehension_alias':
+  /*@
+     behavior typed:
+     requires \separated({alias | int *alias; alias ≡ \at(g_alias,Pre)},
+                \union(&g_alias,global+(..)));
+     */
+  void comprehension_alias(void);
+[wp] Warning: Memory model hypotheses for function 'union_alias':
+  /*@
+     behavior typed:
+     requires \separated(\union(global+(..),&g_alias),f_alias);
+     requires \separated({g_alias, f_alias},\union(&g_alias,global+(..)));
+     */
+  void union_alias(int *f_alias);

src/plugins/wp/tests/wp_hoare/oracle/reference_and_struct.res.oracle

@@ -255,3 +255,6 @@ Prove: true.
 [wp] Warning: Memory model hypotheses for function 'reset':
   /*@ behavior typed_ref: requires \valid(p); */
   void reset(struct T *p);
+[wp] Warning: Memory model hypotheses for function 'call_reset_5_tps':
+  /*@ behavior typed_ref: requires \separated(tps[9] + (0 .. 4),tps+(..)); */
+  void call_reset_5_tps(void);

src/plugins/wp/tests/wp_hoare/oracle_qualif/alias_assigns_hypotheses.res.oracle

+# frama-c -wp [...]
+[kernel] Parsing tests/wp_hoare/alias_assigns_hypotheses.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Loading driver 'share/wp.driver'
+[wp] Warning: Missing RTE guards
+[wp] 30 goals scheduled
+[wp] [Qed] Goal typed_comprehension_alias_ensures : Valid
+[wp] [Qed] Goal typed_comprehension_alias_ensures_2 : Valid
+[wp] [Qed] Goal typed_comprehension_alias_assigns : Valid
+[wp] [Qed] Goal typed_field_alias_ensures : Valid
+[wp] [Qed] Goal typed_field_alias_ensures_2 : Valid
+[wp] [Qed] Goal typed_field_alias_assigns : Valid
+[wp] [Qed] Goal typed_field_range_alias_ensures : Valid
+[wp] [Qed] Goal typed_field_range_alias_ensures_2 : Valid
+[wp] [Qed] Goal typed_field_range_alias_assigns : Valid
+[wp] [Qed] Goal typed_formal_alias_ensures : Valid
+[wp] [Qed] Goal typed_formal_alias_ensures_2 : Valid
+[wp] [Qed] Goal typed_formal_alias_assigns : Valid
+[wp] [Qed] Goal typed_formal_alias_array_ensures : Valid
+[wp] [Qed] Goal typed_formal_alias_array_ensures_2 : Valid
+[wp] [Qed] Goal typed_formal_alias_array_ensures_3 : Valid
+[wp] [Qed] Goal typed_formal_alias_array_assigns_part1 : Valid
+[wp] [Qed] Goal typed_formal_alias_array_assigns_part2 : Valid
+[wp] [Qed] Goal typed_formal_no_alias_ensures : Valid
+[wp] [Qed] Goal typed_formal_no_alias_assigns : Valid
+[wp] [Qed] Goal typed_global_alias_ensures : Valid
+[wp] [Qed] Goal typed_global_alias_ensures_2 : Valid
+[wp] [Qed] Goal typed_global_alias_assigns : Valid
+[wp] [Qed] Goal typed_global_no_alias_ensures : Valid
+[wp] [Qed] Goal typed_global_no_alias_assigns : Valid
+[wp] [Qed] Goal typed_set_alias_ensures : Valid
+[wp] [Qed] Goal typed_set_alias_ensures_2 : Valid
+[wp] [Qed] Goal typed_set_alias_assigns : Valid
+[wp] [Qed] Goal typed_union_alias_ensures : Valid
+[wp] [Qed] Goal typed_union_alias_ensures_2 : Valid
+[wp] [Qed] Goal typed_union_alias_assigns : Valid
+[wp] Proved goals:   30 / 30
+  Qed:            30
+------------------------------------------------------------
+ Functions                 WP     Alt-Ergo  Total   Success
+  global_alias              3        -        3       100%
+  global_no_alias           2        -        2       100%
+  formal_alias              3        -        3       100%
+  formal_no_alias           2        -        2       100%
+  formal_alias_array        5        -        5       100%
+  field_alias               3        -        3       100%
+  field_range_alias         3        -        3       100%
+  set_alias                 3        -        3       100%
+  comprehension_alias       3        -        3       100%
+  union_alias               3        -        3       100%
+------------------------------------------------------------
+[wp] Warning: Memory model hypotheses for function 'global_alias':
+  /*@
+     behavior typed:
+     requires \separated(g_alias,\union(&g_alias,global+(..)));
+     */
+  void global_alias(void);
+[wp] Warning: Memory model hypotheses for function 'global_no_alias':
+  /*@ behavior typed: requires \separated(g_alias,&g_alias); */
+  void global_no_alias(void);
+[wp] Warning: Memory model hypotheses for function 'formal_alias':
+  /*@
+     behavior typed:
+     requires \separated(global+(..),f_alias);
+     requires \separated(f_alias,global+(..));
+     */
+  void formal_alias(int *f_alias);
+[wp] Warning: Memory model hypotheses for function 'formal_alias_array':
+  /*@
+     behavior typed:
+     requires \separated(global+(..),alias_array+(..));
+     requires \separated(&(*alias_array)[0 .. 1],global+(..));
+     */
+  void formal_alias_array(int (*alias_array)[2]);
+[wp] Warning: Memory model hypotheses for function 'field_alias':
+  /*@
+     behavior typed:
+     requires \separated(global+(..),x);
+     requires \separated(&x->x,global+(..));
+     */
+  void field_alias(struct X *x);
+[wp] Warning: Memory model hypotheses for function 'field_range_alias':
+  /*@
+     behavior typed:
+     requires \separated(global+(..),x+(..));
+     requires \separated(&(x + (0 .. 3))->x,global+(..));
+     */
+  void field_range_alias(struct X *x);
+[wp] Warning: Memory model hypotheses for function 'set_alias':
+  /*@
+     behavior typed:
+     requires \separated(\union(global+(..),&g_alias),f_alias);
+     requires \separated({g_alias, f_alias},\union(&g_alias,global+(..)));
+     */
+  void set_alias(int *f_alias);
+[wp] Warning: Memory model hypotheses for function 'comprehension_alias':
+  /*@
+     behavior typed:
+     requires \separated({alias | int *alias; alias ≡ \at(g_alias,Pre)},
+                \union(&g_alias,global+(..)));
+     */
+  void comprehension_alias(void);
+[wp] Warning: Memory model hypotheses for function 'union_alias':
+  /*@
+     behavior typed:
+     requires \separated(\union(global+(..),&g_alias),f_alias);
+     requires \separated({g_alias, f_alias},\union(&g_alias,global+(..)));
+     */
+  void union_alias(int *f_alias);

src/plugins/wp/tests/wp_hoare/oracle_qualif/reference_and_struct.res.oracle

@@ -53,3 +53,6 @@
 [wp] Warning: Memory model hypotheses for function 'reset':
   /*@ behavior typed_ref: requires \valid(p); */
   void reset(struct T *p);
+[wp] Warning: Memory model hypotheses for function 'call_reset_5_tps':
+  /*@ behavior typed_ref: requires \separated(tps[9] + (0 .. 4),tps+(..)); */
+  void call_reset_5_tps(void);

src/plugins/wp/tests/wp_plugin/oracle/overassign.res.oracle

@@ -101,3 +101,9 @@ Assume { (* Heap *) Type: linked(Malloc_0). }
 Prove: invalid(Malloc_0, shift_sint32(global(G_A_32), -5), 10).
 
 ------------------------------------------------------------
+[wp] Warning: Memory model hypotheses for function 'f1_ok':
+  /*@ behavior typed: requires \separated(p + (0 .. 9),&p); */
+  void f1_ok(void);
+[wp] Warning: Memory model hypotheses for function 'f2_ok':
+  /*@ behavior typed: requires \separated(p + (10 .. 19),&p); */
+  void f2_ok(void);

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

@@ -28,3 +28,9 @@
   f5_ko                     -        -        2       0.0%
   f6_ko                     -        -        2       0.0%
 ------------------------------------------------------------
+[wp] Warning: Memory model hypotheses for function 'f1_ok':
+  /*@ behavior typed: requires \separated(p + (0 .. 9),&p); */
+  void f1_ok(void);
+[wp] Warning: Memory model hypotheses for function 'f2_ok':
+  /*@ behavior typed: requires \separated(p + (10 .. 19),&p); */
+  void f2_ok(void);

src/plugins/wp/tests/wp_typed/oracle/user_injector.res.oracle

@@ -121,5 +121,7 @@ Prove: true.
      behavior typed:
      requires \separated(\union(&seq,&service_cpt,service_id+(..),
                            service_result+(..)),error);
+     requires \separated(error,
+                \union(service_result+(..),service_id+(..),&service_cpt,&seq));
      */
   int job(int a, int b, int *error);

src/plugins/wp/tests/wp_typed/oracle_qualif/user_injector.0.res.oracle

@@ -35,5 +35,7 @@
      behavior typed:
      requires \separated(\union(&seq,&service_cpt,service_id+(..),
                            service_result+(..)),error);
+     requires \separated(error,
+                \union(service_result+(..),service_id+(..),&service_cpt,&seq));
      */
   int job(int a, int b, int *error);

src/plugins/wp/tests/wp_typed/oracle_qualif/user_injector.1.res.oracle

@@ -31,6 +31,8 @@
      behavior typed_ref:
      requires \separated(error,
                 \union(&seq,&service_cpt,service_id+(..),service_result+(..)));
+     requires \separated(error,
+                \union(service_result+(..),service_id+(..),&service_cpt,&seq));
      requires \valid(error);
      */
   int job(int a, int b, int *error);

src/plugins/wp/wp_parameters.ml

@@ -1040,6 +1040,10 @@ module MemoryContext =
       let help = "Warn Against Memory Model Hypotheses"
     end)
 
+let wkey_imprecise_hypotheses_assigns =
+  register_warn_category "hypotheses:assigns"
+let () = set_warn_status wkey_imprecise_hypotheses_assigns Log.Winactive
+
 let () = Parameter_customize.set_group wp_po
 module OutputDir =
   String(struct

src/plugins/wp/wp_parameters.mli

@@ -155,6 +155,8 @@ module SmokeDeadloop: Parameter_sig.Bool
 module SmokeDeadcode: Parameter_sig.Bool
 module SmokeDeadcall: Parameter_sig.Bool
 
+val wkey_imprecise_hypotheses_assigns: warn_category
+
 (** {2 Getters} *)
 
 val has_out : unit -> bool