diff --git a/src/plugins/wp/MemoryContext.ml b/src/plugins/wp/MemoryContext.ml
index b97d05a8b643a0d9183d41161244be33380f5b82..f0d8d79fed92265e4e5cc29f3af504532eaa8808 100644
--- a/src/plugins/wp/MemoryContext.ml
+++ b/src/plugins/wp/MemoryContext.ml
@@ -40,13 +40,11 @@ let pp_param fmt = function
(* -------------------------------------------------------------------------- *)
open Cil_types
-open Cil_datatype
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
type partition = {
globals : zone list ; (* [ &G , G[...], ... ] *)
@@ -55,106 +53,6 @@ type partition = {
assigned: identified_term list (* Must refer to pointed locations *)
}
-type clause = Valid of zone | Separated of zone list list
-
-(* -------------------------------------------------------------------------- *)
-
-let is_separated_true = function [] | [_] -> true | _ -> false
-
-(* -------------------------------------------------------------------------- *)
-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"
- | [z] -> pp_zone fmt z
- | z::zs ->
- Format.fprintf fmt "@[<hov 2>\\union(%a" pp_zone z ;
- List.iter (fun z -> Format.fprintf fmt ",@,%a" pp_zone z) zs ;
- Format.fprintf fmt ")@]"
-
-let pp_separation fmt = function
- | [] | [_] -> Format.pp_print_string fmt "\\true"
- | r::rs ->
- Format.fprintf fmt "@[<hov 2>\\separated(%a" pp_region r ;
- List.iter (fun r -> Format.fprintf fmt ",@,%a" pp_region r) rs ;
- Format.fprintf fmt ")@]"
-
-let pp_clause fmt = function
- | Separated sep -> Format.fprintf fmt "@ @[<hov 2>requires %a;@]" pp_separation sep
- | Valid zone -> Format.fprintf fmt "@ @[<hov 2>requires \\valid(%a);@]" pp_zone zone
-
-(* -------------------------------------------------------------------------- *)
-(* --- 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 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 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
- s @ v
-
(* -------------------------------------------------------------------------- *)
(* --- Partition --- *)
(* -------------------------------------------------------------------------- *)
@@ -205,3 +103,189 @@ let assigned t w =
{ w with assigned = assigned }
(* -------------------------------------------------------------------------- *)
+(* ANNOTS *)
+(* -------------------------------------------------------------------------- *)
+
+open Logic_const
+
+
+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 type_of_zone = function
+ | Ptr vi -> vi.vtype
+ | Var vi -> TPtr(vi.vtype, [])
+ | Arr vi when Cil.isPointerType vi.vtype -> vi.vtype
+ | Arr vi -> TPtr(Cil.typeOf_array_elem vi.vtype, [])
+
+let zone_to_term ?(to_char=false) loc zone =
+ let typ = Ctype (type_of_zone zone) in
+ let lval vi = TVar (Cil.cvar_to_lvar vi), TNoOffset in
+ let loc_range ptr =
+ if not to_char then ptr
+ else
+ let pointed =
+ match typ with
+ | (Ctype (TPtr (t, []))) -> t
+ | _ -> assert false (* typ has been generated by type_of_zone *)
+ in
+ let len = Logic_utils.expr_to_term (Cil.sizeOf ~loc pointed) in
+ let last = term (TBinOp(MinusA, len, tinteger ~loc 1)) len.term_type in
+ let range = trange ~loc (Some (tinteger ~loc 0), Some last) in
+ let ptr = Logic_utils.mk_cast ~loc Cil.charPtrType ptr in
+ term ~loc (TBinOp(PlusPI, ptr, range)) ptr.term_type
+ in
+ match zone with
+ | Var vi -> loc_range (term ~loc (TAddrOf(lval vi)) typ)
+ | Ptr vi -> loc_range (term ~loc (TLval(lval vi)) typ)
+ | Arr vi ->
+ let ptr =
+ if Cil.isArrayType vi.vtype
+ then term ~loc (TStartOf (lval vi)) typ
+ else term ~loc (TLval(lval vi)) typ
+ in
+ let ptr =
+ if not to_char then ptr
+ else Logic_utils.mk_cast ~loc Cil.charPtrType ptr
+ in
+ let range = trange ~loc (None, None) in
+ term ~loc (TBinOp(PlusPI, ptr, range)) ptr.term_type
+
+let region_to_term loc = function
+ | [] -> term ~loc Tempty_set (Ctype Cil.charPtrType)
+ | [z] -> zone_to_term loc z
+ | x :: tl as l ->
+ let fst = type_of_zone x in
+ let tl = List.map type_of_zone tl in
+ let to_char = not (List.for_all (Cil_datatype.Typ.equal fst) tl) in
+ let set_typ =
+ make_set_type (Ctype (if to_char then Cil.charPtrType else fst))
+ in
+ term ~loc (Tunion (List.map (zone_to_term ~to_char loc) l)) set_typ
+
+let separated_list ?loc = function
+ | [] | [ _ ] -> ptrue
+ | l -> pseparated ?loc l
+
+let separated_from_term loc assigned l =
+ separated_list ~loc (assigned :: List.map (region_to_term loc) l)
+
+let separated_from_addr loc assigned =
+ separated_from_term loc (addr_of_lval ~loc assigned.it_content)
+
+let valid_region loc r =
+ let t = region_to_term loc r in
+ pvalid ~loc (here_label, t)
+
+let global_zones partition =
+ List.map (fun z -> [z]) partition.globals
+
+let context_zones partition =
+ List.map (fun z -> [z]) partition.context
+
+let heap_zones partition =
+ let comp a b = Cil_datatype.Typ.compare (type_of_zone a) (type_of_zone b) in
+ List.sort comp partition.to_heap
+
+(* Note that this function does not return separated zone lists, but well-typed
+ zone lists.
+*)
+let heaps partition =
+ let rec partition_by_type t acc l =
+ match l, acc with
+ | [], _ ->
+ acc
+ | x :: l, [] ->
+ partition_by_type (type_of_zone x) [[x]] l
+ | x :: l, p :: acc' when Cil_datatype.Typ.equal t (type_of_zone x) ->
+ partition_by_type t ((x :: p) :: acc') l
+ | x :: l, acc ->
+ partition_by_type (type_of_zone x) ([x] :: acc) l
+ in
+ partition_by_type Cil.voidType [] (heap_zones partition)
+
+let main_separation loc globals context heaps =
+ match heaps, context with
+ | [], [] ->
+ (* In this case, separation is completely trivial *)
+ [ ptrue ]
+ | [], context ->
+ let zones = globals @ context in
+ [ separated_list ~loc (List.map (region_to_term loc) zones) ]
+ | heaps, context ->
+ let for_typed_heap h =
+ let zones = h :: globals @ context in
+ separated_list ~loc (List.map (region_to_term loc) zones)
+ in
+ List.map for_typed_heap heaps
+
+let clauses_of_partition loc p =
+ let globals = global_zones p in
+ let filter p = not (Logic_utils.is_trivially_true p) in
+ let main_sep =
+ main_separation loc globals (context_zones p) (heaps p)
+ in
+ let assigns_sep =
+ List.map (fun t -> separated_from_addr loc t globals) p.assigned
+ in
+ let context_validity =
+ List.map (valid_region loc) (context_zones p)
+ in
+ let reqs = main_sep @ assigns_sep @ context_validity in
+ let reqs = List.filter filter reqs in
+ let reqs = List.sort_uniq Logic_utils.compare_predicate reqs in
+ reqs, []
+
+let emitter =
+ Emitter.(create "Wp.Hypotheses" [Funspec] ~correctness:[] ~tuning:[])
+
+let get_behavior kf name partition =
+ let loc = Kernel_function.get_location kf in
+ let reqs,enss = clauses_of_partition loc partition in
+ let reqs = List.map Logic_const.new_predicate reqs in
+ let enss = List.map (fun p -> Normal, Logic_const.new_predicate p) enss in
+ match reqs,enss with
+ | [], [] -> None
+ | l1, l2 ->
+ Some {
+ b_name = name ;
+ b_requires = l1 ;
+ b_assumes = [] ;
+ b_post_cond = l2 ;
+ b_assigns = WritesAny ;
+ b_allocation = FreeAllocAny ;
+ b_extended = []
+ }
+
+let add_behavior kf name partition =
+ match get_behavior kf name partition with
+ | None -> ()
+ | Some bhv -> Annotations.add_behaviors emitter kf [bhv]
diff --git a/src/plugins/wp/MemoryContext.mli b/src/plugins/wp/MemoryContext.mli
index 96707953d647acacfa7c5e2a3faf8607aa52072e..45dc45afbea5c8020e85250c629b5a40aa6deea4 100644
--- a/src/plugins/wp/MemoryContext.mli
+++ b/src/plugins/wp/MemoryContext.mli
@@ -32,15 +32,5 @@ val empty : partition
val set : varinfo -> param -> partition -> partition
val assigned : identified_term -> partition -> partition
-type zone
-
-type clause =
- | Valid of zone
- | Separated of zone list list
-
-(** Build the separation clause from a partition,
- including the clauses related to the pointer validity *)
-val requires : partition -> clause list
-
-val pp_zone : Format.formatter -> zone -> unit
-val pp_clause : Format.formatter -> clause -> unit
+val add_behavior : kernel_function -> string -> partition -> unit
+val get_behavior : kernel_function -> string -> partition -> behavior option
diff --git a/src/plugins/wp/register.ml b/src/plugins/wp/register.ml
index bb54e4da62830925b1491204604eeed8fb21a66e..83a43cc7466ca4c15fa328dc64918301c4350c90 100644
--- a/src/plugins/wp/register.ml
+++ b/src/plugins/wp/register.ml
@@ -89,13 +89,11 @@ let wp_iter_model ?ip ?index job =
Fmap.iter (fun kf ms -> Models.iter (fun m -> job kf m) ms) !pool
end
-let wp_print_memory_context kf m hyp fmt =
+let wp_print_memory_context kf bhv fmt =
begin
let printer = new Printer.extensible_printer () in
let pp_vdecl = printer#without_annot printer#vdecl in
- Format.fprintf fmt
- "@[<hv 0>@[<hv 3>/*@@@ behavior %s:" (WpContext.MODEL.id m) ;
- List.iter (MemoryContext.pp_clause fmt) hyp ;
+ Format.fprintf fmt "@[<hv 0>@[<hv 3>/*@@@ %a" Cil_printer.pp_behavior bhv ;
let vkf = Kernel_function.get_vi kf in
Format.fprintf fmt "@ @]*/@]@\n@[<hov 2>%a;@]@\n"
pp_vdecl vkf ;
@@ -106,13 +104,16 @@ let wp_warn_memory_context () =
wp_iter_model
begin fun kf m ->
let partition = WpContext.compute_hypotheses m kf in
- let hyp = MemoryContext.requires partition in
- if hyp <> [] then
+ let model = WpContext.MODEL.id m in
+ let hyp = MemoryContext.get_behavior kf model partition in
+ match hyp with
+ | None -> ()
+ | Some bhv ->
Wp_parameters.warning
~current:false
"@[<hv 0>Memory model hypotheses for function '%s':@ %t@]"
(Kernel_function.get_name kf)
- (wp_print_memory_context kf m hyp)
+ (wp_print_memory_context kf bhv)
end
end
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/assigns_path.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/assigns_path.res.oracle
index 6d629988524ec0e2396fd74cb9392e73d645e99d..0c4bd8dfbdfced7b662260ad12ba7264848f940e 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/assigns_path.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/assigns_path.res.oracle
@@ -99,5 +99,6 @@ Prove: true.
------------------------------------------------------------
[wp] Warning: Memory model hypotheses for function 'job':
- /*@ behavior typed: requires \separated(&p,b+(..)); */
+ /*@ behavior typed:
+ requires \separated(b + (..), &p); */
void job(int n, int *b);
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/chunk_typing.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/chunk_typing.res.oracle
index 8f21ca532c0fe39f1713a5a780ff7e2cb2fa5f56..72d6142a7ae9a1b19088aa984720d20caba2956c 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/chunk_typing.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/chunk_typing.res.oracle
@@ -1879,9 +1879,14 @@ Prove: true.
[wp] Warning: Memory model hypotheses for function 'function':
/*@
behavior typed:
- requires \separated(x+(..),
- \union(i8+(..),u8+(..),i16+(..),u16+(..),i32+(..),u32+(..),
- i64+(..),u64+(..)));
+ requires \separated(i16 + (..), (char const *)x + (..));
+ requires \separated(i32 + (..), (char const *)x + (..));
+ requires \separated(i64 + (..), (char const *)x + (..));
+ requires \separated(i8 + (..), (char const *)x + (..));
+ requires \separated(u16 + (..), (char const *)x + (..));
+ requires \separated(u32 + (..), (char const *)x + (..));
+ requires \separated(u64 + (..), (char const *)x + (..));
+ requires \separated(u8 + (..), (char const *)x + (..));
*/
void function(signed char * /*[10]*/ i8, unsigned char * /*[10]*/ u8,
short * /*[10]*/ i16, unsigned short * /*[10]*/ u16,
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/pointer.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/pointer.res.oracle
index 1737e32302ff4c5e5d4697e084868bd3665b1c7c..76387c61d8110277aae032a327ba43d0482dcd2d 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/pointer.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/pointer.res.oracle
@@ -236,8 +236,10 @@ Prove: false.
------------------------------------------------------------
[wp] Warning: Memory model hypotheses for function 'compare':
- /*@ behavior typed: requires \separated(&p,q+(..)); */
+ /*@ behavior typed:
+ requires \separated(q + (..), &p); */
void compare(int *q);
[wp] Warning: Memory model hypotheses for function 'absurd':
- /*@ behavior typed: requires \separated(&p,q+(..)); */
+ /*@ behavior typed:
+ requires \separated(q + (..), &p); */
void absurd(int *q);
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigns_path.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigns_path.res.oracle
index 1c72369eadb0141c75c9fb022c8f36a4559cb1d7..a2e6ef5f8fb10702b95b325bc38065fbed816b49 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigns_path.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigns_path.res.oracle
@@ -21,5 +21,6 @@
job 6 3 9 100%
------------------------------------------------------------
[wp] Warning: Memory model hypotheses for function 'job':
- /*@ behavior typed: requires \separated(&p,b+(..)); */
+ /*@ behavior typed:
+ requires \separated(b + (..), &p); */
void job(int n, int *b);
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.res.oracle
index 89b1b1b5b973e603935151a80fee6115eeaa1b79..992ef461134cea13948c5dedbddc13f9a9586ca7 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.res.oracle
@@ -53,9 +53,14 @@
[wp] Warning: Memory model hypotheses for function 'function':
/*@
behavior typed:
- requires \separated(x+(..),
- \union(i8+(..),u8+(..),i16+(..),u16+(..),i32+(..),u32+(..),
- i64+(..),u64+(..)));
+ requires \separated(i16 + (..), (char const *)x + (..));
+ requires \separated(i32 + (..), (char const *)x + (..));
+ requires \separated(i64 + (..), (char const *)x + (..));
+ requires \separated(i8 + (..), (char const *)x + (..));
+ requires \separated(u16 + (..), (char const *)x + (..));
+ requires \separated(u32 + (..), (char const *)x + (..));
+ requires \separated(u64 + (..), (char const *)x + (..));
+ requires \separated(u8 + (..), (char const *)x + (..));
*/
void function(signed char * /*[10]*/ i8, unsigned char * /*[10]*/ u8,
short * /*[10]*/ i16, unsigned short * /*[10]*/ u16,
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/pointer.0.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/pointer.0.res.oracle
index 310d71f125800a7127da749babf9e34cea6597e5..e84a81d12463b0848c3ced81c696018af2e7c9ea 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/pointer.0.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/pointer.0.res.oracle
@@ -28,5 +28,6 @@
absurd - - 2 0.0%
------------------------------------------------------------
[wp] Warning: Memory model hypotheses for function 'absurd':
- /*@ behavior typed_ref: requires \separated(&p,q+(..)); */
+ /*@ behavior typed_ref:
+ requires \separated(q + (..), &p); */
void absurd(int *q);
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/pointer.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/pointer.1.res.oracle
index ee3c703ca332e470ac35ac0e4f6b09f71ac1fcb0..89712b41fe44ba795beedd5c8ff74aada4bbd6ae 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/pointer.1.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/pointer.1.res.oracle
@@ -28,5 +28,6 @@
absurd - - 2 0.0%
------------------------------------------------------------
[wp] Warning: Memory model hypotheses for function 'absurd':
- /*@ behavior typed: requires \separated(&p,q+(..)); */
+ /*@ behavior typed:
+ requires \separated(q + (..), &p); */
void absurd(int *q);
diff --git a/src/plugins/wp/tests/wp_bts/oracle/bts0843.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/bts0843.res.oracle
index e99403ea34806bd70ca1033b498affc24920dfb1..d68634ce45e42d1d6383e979b2802686f9f35e38 100644
--- a/src/plugins/wp/tests/wp_bts/oracle/bts0843.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle/bts0843.res.oracle
@@ -54,5 +54,6 @@ Prove: true.
------------------------------------------------------------
[wp] Warning: Memory model hypotheses for function 'f3':
- /*@ behavior typed: requires \separated(&p->a,&p); */
+ /*@ behavior typed:
+ requires \separated(&p->a, &p); */
void f3(void);
diff --git a/src/plugins/wp/tests/wp_bts/oracle/bts_1828.0.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/bts_1828.0.res.oracle
index 0054a9afc534ef9dabc91f05cfd5c7473c1f35d4..66651f78d70d24a450248991ff34bba6060340aa 100644
--- a/src/plugins/wp/tests/wp_bts/oracle/bts_1828.0.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle/bts_1828.0.res.oracle
@@ -67,5 +67,6 @@ Prove: global(L_two_24) != one_0.
------------------------------------------------------------
[wp] Warning: Memory model hypotheses for function 'global_frame':
- /*@ behavior typed: requires \separated(&zero,one); */
+ /*@ behavior typed:
+ requires \separated(one, &zero); */
void global_frame(int *one, int arg);
diff --git a/src/plugins/wp/tests/wp_bts/oracle/bts_1828.1.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/bts_1828.1.res.oracle
index 3949d8d5a746ef39ce761d4744be2896bfa2b93e..6a0f4dd76d0f8d11199c80eb863465e4dd91ea24 100644
--- a/src/plugins/wp/tests/wp_bts/oracle/bts_1828.1.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle/bts_1828.1.res.oracle
@@ -48,8 +48,8 @@ Prove: global(L_two_24) != one_0.
[wp] Warning: Memory model hypotheses for function 'global_frame':
/*@
behavior typed_ref:
- requires \separated(zero,one);
- requires \valid(zero);
- requires \valid(one);
+ requires \separated(one, zero);
+ requires \valid(one);
+ requires \valid(zero);
*/
void global_frame(int *one, int arg);
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts0843.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts0843.res.oracle
index 159f27542afda2730a180ae834b3358dee335bb2..f2b4509858e87d795d5087317472f3b6b6174b6a 100644
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts0843.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts0843.res.oracle
@@ -17,5 +17,6 @@
g3 1 2 3 100%
------------------------------------------------------------
[wp] Warning: Memory model hypotheses for function 'f3':
- /*@ behavior typed: requires \separated(&p->a,&p); */
+ /*@ behavior typed:
+ requires \separated(&p->a, &p); */
void f3(void);
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1828.0.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1828.0.res.oracle
index 24788faf50d022b02cd79a79e3d0022ec3ce87f9..ebe06ce52f4bf7f8adad0f4454e1b0f5ca738179 100644
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1828.0.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1828.0.res.oracle
@@ -19,5 +19,6 @@
global_frame 3 - 5 60.0%
------------------------------------------------------------
[wp] Warning: Memory model hypotheses for function 'global_frame':
- /*@ behavior typed: requires \separated(&zero,one); */
+ /*@ behavior typed:
+ requires \separated(one, &zero); */
void global_frame(int *one, int arg);
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1828.1.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1828.1.res.oracle
index f560c0a026a581f5e35e055a63f695517f83361c..b8015e5f58f65ce93725f6d6744252ed19bea9ce 100644
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1828.1.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1828.1.res.oracle
@@ -21,8 +21,8 @@
[wp] Warning: Memory model hypotheses for function 'global_frame':
/*@
behavior typed_ref:
- requires \separated(zero,one);
- requires \valid(zero);
- requires \valid(one);
+ requires \separated(one, zero);
+ requires \valid(one);
+ requires \valid(zero);
*/
void global_frame(int *one, int arg);
diff --git a/src/plugins/wp/tests/wp_gallery/oracle/frama_c_exo3_solved.old.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle/frama_c_exo3_solved.old.res.oracle
index d0d68abc9caadab4d4002d9a8bd206d5e529a233..83c3ad493cfc1a5e3131e07961343bbeb14d01fa 100644
--- a/src/plugins/wp/tests/wp_gallery/oracle/frama_c_exo3_solved.old.res.oracle
+++ b/src/plugins/wp/tests/wp_gallery/oracle/frama_c_exo3_solved.old.res.oracle
@@ -56,8 +56,8 @@
[wp] Warning: Memory model hypotheses for function 'equal_elements':
/*@
behavior typed_ref:
- requires \separated(v1,v2,a+(..));
- requires \valid(v1);
- requires \valid(v2);
+ requires \separated(a + (..), v2, v1);
+ requires \valid(v1);
+ requires \valid(v2);
*/
void equal_elements(int *a, int *v1, int *v2);
diff --git a/src/plugins/wp/tests/wp_gallery/oracle/frama_c_exo3_solved.old.v2.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle/frama_c_exo3_solved.old.v2.res.oracle
index 8b40acb3f436b766feb9fef4bb8d7b960945d098..406c46f42e2f796ad88072d3521434155a127894 100644
--- a/src/plugins/wp/tests/wp_gallery/oracle/frama_c_exo3_solved.old.v2.res.oracle
+++ b/src/plugins/wp/tests/wp_gallery/oracle/frama_c_exo3_solved.old.v2.res.oracle
@@ -57,8 +57,8 @@
[wp] Warning: Memory model hypotheses for function 'equal_elements':
/*@
behavior typed_ref:
- requires \separated(v1,v2,a+(..));
- requires \valid(v1);
- requires \valid(v2);
+ requires \separated(a + (..), v2, v1);
+ requires \valid(v1);
+ requires \valid(v2);
*/
void equal_elements(int *a, int *v1, int *v2);
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.res.oracle
index 56be9acc1dbb068d766b2e7c67dddfb01ae5a727..36e3c1f31d601958fd1d3f9360eeeb19f821fc04 100644
--- a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.res.oracle
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.res.oracle
@@ -48,9 +48,9 @@
[wp] Warning: Memory model hypotheses for function 'equal_elements':
/*@
behavior typed_ref:
- requires \separated(v1,v2,a+(..));
- requires \valid(v1);
- requires \valid(v2);
+ requires \separated(a + (..), v2, v1);
+ requires \valid(v1);
+ requires \valid(v2);
*/
void equal_elements(int *a, int *v1, int *v2);
[wp] Running WP plugin...
@@ -116,8 +116,8 @@
[wp] Warning: Memory model hypotheses for function 'equal_elements':
/*@
behavior typed_ref:
- requires \separated(v1,v2,a+(..));
- requires \valid(v1);
- requires \valid(v2);
+ requires \separated(a + (..), v2, v1);
+ requires \valid(v1);
+ requires \valid(v2);
*/
void equal_elements(int *a, int *v1, int *v2);
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.v2.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.v2.res.oracle
index 0d2cb66d920886acaab8d67242ea56cb9bd5b2f9..0452368047241e014d978d731182384e49884b7b 100644
--- a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.v2.res.oracle
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.v2.res.oracle
@@ -49,9 +49,9 @@
[wp] Warning: Memory model hypotheses for function 'equal_elements':
/*@
behavior typed_ref:
- requires \separated(v1,v2,a+(..));
- requires \valid(v1);
- requires \valid(v2);
+ requires \separated(a + (..), v2, v1);
+ requires \valid(v1);
+ requires \valid(v2);
*/
void equal_elements(int *a, int *v1, int *v2);
[wp] Running WP plugin...
@@ -118,8 +118,8 @@
[wp] Warning: Memory model hypotheses for function 'equal_elements':
/*@
behavior typed_ref:
- requires \separated(v1,v2,a+(..));
- requires \valid(v1);
- requires \valid(v2);
+ requires \separated(a + (..), v2, v1);
+ requires \valid(v1);
+ requires \valid(v2);
*/
void equal_elements(int *a, int *v1, int *v2);
diff --git a/src/plugins/wp/tests/wp_hoare/oracle/alias_assigns_hypotheses.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle/alias_assigns_hypotheses.res.oracle
index c9a461392e7cb29343481e9e0560a5021bf0beb2..60d04236d9a2c48f5ec6b80b0de6592c979b62f5 100644
--- a/src/plugins/wp/tests/wp_hoare/oracle/alias_assigns_hypotheses.res.oracle
+++ b/src/plugins/wp/tests/wp_hoare/oracle/alias_assigns_hypotheses.res.oracle
@@ -197,58 +197,59 @@ Prove: true.
[wp] Warning: Memory model hypotheses for function 'global_alias':
/*@
behavior typed:
- requires \separated(g_alias,\union(&g_alias,global+(..)));
+ requires \separated(g_alias, &g_alias, (int *)global + (..));
*/
void global_alias(void);
[wp] Warning: Memory model hypotheses for function 'global_no_alias':
- /*@ behavior typed: requires \separated(g_alias,&g_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+(..));
- */
+ /*@ behavior typed:
+ requires \separated(f_alias, (int *)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+(..));
+ requires \separated(&(*alias_array)[0 .. 1], (int *)global + (..));
+ requires \separated(alias_array + (..), (int *)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+(..));
+ requires \separated(&x->x, (int *)global + (..));
+ requires \separated(x, (int *)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+(..));
+ requires \separated(&(x + (0 .. 3))->x, (int *)global + (..));
+ requires \separated(x + (..), (int *)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+(..)));
+ requires \separated({g_alias, f_alias}, &g_alias, (int *)global + (..));
+ requires \separated(f_alias, &g_alias, (int *)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+(..)));
+ requires
+ \separated(
+ {alias | int *alias; alias ≡ \at(g_alias,Pre)}, &g_alias,
+ (int *)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+(..)));
+ requires \separated({g_alias, f_alias}, &g_alias, (int *)global + (..));
+ requires \separated(f_alias, &g_alias, (int *)global + (..));
*/
void union_alias(int *f_alias);
diff --git a/src/plugins/wp/tests/wp_hoare/oracle/byref.1.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle/byref.1.res.oracle
index 4720ded827794cf0a147a1cf332f7122fbcdda2f..051a94929b453b37ea0317b9496dcb85fd2c334c 100644
--- a/src/plugins/wp/tests/wp_hoare/oracle/byref.1.res.oracle
+++ b/src/plugins/wp/tests/wp_hoare/oracle/byref.1.res.oracle
@@ -87,11 +87,14 @@ Prove: true.
------------------------------------------------------------
[wp] Warning: Memory model hypotheses for function 'f':
- /*@ behavior typed_ref: requires \valid(r); */
+ /*@ behavior typed_ref:
+ requires \valid(r); */
void f(int *r);
[wp] Warning: Memory model hypotheses for function 'wrong_without_ref':
- /*@ behavior typed_ref: requires \valid(q); */
+ /*@ behavior typed_ref:
+ requires \valid(q); */
int wrong_without_ref(int *q);
[wp] Warning: Memory model hypotheses for function 'pointer':
- /*@ behavior typed_ref: requires \valid(q); */
+ /*@ behavior typed_ref:
+ requires \valid(q); */
int pointer(int *q);
diff --git a/src/plugins/wp/tests/wp_hoare/oracle/dispatch_var.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle/dispatch_var.res.oracle
index f9c9e2a5b35ffdd6194a574cde42c5a3620f522d..bb48a4672be4861c972fbcf9b7ba124c21dd3329 100644
--- a/src/plugins/wp/tests/wp_hoare/oracle/dispatch_var.res.oracle
+++ b/src/plugins/wp/tests/wp_hoare/oracle/dispatch_var.res.oracle
@@ -498,8 +498,10 @@ Prove: true.
------------------------------------------------------------
[wp] Warning: Memory model hypotheses for function 'ref_bd':
- /*@ behavior typed_ref: requires \valid(q); */
+ /*@ behavior typed_ref:
+ requires \valid(q); */
int ref_bd(int *q);
[wp] Warning: Memory model hypotheses for function 'g':
- /*@ behavior typed_ref: requires \valid(pg); */
+ /*@ behavior typed_ref:
+ requires \valid(pg); */
int g(int *pg);
diff --git a/src/plugins/wp/tests/wp_hoare/oracle/dispatch_var2.0.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle/dispatch_var2.0.res.oracle
index b128329870f278390c61503d8e3f1715cbc7695e..72989020ecec9747960fbc528524a8b097623523 100644
--- a/src/plugins/wp/tests/wp_hoare/oracle/dispatch_var2.0.res.oracle
+++ b/src/plugins/wp/tests/wp_hoare/oracle/dispatch_var2.0.res.oracle
@@ -464,14 +464,18 @@ Prove: true.
------------------------------------------------------------
[wp] Warning: Memory model hypotheses for function 'reset':
- /*@ behavior typed_ref: requires \valid(rp); */
+ /*@ behavior typed_ref:
+ requires \valid(rp); */
void reset(int *rp);
[wp] Warning: Memory model hypotheses for function 'incr':
- /*@ behavior typed_ref: requires \valid(ip); */
+ /*@ behavior typed_ref:
+ requires \valid(ip); */
void incr(int *ip);
[wp] Warning: Memory model hypotheses for function 'load':
- /*@ behavior typed_ref: requires \valid(lp); */
+ /*@ behavior typed_ref:
+ requires \valid(lp); */
int load(int *lp);
[wp] Warning: Memory model hypotheses for function 'call_param_ref':
- /*@ behavior typed_ref: requires \valid(q); */
+ /*@ behavior typed_ref:
+ requires \valid(q); */
int call_param_ref(int *q);
diff --git a/src/plugins/wp/tests/wp_hoare/oracle/dispatch_var2.1.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle/dispatch_var2.1.res.oracle
index 9845add669affa7de094d3deaa2df6b99eb3bdd4..181d3c1dad2dbe0491b867861f33163305f06fa5 100644
--- a/src/plugins/wp/tests/wp_hoare/oracle/dispatch_var2.1.res.oracle
+++ b/src/plugins/wp/tests/wp_hoare/oracle/dispatch_var2.1.res.oracle
@@ -212,14 +212,18 @@ Prove: true.
------------------------------------------------------------
[wp] Warning: Memory model hypotheses for function 'reset':
- /*@ behavior typed_ref: requires \valid(rp); */
+ /*@ behavior typed_ref:
+ requires \valid(rp); */
void reset(int *rp);
[wp] Warning: Memory model hypotheses for function 'incr':
- /*@ behavior typed_ref: requires \valid(ip); */
+ /*@ behavior typed_ref:
+ requires \valid(ip); */
void incr(int *ip);
[wp] Warning: Memory model hypotheses for function 'load':
- /*@ behavior typed_ref: requires \valid(lp); */
+ /*@ behavior typed_ref:
+ requires \valid(lp); */
int load(int *lp);
[wp] Warning: Memory model hypotheses for function 'call_param_ref':
- /*@ behavior typed_ref: requires \valid(q); */
+ /*@ behavior typed_ref:
+ requires \valid(q); */
int call_param_ref(int *q);
diff --git a/src/plugins/wp/tests/wp_hoare/oracle/reference.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle/reference.res.oracle
index f5c773ac7bd37ad8bbda40a9e46292e843806e23..3eef87eaec34b72a92be8b571d96c65ae88bad9e 100644
--- a/src/plugins/wp/tests/wp_hoare/oracle/reference.res.oracle
+++ b/src/plugins/wp/tests/wp_hoare/oracle/reference.res.oracle
@@ -143,11 +143,14 @@ Prove: true.
------------------------------------------------------------
[wp] Warning: Memory model hypotheses for function 'call_f2':
- /*@ behavior typed_ref: requires \valid(ptr); */
+ /*@ behavior typed_ref:
+ requires \valid(ptr); */
int call_f2(int *ptr, int y);
[wp] Warning: Memory model hypotheses for function 'call_global':
- /*@ behavior typed_ref: requires \valid(gl); */
+ /*@ behavior typed_ref:
+ requires \valid(gl); */
int call_global(void);
[wp] Warning: Memory model hypotheses for function 'write':
- /*@ behavior typed_ref: requires \valid(pa); */
+ /*@ behavior typed_ref:
+ requires \valid(pa); */
void write(int kb, int *pa);
diff --git a/src/plugins/wp/tests/wp_hoare/oracle/reference_and_struct.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle/reference_and_struct.res.oracle
index 502ee3eec09baebe1be54ef63f03d068f95b5ca0..b68225c3d9a4ed808c1aff57020093559ee9a1d2 100644
--- a/src/plugins/wp/tests/wp_hoare/oracle/reference_and_struct.res.oracle
+++ b/src/plugins/wp/tests/wp_hoare/oracle/reference_and_struct.res.oracle
@@ -253,8 +253,12 @@ Prove: true.
------------------------------------------------------------
[wp] Warning: Memory model hypotheses for function 'reset':
- /*@ behavior typed_ref: requires \valid(p); */
+ /*@ 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+(..)); */
+ /*@
+ behavior typed_ref:
+ requires \separated(tps[9] + (0 .. 4), (struct T **)tps + (..));
+ */
void call_reset_5_tps(void);
diff --git a/src/plugins/wp/tests/wp_hoare/oracle/reference_array.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle/reference_array.res.oracle
index 8cdc9f4d9d23e67d381f6cfc6d7affffcb8ad1c2..aba051f764c973108a81c2837ecffa832795710d 100644
--- a/src/plugins/wp/tests/wp_hoare/oracle/reference_array.res.oracle
+++ b/src/plugins/wp/tests/wp_hoare/oracle/reference_array.res.oracle
@@ -403,11 +403,15 @@ Prove: true.
------------------------------------------------------------
[wp] Warning: Memory model hypotheses for function 'load_1_5':
- /*@ behavior typed_ref: requires \separated(reg_load+(..),lp+(..)); */
+ /*@
+ behavior typed_ref:
+ requires \separated(lp + (..), (int *)reg_load + (..));
+ */
void load_1_5(int (*lp)[5]);
[wp] Warning: Memory model hypotheses for function 'add_1_5':
/*@
behavior typed_ref:
- requires \separated(\union(reg_load+(..),reg_add+(..)),ap+(..));
+ requires
+ \separated(ap + (..), (int *)reg_add + (..), (int *)reg_load + (..));
*/
void add_1_5(int (*ap)[5]);
diff --git a/src/plugins/wp/tests/wp_hoare/oracle/refguards.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle/refguards.res.oracle
index 25649f1ac968befd3f1858a7d2ba9d75962cf1fb..615dc3254262084acb538ce9500a8b32bcf76c6b 100644
--- a/src/plugins/wp/tests/wp_hoare/oracle/refguards.res.oracle
+++ b/src/plugins/wp/tests/wp_hoare/oracle/refguards.res.oracle
@@ -72,24 +72,24 @@ Prove: d != c.
[wp] Warning: Memory model hypotheses for function 'f':
/*@
behavior typed_ref:
- requires \separated(c,d,\union(a+(..),b+(..)));
- requires \valid(c);
- requires \valid(d);
+ requires \separated({a + (..), b + (..)}, d, c);
+ requires \valid(c);
+ requires \valid(d);
*/
void f(int *a, int *b, int *c, int *d, int k);
[wp] Warning: Memory model hypotheses for function 'h':
/*@
behavior typed_ref:
- requires \separated(c,d);
- requires \valid(c);
- requires \valid(d);
+ requires \separated(d, c);
+ requires \valid(c);
+ requires \valid(d);
*/
void h(int *c, int *d, int k);
[wp] Warning: Memory model hypotheses for function 's':
/*@
behavior typed_ref:
- requires \separated(c,d);
- requires \valid(c);
- requires \valid(d);
+ requires \separated(d, c);
+ requires \valid(c);
+ requires \valid(d);
*/
void s(int **c, int **d, int k);
diff --git a/src/plugins/wp/tests/wp_hoare/oracle_qualif/alias_assigns_hypotheses.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle_qualif/alias_assigns_hypotheses.res.oracle
index f524e017b1a1a3e6e4d9b95948c4b50947b67ff9..c189e0e008e622fecb804884743ceb6957539a0b 100644
--- a/src/plugins/wp/tests/wp_hoare/oracle_qualif/alias_assigns_hypotheses.res.oracle
+++ b/src/plugins/wp/tests/wp_hoare/oracle_qualif/alias_assigns_hypotheses.res.oracle
@@ -52,58 +52,59 @@
[wp] Warning: Memory model hypotheses for function 'global_alias':
/*@
behavior typed:
- requires \separated(g_alias,\union(&g_alias,global+(..)));
+ requires \separated(g_alias, &g_alias, (int *)global + (..));
*/
void global_alias(void);
[wp] Warning: Memory model hypotheses for function 'global_no_alias':
- /*@ behavior typed: requires \separated(g_alias,&g_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+(..));
- */
+ /*@ behavior typed:
+ requires \separated(f_alias, (int *)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+(..));
+ requires \separated(&(*alias_array)[0 .. 1], (int *)global + (..));
+ requires \separated(alias_array + (..), (int *)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+(..));
+ requires \separated(&x->x, (int *)global + (..));
+ requires \separated(x, (int *)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+(..));
+ requires \separated(&(x + (0 .. 3))->x, (int *)global + (..));
+ requires \separated(x + (..), (int *)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+(..)));
+ requires \separated({g_alias, f_alias}, &g_alias, (int *)global + (..));
+ requires \separated(f_alias, &g_alias, (int *)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+(..)));
+ requires
+ \separated(
+ {alias | int *alias; alias ≡ \at(g_alias,Pre)}, &g_alias,
+ (int *)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+(..)));
+ requires \separated({g_alias, f_alias}, &g_alias, (int *)global + (..));
+ requires \separated(f_alias, &g_alias, (int *)global + (..));
*/
void union_alias(int *f_alias);
diff --git a/src/plugins/wp/tests/wp_hoare/oracle_qualif/byref.1.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle_qualif/byref.1.res.oracle
index fabfc588e61698f7b7f50002bf66e59b6cde1fad..0d4681981ee83417394762d0437fc01738433cc2 100644
--- a/src/plugins/wp/tests/wp_hoare/oracle_qualif/byref.1.res.oracle
+++ b/src/plugins/wp/tests/wp_hoare/oracle_qualif/byref.1.res.oracle
@@ -28,11 +28,14 @@
global 2 - 2 100%
------------------------------------------------------------
[wp] Warning: Memory model hypotheses for function 'f':
- /*@ behavior typed_ref: requires \valid(r); */
+ /*@ behavior typed_ref:
+ requires \valid(r); */
void f(int *r);
[wp] Warning: Memory model hypotheses for function 'wrong_without_ref':
- /*@ behavior typed_ref: requires \valid(q); */
+ /*@ behavior typed_ref:
+ requires \valid(q); */
int wrong_without_ref(int *q);
[wp] Warning: Memory model hypotheses for function 'pointer':
- /*@ behavior typed_ref: requires \valid(q); */
+ /*@ behavior typed_ref:
+ requires \valid(q); */
int pointer(int *q);
diff --git a/src/plugins/wp/tests/wp_hoare/oracle_qualif/dispatch_var.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle_qualif/dispatch_var.res.oracle
index 0824c5c95dd32122016dcc53c980a5f21e6f38fe..179a92599507e1a11c4c79687ba0b471c8ef2c52 100644
--- a/src/plugins/wp/tests/wp_hoare/oracle_qualif/dispatch_var.res.oracle
+++ b/src/plugins/wp/tests/wp_hoare/oracle_qualif/dispatch_var.res.oracle
@@ -101,8 +101,10 @@
array_in_struct_param 2 - 2 100%
------------------------------------------------------------
[wp] Warning: Memory model hypotheses for function 'ref_bd':
- /*@ behavior typed_ref: requires \valid(q); */
+ /*@ behavior typed_ref:
+ requires \valid(q); */
int ref_bd(int *q);
[wp] Warning: Memory model hypotheses for function 'g':
- /*@ behavior typed_ref: requires \valid(pg); */
+ /*@ behavior typed_ref:
+ requires \valid(pg); */
int g(int *pg);
diff --git a/src/plugins/wp/tests/wp_hoare/oracle_qualif/dispatch_var2.0.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle_qualif/dispatch_var2.0.res.oracle
index c472b2c06f3347455cd43b7941e613ac1558a80e..f2b9868fd88e56ba518ff919dae5f869d6f55307 100644
--- a/src/plugins/wp/tests/wp_hoare/oracle_qualif/dispatch_var2.0.res.oracle
+++ b/src/plugins/wp/tests/wp_hoare/oracle_qualif/dispatch_var2.0.res.oracle
@@ -51,14 +51,18 @@
call_param_ref 6 - 6 100%
------------------------------------------------------------
[wp] Warning: Memory model hypotheses for function 'reset':
- /*@ behavior typed_ref: requires \valid(rp); */
+ /*@ behavior typed_ref:
+ requires \valid(rp); */
void reset(int *rp);
[wp] Warning: Memory model hypotheses for function 'incr':
- /*@ behavior typed_ref: requires \valid(ip); */
+ /*@ behavior typed_ref:
+ requires \valid(ip); */
void incr(int *ip);
[wp] Warning: Memory model hypotheses for function 'load':
- /*@ behavior typed_ref: requires \valid(lp); */
+ /*@ behavior typed_ref:
+ requires \valid(lp); */
int load(int *lp);
[wp] Warning: Memory model hypotheses for function 'call_param_ref':
- /*@ behavior typed_ref: requires \valid(q); */
+ /*@ behavior typed_ref:
+ requires \valid(q); */
int call_param_ref(int *q);
diff --git a/src/plugins/wp/tests/wp_hoare/oracle_qualif/dispatch_var2.1.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle_qualif/dispatch_var2.1.res.oracle
index 3996bedbab0c49a1ef56b6ee221173adfd897428..d23ba332da0642c03ac334a848c66f419b8ef0ea 100644
--- a/src/plugins/wp/tests/wp_hoare/oracle_qualif/dispatch_var2.1.res.oracle
+++ b/src/plugins/wp/tests/wp_hoare/oracle_qualif/dispatch_var2.1.res.oracle
@@ -51,14 +51,18 @@
call_param_ref 6 - 6 100%
------------------------------------------------------------
[wp] Warning: Memory model hypotheses for function 'reset':
- /*@ behavior typed_ref: requires \valid(rp); */
+ /*@ behavior typed_ref:
+ requires \valid(rp); */
void reset(int *rp);
[wp] Warning: Memory model hypotheses for function 'incr':
- /*@ behavior typed_ref: requires \valid(ip); */
+ /*@ behavior typed_ref:
+ requires \valid(ip); */
void incr(int *ip);
[wp] Warning: Memory model hypotheses for function 'load':
- /*@ behavior typed_ref: requires \valid(lp); */
+ /*@ behavior typed_ref:
+ requires \valid(lp); */
int load(int *lp);
[wp] Warning: Memory model hypotheses for function 'call_param_ref':
- /*@ behavior typed_ref: requires \valid(q); */
+ /*@ behavior typed_ref:
+ requires \valid(q); */
int call_param_ref(int *q);
diff --git a/src/plugins/wp/tests/wp_hoare/oracle_qualif/reference.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle_qualif/reference.res.oracle
index 4ff3c1673ecaaf07a95846a27e9b3c0e78eab007..e4be92ac66b9066968792697b0dbc7a0ae389d0a 100644
--- a/src/plugins/wp/tests/wp_hoare/oracle_qualif/reference.res.oracle
+++ b/src/plugins/wp/tests/wp_hoare/oracle_qualif/reference.res.oracle
@@ -38,11 +38,14 @@
write 2 - 2 100%
------------------------------------------------------------
[wp] Warning: Memory model hypotheses for function 'call_f2':
- /*@ behavior typed_ref: requires \valid(ptr); */
+ /*@ behavior typed_ref:
+ requires \valid(ptr); */
int call_f2(int *ptr, int y);
[wp] Warning: Memory model hypotheses for function 'call_global':
- /*@ behavior typed_ref: requires \valid(gl); */
+ /*@ behavior typed_ref:
+ requires \valid(gl); */
int call_global(void);
[wp] Warning: Memory model hypotheses for function 'write':
- /*@ behavior typed_ref: requires \valid(pa); */
+ /*@ behavior typed_ref:
+ requires \valid(pa); */
void write(int kb, int *pa);
diff --git a/src/plugins/wp/tests/wp_hoare/oracle_qualif/reference_and_struct.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle_qualif/reference_and_struct.res.oracle
index d7fdaedb3bd8fcae019af39eefb28e9861c7175a..7f79d288a41728995d7839894ab6efbf79d9c765 100644
--- a/src/plugins/wp/tests/wp_hoare/oracle_qualif/reference_and_struct.res.oracle
+++ b/src/plugins/wp/tests/wp_hoare/oracle_qualif/reference_and_struct.res.oracle
@@ -51,8 +51,12 @@
call_array_in_struct_param 5 - 5 100%
------------------------------------------------------------
[wp] Warning: Memory model hypotheses for function 'reset':
- /*@ behavior typed_ref: requires \valid(p); */
+ /*@ 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+(..)); */
+ /*@
+ behavior typed_ref:
+ requires \separated(tps[9] + (0 .. 4), (struct T **)tps + (..));
+ */
void call_reset_5_tps(void);
diff --git a/src/plugins/wp/tests/wp_hoare/oracle_qualif/reference_array.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle_qualif/reference_array.res.oracle
index 72ab30d0d2f37fddb5c97a37a325cc0e5d441a49..cc9487f8d96988c74b747d72a8b83a316f3afd55 100644
--- a/src/plugins/wp/tests/wp_hoare/oracle_qualif/reference_array.res.oracle
+++ b/src/plugins/wp/tests/wp_hoare/oracle_qualif/reference_array.res.oracle
@@ -53,11 +53,15 @@
calls_on_array_dim_2 5 3 8 100%
------------------------------------------------------------
[wp] Warning: Memory model hypotheses for function 'load_1_5':
- /*@ behavior typed_ref: requires \separated(reg_load+(..),lp+(..)); */
+ /*@
+ behavior typed_ref:
+ requires \separated(lp + (..), (int *)reg_load + (..));
+ */
void load_1_5(int (*lp)[5]);
[wp] Warning: Memory model hypotheses for function 'add_1_5':
/*@
behavior typed_ref:
- requires \separated(\union(reg_load+(..),reg_add+(..)),ap+(..));
+ requires
+ \separated(ap + (..), (int *)reg_add + (..), (int *)reg_load + (..));
*/
void add_1_5(int (*ap)[5]);
diff --git a/src/plugins/wp/tests/wp_hoare/oracle_qualif/refguards.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle_qualif/refguards.res.oracle
index b61a8f43c6af24e470d75344f190a40f41b4e534..82ba6e3fe6fe6e65f7e318bc97987d47325ebd56 100644
--- a/src/plugins/wp/tests/wp_hoare/oracle_qualif/refguards.res.oracle
+++ b/src/plugins/wp/tests/wp_hoare/oracle_qualif/refguards.res.oracle
@@ -26,24 +26,24 @@
[wp] Warning: Memory model hypotheses for function 'f':
/*@
behavior typed_ref:
- requires \separated(c,d,\union(a+(..),b+(..)));
- requires \valid(c);
- requires \valid(d);
+ requires \separated({a + (..), b + (..)}, d, c);
+ requires \valid(c);
+ requires \valid(d);
*/
void f(int *a, int *b, int *c, int *d, int k);
[wp] Warning: Memory model hypotheses for function 'h':
/*@
behavior typed_ref:
- requires \separated(c,d);
- requires \valid(c);
- requires \valid(d);
+ requires \separated(d, c);
+ requires \valid(c);
+ requires \valid(d);
*/
void h(int *c, int *d, int k);
[wp] Warning: Memory model hypotheses for function 's':
/*@
behavior typed_ref:
- requires \separated(c,d);
- requires \valid(c);
- requires \valid(d);
+ requires \separated(d, c);
+ requires \valid(c);
+ requires \valid(d);
*/
void s(int **c, int **d, int k);
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/dynamic.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/dynamic.res.oracle
index f61e601b4d210a4a8afbea9a51402de2d1d963f1..6e4b15fb4d0a29aad67e97dc0a87dcddf8d33714 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/dynamic.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/dynamic.res.oracle
@@ -374,14 +374,18 @@ Prove: true.
------------------------------------------------------------
[wp] Warning: Memory model hypotheses for function 'guarded_call':
- /*@ behavior typed: requires \separated(&X,p); */
+ /*@ behavior typed:
+ requires \separated(p, &X); */
void guarded_call(struct S *p);
[wp] Warning: Memory model hypotheses for function 'behavior':
- /*@ behavior typed: requires \separated(&X1,p+(..)); */
+ /*@ behavior typed:
+ requires \separated(p + (..), &X1); */
int behavior(int (*p)(void));
[wp] Warning: Memory model hypotheses for function 'some_behaviors':
- /*@ behavior typed: requires \separated(&X1,p+(..)); */
+ /*@ behavior typed:
+ requires \separated(p + (..), &X1); */
int some_behaviors(int (*p)(void));
[wp] Warning: Memory model hypotheses for function 'missing_context':
- /*@ behavior typed: requires \separated(&X1,p); */
+ /*@ behavior typed:
+ requires \separated(p, &X1); */
int missing_context(int (*p)(void));
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/overassign.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/overassign.res.oracle
index e522e7712891c7631d77bf7400632795b3bfd77d..c0547370f6fd1fd42458c7e2d7542f96ea29c8b0 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/overassign.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/overassign.res.oracle
@@ -102,8 +102,10 @@ 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); */
+ /*@ 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); */
+ /*@ behavior typed:
+ requires \separated(p + (10 .. 19), &p); */
void f2_ok(void);
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/sep.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/sep.res.oracle
index 9d7b81db6f6d44f2464af7aa0fc0575ebf7eea30..62a03745ae24323360affa779b605b010999835d 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/sep.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/sep.res.oracle
@@ -68,51 +68,51 @@ Prove: true.
------------------------------------------------------------
[wp] Warning: Memory model hypotheses for function 'f2_p_a':
- /*@ behavior typed_caveat: requires \separated(p,&a); requires \valid(p); */
+ /*@ behavior typed_caveat:
+ requires \separated(&a, p);
+ requires \valid(p); */
void f2_p_a(int *p);
[wp] Warning: Memory model hypotheses for function 'f3_p_ab':
- /*@
- behavior typed_caveat:
- requires \separated(p,\union(&a,&b));
- requires \valid(p);
- */
+ /*@ behavior typed_caveat:
+ requires \separated(&b, &a, p);
+ requires \valid(p); */
void f3_p_ab(int *p);
[wp] Warning: Memory model hypotheses for function 'f4_pq_ab':
/*@
behavior typed_caveat:
- requires \separated(p,q,\union(&a,&b));
- requires \valid(p);
- requires \valid(q);
+ requires \separated(&b, &a, q, p);
+ requires \valid(p);
+ requires \valid(q);
*/
void f4_pq_ab(int *p, int *q);
[wp] Warning: Memory model hypotheses for function 'f5_pq':
/*@
behavior typed_caveat:
- requires \separated(p,q);
- requires \valid(p);
- requires \valid(q);
+ requires \separated(q, p);
+ requires \valid(p);
+ requires \valid(q);
*/
void f5_pq(int *p, int *q);
[wp] Warning: Memory model hypotheses for function 'f6_Pa':
/*@
behavior typed_caveat:
- requires \separated(p+(..),&a);
- requires \valid(p+(..));
+ requires \separated(&a, p + (..));
+ requires \valid(p + (..));
*/
void f6_Pa(int *p, int k);
[wp] Warning: Memory model hypotheses for function 'f7_pq_ad':
/*@
behavior typed_caveat:
- requires \separated(p,q,\union(&a,&d));
- requires \valid(p);
- requires \valid(q);
+ requires \separated(&d, &a, q, p);
+ requires \valid(p);
+ requires \valid(q);
*/
void f7_pq_ad(int *p, int *q);
[wp] Warning: Memory model hypotheses for function 'f8_pq_a':
/*@
behavior typed_caveat:
- requires \separated(p,q,&a);
- requires \valid(p);
- requires \valid(q);
+ requires \separated(&a, q, p);
+ requires \valid(p);
+ requires \valid(q);
*/
void f8_pq_a(int *p, int *q);
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/volatile.0.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/volatile.0.res.oracle
index 0c06a8becec85b905f2f501ec5d78ba93f9bd10c..8f8e6a453d9cb4d2e03ce0fdbad93c78c450de4d 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/volatile.0.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/volatile.0.res.oracle
@@ -37,5 +37,6 @@ Prove: EqS1_st_v(w, w_1).
------------------------------------------------------------
[wp] Warning: Memory model hypotheses for function 'job_struct_assigns':
- /*@ behavior typed: requires \separated(&sv,p); */
+ /*@ behavior typed:
+ requires \separated(p, &sv); */
void job_struct_assigns(struct st_v *p);
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/volatile.1.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/volatile.1.res.oracle
index 64cb1c399406456ed9e2ae41d46887120ed47026..129e94d6af2a3561d291ac217db596b83db08246 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/volatile.1.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/volatile.1.res.oracle
@@ -71,5 +71,6 @@ Prove: true.
------------------------------------------------------------
[wp] Warning: Memory model hypotheses for function 'job_struct_assigns':
- /*@ behavior typed: requires \separated(&sv,p); */
+ /*@ behavior typed:
+ requires \separated(p, &sv); */
void job_struct_assigns(struct st_v *p);
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/dynamic.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/dynamic.res.oracle
index c38d5c4f2132bec412e28f4880848457b2f7b423..a0f09e08be3c8acf22540e19f8ea9cf9d7298c7b 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/dynamic.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/dynamic.res.oracle
@@ -69,14 +69,18 @@
no_call 4 - 4 100%
------------------------------------------------------------
[wp] Warning: Memory model hypotheses for function 'guarded_call':
- /*@ behavior typed: requires \separated(&X,p); */
+ /*@ behavior typed:
+ requires \separated(p, &X); */
void guarded_call(struct S *p);
[wp] Warning: Memory model hypotheses for function 'behavior':
- /*@ behavior typed: requires \separated(&X1,p+(..)); */
+ /*@ behavior typed:
+ requires \separated(p + (..), &X1); */
int behavior(int (*p)(void));
[wp] Warning: Memory model hypotheses for function 'some_behaviors':
- /*@ behavior typed: requires \separated(&X1,p+(..)); */
+ /*@ behavior typed:
+ requires \separated(p + (..), &X1); */
int some_behaviors(int (*p)(void));
[wp] Warning: Memory model hypotheses for function 'missing_context':
- /*@ behavior typed: requires \separated(&X1,p); */
+ /*@ behavior typed:
+ requires \separated(p, &X1); */
int missing_context(int (*p)(void));
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/overassign.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/overassign.res.oracle
index 31cd7d9aaed823f36c18a8b88ca63c9e18e61f40..5222a717ce69ab4c9583dd47bf8802e0cb09858c 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/overassign.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/overassign.res.oracle
@@ -29,8 +29,10 @@
f6_ko - - 2 0.0%
------------------------------------------------------------
[wp] Warning: Memory model hypotheses for function 'f1_ok':
- /*@ behavior typed: requires \separated(p + (0 .. 9),&p); */
+ /*@ 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); */
+ /*@ behavior typed:
+ requires \separated(p + (10 .. 19), &p); */
void f2_ok(void);
diff --git a/src/plugins/wp/tests/wp_typed/oracle/unit_ite.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/unit_ite.1.res.oracle
index 9976179a7121da8220bd6193dba9b4a47b1af624..43877a403428fbd5a0e8f4b71f516edf1102e3aa 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/unit_ite.1.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/unit_ite.1.res.oracle
@@ -12,5 +12,6 @@ Prove: true.
------------------------------------------------------------
[wp] Warning: Memory model hypotheses for function 'check':
- /*@ behavior typed_ref: requires \valid(p); */
+ /*@ behavior typed_ref:
+ requires \valid(p); */
void check(int x, int *p);
diff --git a/src/plugins/wp/tests/wp_typed/oracle/unit_labels.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/unit_labels.1.res.oracle
index cba638b02bb8c53145c8fb5181adf1fbdf1982b4..6759a580906bcb3c00bfd186e95f828ee34e92a7 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/unit_labels.1.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/unit_labels.1.res.oracle
@@ -30,8 +30,8 @@ Prove: true.
[wp] Warning: Memory model hypotheses for function 'duplet':
/*@
behavior typed_ref:
- requires \separated(pi,pj,a+(..));
- requires \valid(pi);
- requires \valid(pj);
+ requires \separated(a + (..), pj, pi);
+ requires \valid(pi);
+ requires \valid(pj);
*/
void duplet(int *a, int *pi, int *pj);
diff --git a/src/plugins/wp/tests/wp_typed/oracle/unit_loopscope.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/unit_loopscope.1.res.oracle
index 6413e9d7d3206f7ff6ac1464b9378c04dac005ce..62ec7355781e8b95e3a43a8d9f9c5a6bf5c14416 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/unit_loopscope.1.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/unit_loopscope.1.res.oracle
@@ -19,5 +19,6 @@ Prove: false.
------------------------------------------------------------
[wp] Warning: Memory model hypotheses for function 'f':
- /*@ behavior typed_ref: requires \valid(written); */
+ /*@ behavior typed_ref:
+ requires \valid(written); */
void f(unsigned int *written);
diff --git a/src/plugins/wp/tests/wp_typed/oracle/user_injector.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/user_injector.res.oracle
index 3dd0d642f5857395c7b9903264ace65995998a7c..a07757a5ff942b50e56944a40b1d00ca715240b7 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/user_injector.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/user_injector.res.oracle
@@ -119,9 +119,10 @@ Prove: true.
[wp] Warning: Memory model hypotheses for function 'job':
/*@
behavior typed:
- requires \separated(\union(&seq,&service_cpt,service_id+(..),
- service_result+(..)),error);
- requires \separated(error,
- \union(service_result+(..),service_id+(..),&service_cpt,&seq));
+ requires
+ \separated(
+ error, (int *)service_result + (..), (int *)service_id + (..),
+ &service_cpt, &seq
+ );
*/
int job(int a, int b, int *error);
diff --git a/src/plugins/wp/tests/wp_typed/oracle/user_swap.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/user_swap.1.res.oracle
index d4109c976370521d7cc76a28e3f8f96a325a377e..c56fc78178c50807b4ed644139ec1d2a7ae4737d 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/user_swap.1.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/user_swap.1.res.oracle
@@ -44,8 +44,8 @@ Prove: true.
[wp] Warning: Memory model hypotheses for function 'swap':
/*@
behavior typed_ref:
- requires \separated(a,b);
- requires \valid(a);
- requires \valid(b);
+ requires \separated(b, a);
+ requires \valid(a);
+ requires \valid(b);
*/
void swap(int *a, int *b);
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_loopscope.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_loopscope.1.res.oracle
index 58761bdefa349443b64e729fa5e64f3ed17f288f..7e327b11a789f998a2e487876f530db99f3c476a 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_loopscope.1.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_loopscope.1.res.oracle
@@ -16,5 +16,6 @@
f 1 - 2 50.0%
------------------------------------------------------------
[wp] Warning: Memory model hypotheses for function 'f':
- /*@ behavior typed_ref: requires \valid(written); */
+ /*@ behavior typed_ref:
+ requires \valid(written); */
void f(unsigned int *written);
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_injector.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_injector.0.res.oracle
index 510cdf0e6515a3942cc18cdd34f16d5a71cdb40c..1928fc98220abc5021dbaacf7f624dc769aa08e1 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_injector.0.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_injector.0.res.oracle
@@ -33,9 +33,10 @@
[wp] Warning: Memory model hypotheses for function 'job':
/*@
behavior typed:
- requires \separated(\union(&seq,&service_cpt,service_id+(..),
- service_result+(..)),error);
- requires \separated(error,
- \union(service_result+(..),service_id+(..),&service_cpt,&seq));
+ requires
+ \separated(
+ error, (int *)service_result + (..), (int *)service_id + (..),
+ &service_cpt, &seq
+ );
*/
int job(int a, int b, int *error);
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_injector.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_injector.1.res.oracle
index 3f86181576795e8489a9f758ae342a2559a5301f..dbb2487bebbd74591dec9a919c67e11a771a55b6 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_injector.1.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_injector.1.res.oracle
@@ -29,10 +29,16 @@
[wp] Warning: Memory model hypotheses for function 'job':
/*@
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);
+ requires
+ \separated(
+ (int *)service_result + (..), (int *)service_id + (..),
+ &service_cpt, &seq, error
+ );
+ requires
+ \separated(
+ error, (int *)service_result + (..), (int *)service_id + (..),
+ &service_cpt, &seq
+ );
+ requires \valid(error);
*/
int job(int a, int b, int *error);
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_swap.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_swap.1.res.oracle
index ce020046acf9048667a7c9075e093f25b91b240e..6f039f366e4de88733fe8be43f46a2fa01f052a7 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_swap.1.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_swap.1.res.oracle
@@ -20,8 +20,8 @@
[wp] Warning: Memory model hypotheses for function 'swap':
/*@
behavior typed_ref:
- requires \separated(a,b);
- requires \valid(a);
- requires \valid(b);
+ requires \separated(b, a);
+ requires \valid(a);
+ requires \valid(b);
*/
void swap(int *a, int *b);
diff --git a/src/plugins/wp/tests/wp_usage/oracle/caveat.1.res.oracle b/src/plugins/wp/tests/wp_usage/oracle/caveat.1.res.oracle
index bf3ddd5799774b1ac136def68852e3a87dd4d78e..99b18742b0ce42dcf50c680a4d704947e679b992 100644
--- a/src/plugins/wp/tests/wp_usage/oracle/caveat.1.res.oracle
+++ b/src/plugins/wp/tests/wp_usage/oracle/caveat.1.res.oracle
@@ -72,24 +72,24 @@ Prove: P_OBS(x_2, x_3, x_4).
[wp] Warning: Memory model hypotheses for function 'implicit':
/*@
behavior typed_caveat:
- requires \separated(a,r);
- requires \valid(a);
- requires \valid(r);
+ requires \separated(r, a);
+ requires \valid(a);
+ requires \valid(r);
*/
void implicit(struct S *a, int *r);
[wp] Warning: Memory model hypotheses for function 'explicit':
/*@
behavior typed_caveat:
- requires \separated(a,r);
- requires \valid(a);
- requires \valid(r);
+ requires \separated(r, a);
+ requires \valid(a);
+ requires \valid(r);
*/
void explicit(struct S *a, int *r);
[wp] Warning: Memory model hypotheses for function 'observer':
/*@
behavior typed_caveat:
- requires \separated(a,r);
- requires \valid(a);
- requires \valid(r);
+ requires \separated(r, a);
+ requires \valid(a);
+ requires \valid(r);
*/
void observer(struct S *a, int *r);
diff --git a/src/plugins/wp/tests/wp_usage/oracle/caveat2.res.oracle b/src/plugins/wp/tests/wp_usage/oracle/caveat2.res.oracle
index e1c317646d5c3668adc48bea4aed56cf81a2b64c..234508ea4f734905e15977f9d2696735782f27b5 100644
--- a/src/plugins/wp/tests/wp_usage/oracle/caveat2.res.oracle
+++ b/src/plugins/wp/tests/wp_usage/oracle/caveat2.res.oracle
@@ -101,8 +101,8 @@ Prove: true.
[wp] Warning: Memory model hypotheses for function 'job':
/*@
behavior typed_caveat:
- requires \separated(p,b+(..));
- requires \valid(p);
- requires \valid(b+(..));
+ requires \separated(b + (..), p);
+ requires \valid(b + (..));
+ requires \valid(p);
*/
void job(struct S *p, int n, int *b);
diff --git a/src/plugins/wp/tests/wp_usage/oracle/caveat_range.res.oracle b/src/plugins/wp/tests/wp_usage/oracle/caveat_range.res.oracle
index 514fab0cd9fcf83dc2cd37d5a5ff18e1057c975c..200b214f0ccfe0b3cc9a7e5f43a23baa60d71afa 100644
--- a/src/plugins/wp/tests/wp_usage/oracle/caveat_range.res.oracle
+++ b/src/plugins/wp/tests/wp_usage/oracle/caveat_range.res.oracle
@@ -156,5 +156,6 @@ Prove: true.
------------------------------------------------------------
[wp] Warning: Memory model hypotheses for function 'reset':
- /*@ behavior typed_caveat: requires \valid(p+(..)); */
+ /*@ behavior typed_caveat:
+ requires \valid(p + (..)); */
void reset(struct S *p);
diff --git a/src/plugins/wp/tests/wp_usage/oracle/global.1.res.oracle b/src/plugins/wp/tests/wp_usage/oracle/global.1.res.oracle
index a6c3906898ab2a46097521bb629c95a4baea45c2..504e20e6bd6202c3bf8cfb5b05d9ee181c31efb3 100644
--- a/src/plugins/wp/tests/wp_usage/oracle/global.1.res.oracle
+++ b/src/plugins/wp/tests/wp_usage/oracle/global.1.res.oracle
@@ -21,5 +21,6 @@ Prove: true.
------------------------------------------------------------
[wp] Warning: Memory model hypotheses for function 'foo':
- /*@ behavior typed: requires \separated(&GLOBAL,a); */
+ /*@ behavior typed:
+ requires \separated(a, &GLOBAL); */
void foo(int *a);
diff --git a/src/plugins/wp/tests/wp_usage/oracle/global.2.res.oracle b/src/plugins/wp/tests/wp_usage/oracle/global.2.res.oracle
index 33647c6dcb46b2e1befed2cb567b45d93b8caea2..5d5c635c06b555c2b2717dd33b44fa0d7aa12e51 100644
--- a/src/plugins/wp/tests/wp_usage/oracle/global.2.res.oracle
+++ b/src/plugins/wp/tests/wp_usage/oracle/global.2.res.oracle
@@ -21,5 +21,7 @@ Prove: true.
------------------------------------------------------------
[wp] Warning: Memory model hypotheses for function 'foo':
- /*@ behavior typed_ref: requires \separated(a,&GLOBAL); requires \valid(a); */
+ /*@ behavior typed_ref:
+ requires \separated(&GLOBAL, a);
+ requires \valid(a); */
void foo(int *a);
diff --git a/src/plugins/wp/tests/wp_usage/oracle/issue-189-bis.1.res.oracle b/src/plugins/wp/tests/wp_usage/oracle/issue-189-bis.1.res.oracle
index f3a2767ec5c1975e6ce6eb91bc438810cf292e40..967d775c75e0b4c041e6d445983b911483b80f60 100644
--- a/src/plugins/wp/tests/wp_usage/oracle/issue-189-bis.1.res.oracle
+++ b/src/plugins/wp/tests/wp_usage/oracle/issue-189-bis.1.res.oracle
@@ -171,8 +171,8 @@ Prove: true.
[wp] Warning: Memory model hypotheses for function 'memcpy_context_vars':
/*@
behavior typed:
- requires \separated(src,dst);
- requires \valid(src);
- requires \valid(dst);
+ requires \separated(dst, src);
+ requires \valid(dst);
+ requires \valid(src);
*/
void memcpy_context_vars(unsigned char *src, unsigned char *dst, int len);
diff --git a/src/plugins/wp/tests/wp_usage/oracle/issue-189.2.res.oracle b/src/plugins/wp/tests/wp_usage/oracle/issue-189.2.res.oracle
index ec41c7f550d2d54273da0404d0e7bc613adf0a0d..5ce9a0dd10cada654d1d8f18025ebf09c6bbdb23 100644
--- a/src/plugins/wp/tests/wp_usage/oracle/issue-189.2.res.oracle
+++ b/src/plugins/wp/tests/wp_usage/oracle/issue-189.2.res.oracle
@@ -26,7 +26,7 @@ Prove: true.
[wp] Warning: Memory model hypotheses for function 'f':
/*@
behavior typed_caveat:
- requires \separated(ptr,src);
- requires \valid(ptr);
+ requires \separated(src, ptr);
+ requires \valid(ptr);
*/
void f(char *ptr, char const *src, unsigned int idx);
diff --git a/src/plugins/wp/tests/wp_usage/oracle_qualif/caveat2.res.oracle b/src/plugins/wp/tests/wp_usage/oracle_qualif/caveat2.res.oracle
index c46a68ad13b89baae4c0d141b923caf8a188ee10..e5abfd8d02a9863e9e553f665cf5e186647ab75c 100644
--- a/src/plugins/wp/tests/wp_usage/oracle_qualif/caveat2.res.oracle
+++ b/src/plugins/wp/tests/wp_usage/oracle_qualif/caveat2.res.oracle
@@ -24,8 +24,8 @@
[wp] Warning: Memory model hypotheses for function 'job':
/*@
behavior typed_caveat:
- requires \separated(p,b+(..));
- requires \valid(p);
- requires \valid(b+(..));
+ requires \separated(b + (..), p);
+ requires \valid(b + (..));
+ requires \valid(p);
*/
void job(struct S *p, int n, int *b);
diff --git a/src/plugins/wp/tests/wp_usage/oracle_qualif/caveat_range.res.oracle b/src/plugins/wp/tests/wp_usage/oracle_qualif/caveat_range.res.oracle
index cf2d2ab507e212d9026a3324ba1963b03dba4607..d985f8cbec7862bbf1d917c194ff5c9b438f2403 100644
--- a/src/plugins/wp/tests/wp_usage/oracle_qualif/caveat_range.res.oracle
+++ b/src/plugins/wp/tests/wp_usage/oracle_qualif/caveat_range.res.oracle
@@ -24,5 +24,6 @@
reset 7 5 12 100%
------------------------------------------------------------
[wp] Warning: Memory model hypotheses for function 'reset':
- /*@ behavior typed_caveat: requires \valid(p+(..)); */
+ /*@ behavior typed_caveat:
+ requires \valid(p + (..)); */
void reset(struct S *p);
diff --git a/src/plugins/wp/tests/wp_usage/oracle_qualif/issue-189-bis.1.res.oracle b/src/plugins/wp/tests/wp_usage/oracle_qualif/issue-189-bis.1.res.oracle
index e063c170d221248677920e5087360ea1b8fc5798..d3fa8c4754e5781ab40c05a476169ff82ffe5fa0 100644
--- a/src/plugins/wp/tests/wp_usage/oracle_qualif/issue-189-bis.1.res.oracle
+++ b/src/plugins/wp/tests/wp_usage/oracle_qualif/issue-189-bis.1.res.oracle
@@ -24,8 +24,8 @@
[wp] Warning: Memory model hypotheses for function 'memcpy_context_vars':
/*@
behavior typed:
- requires \separated(src,dst);
- requires \valid(src);
- requires \valid(dst);
+ requires \separated(dst, src);
+ requires \valid(dst);
+ requires \valid(src);
*/
void memcpy_context_vars(unsigned char *src, unsigned char *dst, int len);