From f71d1a0eeae7ba5396ec5ed0f7d1752693176f78 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Tue, 21 Jul 2020 15:24:17 +0200
Subject: [PATCH] [wp] Generate ACSL predicates for model hypotheses
---
src/plugins/wp/MemoryContext.ml | 288 +++++++++++-------
src/plugins/wp/MemoryContext.mli | 14 +-
src/plugins/wp/register.ml | 15 +-
.../wp_acsl/oracle/assigns_path.res.oracle | 3 +-
.../wp_acsl/oracle/chunk_typing.res.oracle | 11 +-
.../tests/wp_acsl/oracle/pointer.res.oracle | 6 +-
.../oracle_qualif/assigns_path.res.oracle | 3 +-
.../oracle_qualif/chunk_typing.res.oracle | 11 +-
.../oracle_qualif/pointer.0.res.oracle | 3 +-
.../oracle_qualif/pointer.1.res.oracle | 3 +-
.../wp/tests/wp_bts/oracle/bts0843.res.oracle | 3 +-
.../tests/wp_bts/oracle/bts_1828.0.res.oracle | 3 +-
.../tests/wp_bts/oracle/bts_1828.1.res.oracle | 6 +-
.../wp_bts/oracle_qualif/bts0843.res.oracle | 3 +-
.../oracle_qualif/bts_1828.0.res.oracle | 3 +-
.../oracle_qualif/bts_1828.1.res.oracle | 6 +-
.../oracle/frama_c_exo3_solved.old.res.oracle | 6 +-
.../frama_c_exo3_solved.old.v2.res.oracle | 6 +-
.../frama_c_exo3_solved.old.res.oracle | 12 +-
.../frama_c_exo3_solved.old.v2.res.oracle | 12 +-
.../alias_assigns_hypotheses.res.oracle | 39 +--
.../tests/wp_hoare/oracle/byref.1.res.oracle | 9 +-
.../wp_hoare/oracle/dispatch_var.res.oracle | 6 +-
.../oracle/dispatch_var2.0.res.oracle | 12 +-
.../oracle/dispatch_var2.1.res.oracle | 12 +-
.../wp_hoare/oracle/reference.res.oracle | 9 +-
.../oracle/reference_and_struct.res.oracle | 8 +-
.../oracle/reference_array.res.oracle | 8 +-
.../wp_hoare/oracle/refguards.res.oracle | 18 +-
.../alias_assigns_hypotheses.res.oracle | 39 +--
.../wp_hoare/oracle_qualif/byref.1.res.oracle | 9 +-
.../oracle_qualif/dispatch_var.res.oracle | 6 +-
.../oracle_qualif/dispatch_var2.0.res.oracle | 12 +-
.../oracle_qualif/dispatch_var2.1.res.oracle | 12 +-
.../oracle_qualif/reference.res.oracle | 9 +-
.../reference_and_struct.res.oracle | 8 +-
.../oracle_qualif/reference_array.res.oracle | 8 +-
.../oracle_qualif/refguards.res.oracle | 18 +-
.../tests/wp_plugin/oracle/dynamic.res.oracle | 12 +-
.../wp_plugin/oracle/overassign.res.oracle | 6 +-
.../wp/tests/wp_plugin/oracle/sep.res.oracle | 40 +--
.../wp_plugin/oracle/volatile.0.res.oracle | 3 +-
.../wp_plugin/oracle/volatile.1.res.oracle | 3 +-
.../oracle_qualif/dynamic.res.oracle | 12 +-
.../oracle_qualif/overassign.res.oracle | 6 +-
.../wp_typed/oracle/unit_ite.1.res.oracle | 3 +-
.../wp_typed/oracle/unit_labels.1.res.oracle | 6 +-
.../oracle/unit_loopscope.1.res.oracle | 3 +-
.../wp_typed/oracle/user_injector.res.oracle | 9 +-
.../wp_typed/oracle/user_swap.1.res.oracle | 6 +-
.../oracle_qualif/unit_loopscope.1.res.oracle | 3 +-
.../oracle_qualif/user_injector.0.res.oracle | 9 +-
.../oracle_qualif/user_injector.1.res.oracle | 16 +-
.../oracle_qualif/user_swap.1.res.oracle | 6 +-
.../tests/wp_usage/oracle/caveat.1.res.oracle | 18 +-
.../tests/wp_usage/oracle/caveat2.res.oracle | 6 +-
.../wp_usage/oracle/caveat_range.res.oracle | 3 +-
.../tests/wp_usage/oracle/global.1.res.oracle | 3 +-
.../tests/wp_usage/oracle/global.2.res.oracle | 4 +-
.../oracle/issue-189-bis.1.res.oracle | 6 +-
.../wp_usage/oracle/issue-189.2.res.oracle | 4 +-
.../wp_usage/oracle_qualif/caveat2.res.oracle | 6 +-
.../oracle_qualif/caveat_range.res.oracle | 3 +-
.../oracle_qualif/issue-189-bis.1.res.oracle | 6 +-
64 files changed, 518 insertions(+), 343 deletions(-)
diff --git a/src/plugins/wp/MemoryContext.ml b/src/plugins/wp/MemoryContext.ml
index b97d05a8b64..f0d8d79fed9 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 96707953d64..45dc45afbea 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 bb54e4da628..83a43cc7466 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 6d629988524..0c4bd8dfbdf 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 8f21ca532c0..72d6142a7ae 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 1737e32302f..76387c61d81 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 1c72369eadb..a2e6ef5f8fb 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 89b1b1b5b97..992ef461134 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 310d71f1258..e84a81d1246 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 ee3c703ca33..89712b41fe4 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 e99403ea348..d68634ce45e 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 0054a9afc53..66651f78d70 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 3949d8d5a74..6a0f4dd76d0 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 159f27542af..f2b4509858e 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 24788faf50d..ebe06ce52f4 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 f560c0a026a..b8015e5f58f 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 d0d68abc9ca..83c3ad493cf 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 8b40acb3f43..406c46f42e2 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 56be9acc1db..36e3c1f31d6 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 0d2cb66d920..04523680472 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 c9a461392e7..60d04236d9a 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 4720ded8277..051a94929b4 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 f9c9e2a5b35..bb48a4672be 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 b128329870f..72989020ece 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 9845add669a..181d3c1dad2 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 f5c773ac7bd..3eef87eaec3 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 502ee3eec09..b68225c3d9a 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 8cdc9f4d9d2..aba051f764c 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 25649f1ac96..615dc325426 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 f524e017b1a..c189e0e008e 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 fabfc588e61..0d4681981ee 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 0824c5c95dd..179a9259950 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 c472b2c06f3..f2b9868fd88 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 3996bedbab0..d23ba332da0 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 4ff3c1673ec..e4be92ac66b 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 d7fdaedb3bd..7f79d288a41 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 72ab30d0d2f..cc9487f8d96 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 b61a8f43c6a..82ba6e3fe6f 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 f61e601b4d2..6e4b15fb4d0 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 e522e771289..c0547370f6f 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 9d7b81db6f6..62a03745ae2 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 0c06a8becec..8f8e6a453d9 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 64cb1c39940..129e94d6af2 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 c38d5c4f213..a0f09e08be3 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 31cd7d9aaed..5222a717ce6 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 9976179a712..43877a40342 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 cba638b02bb..6759a580906 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 6413e9d7d32..62ec7355781 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 3dd0d642f58..a07757a5ff9 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 d4109c97637..c56fc78178c 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 58761bdefa3..7e327b11a78 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 510cdf0e651..1928fc98220 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 3f861815767..dbb2487bebb 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 ce020046acf..6f039f366e4 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 bf3ddd57997..99b18742b0c 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 e1c317646d5..234508ea4f7 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 514fab0cd9f..200b214f0cc 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 a6c3906898a..504e20e6bd6 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 33647c6dcb4..5d5c635c06b 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 f3a2767ec5c..967d775c75e 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 ec41c7f550d..5ce9a0dd10c 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 c46a68ad13b..e5abfd8d02a 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 cf2d2ab507e..d985f8cbec7 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 e063c170d22..d3fa8c4754e 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);
--
GitLab