From 9744d2ad095815188b15e064c213ceb89c59834e Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Mon, 18 Jan 2021 17:54:13 +0100
Subject: [PATCH] [wp] Fixes block_length for opaque structs
---
src/plugins/wp/Cvalues.ml | 43 +++++-
src/plugins/wp/Cvalues.mli | 2 +
src/plugins/wp/Definitions.ml | 22 +--
src/plugins/wp/MemTyped.ml | 19 ++-
src/plugins/wp/MemVar.ml | 20 +--
src/plugins/wp/tests/wp_acsl/opaque_struct.i | 40 ++++--
.../wp_acsl/oracle/opaque_struct.res.oracle | 129 ++++++++++++++++--
.../oracle_qualif/opaque_struct.res.oracle | 49 +++++--
8 files changed, 264 insertions(+), 60 deletions(-)
diff --git a/src/plugins/wp/Cvalues.ml b/src/plugins/wp/Cvalues.ml
index fc6c98b97e2..df578509530 100644
--- a/src/plugins/wp/Cvalues.ml
+++ b/src/plugins/wp/Cvalues.ml
@@ -70,7 +70,10 @@ and constant_term t =
| TConst c -> logic_constant c
| _ -> Warning.error "constant(%a)" Printer.pp_term t
-(* Initialization values *)
+(* -------------------------------------------------------------------------- *)
+(* --- Initialization values --- *)
+(* -------------------------------------------------------------------------- *)
+
module OPAQUE_COMP_INIT = struct
type initialization_funs = {
init: lfun ;
@@ -130,6 +133,44 @@ and init_comp_value value ci =
let initialized_obj = init_value e_true
let uninitialized_obj = init_value e_false
+(* -------------------------------------------------------------------------- *)
+(* --- Length of empty compinfos --- *)
+(* -------------------------------------------------------------------------- *)
+
+module OPAQUE_COMP_BYTES_LENGTH = WpContext.Generator(Cil_datatype.Compinfo)
+ (struct
+ let name = "Cvalues.EmptyCompBytesLength"
+ type key = compinfo
+ type data = lfun
+ let compile c =
+ if c.cfields <> None then
+ Wp_parameters.fatal
+ "Asking for opaque struct length on non opaque struct" ;
+ let result = Lang.t_int in
+ let name = "BytesLength" in
+ let size =
+ Lang.(generated_f ~params:[] ~result "%s_of_%s" name (comp_id c))
+ in
+ (* Registration *)
+ Definitions.define_symbol {
+ d_cluster = Definitions.compinfo c ;
+ d_lfun = size ; d_types = 0 ; d_params = [] ;
+ d_definition = Logic result ;
+ } ;
+ let min_size = if Cil.acceptEmptyCompinfo () then e_zero else e_one in
+ Definitions.define_lemma {
+ l_kind = `Axiom ;
+ l_name = "Positive_" ^ name ^ "_of_" ^ Lang.comp_id c ;
+ l_types = 0 ; l_triggers = [] ; l_forall = [] ;
+ l_cluster = Definitions.compinfo c ;
+ l_lemma = Lang.F.(p_leq min_size (e_fun size []))
+ } ;
+ size
+ end)
+
+let bytes_length_of_opaque_comp c =
+ Lang.F.e_fun (OPAQUE_COMP_BYTES_LENGTH.get c) []
+
(* -------------------------------------------------------------------------- *)
(* The type contains C-integers *)
diff --git a/src/plugins/wp/Cvalues.mli b/src/plugins/wp/Cvalues.mli
index 6c113daf413..85276cb8315 100644
--- a/src/plugins/wp/Cvalues.mli
+++ b/src/plugins/wp/Cvalues.mli
@@ -102,6 +102,8 @@ val constant_term : Cil_types.term -> term
val initialized_obj: c_object -> term
val uninitialized_obj: c_object -> term
+val bytes_length_of_opaque_comp: compinfo -> term
+
(** {2 Lifting Operations over Memory Values} *)
val map_sloc : ('a -> 'b) -> 'a Sigs.sloc -> 'b Sigs.sloc
diff --git a/src/plugins/wp/Definitions.ml b/src/plugins/wp/Definitions.ml
index cf21f0f5bb1..b8bd00cd0e6 100644
--- a/src/plugins/wp/Definitions.ml
+++ b/src/plugins/wp/Definitions.ml
@@ -336,11 +336,12 @@ class virtual visitor main =
let c = compinfo r in
if self#do_local c then
begin
- let fts = Option.map (List.map
- (fun f ->
- let t = Lang.tau_of_ctype f.ftype in
- self#vtau t ; Cfield (f, KValue) , t
- ))
+ let fts = Option.map
+ (List.map
+ (fun f ->
+ let t = Lang.tau_of_ctype f.ftype in
+ self#vtau t ; Cfield (f, KValue) , t
+ ))
r.cfields
in self#on_comp r fts ;
end
@@ -353,11 +354,12 @@ class virtual visitor main =
let c = icompinfo r in
if self#do_local c then
begin
- let fts = Option.map (List.map
- (fun f ->
- let t = Lang.init_of_ctype f.ftype in
- self#vtau t ; Cfield (f, KInit) , t
- ))
+ let fts = Option.map
+ (List.map
+ (fun f ->
+ let t = Lang.init_of_ctype f.ftype in
+ self#vtau t ; Cfield (f, KInit) , t
+ ))
r.cfields
in self#on_icomp r fts ;
end
diff --git a/src/plugins/wp/MemTyped.ml b/src/plugins/wp/MemTyped.ml
index 7671a4f03d7..34b939f685f 100644
--- a/src/plugins/wp/MemTyped.ml
+++ b/src/plugins/wp/MemTyped.ml
@@ -220,18 +220,19 @@ and all_value_chunks () =
let init_footprint _ _ = Heap.Set.singleton T_init
let value_footprint obj _l = footprint obj
-module OPAQUE_COMP_SIZE = WpContext.Generator(Cil_datatype.Compinfo)
+(* Note that it is the length in MemTyped and not the occupied bytes *)
+module OPAQUE_COMP_LENGTH = WpContext.Generator(Cil_datatype.Compinfo)
(struct
- let name = "MemTyped.EmptyCompSize"
+ let name = "MemTyped.EmptyCompLength"
type key = compinfo
type data = lfun
let compile c =
if c.cfields <> None then
Wp_parameters.fatal
- "Asking for opaque struct size on non opaque struct" ;
+ "Asking for opaque struct length on non opaque struct" ;
let result = Lang.t_int in
let size =
- Lang.generated_f ~params:[] ~result "%s" ("Size_of_" ^ Lang.comp_id c)
+ Lang.generated_f ~params:[] ~result "Length_of_%s" (Lang.comp_id c)
in
(* Registration *)
Definitions.define_symbol {
@@ -241,7 +242,7 @@ module OPAQUE_COMP_SIZE = WpContext.Generator(Cil_datatype.Compinfo)
} ;
Definitions.define_lemma {
l_kind = `Axiom ;
- l_name = "Positive_Size_of_" ^ Lang.comp_id c ;
+ l_name = "Positive_Length_of_" ^ Lang.comp_id c ;
l_types = 0 ; l_triggers = [] ; l_forall = [] ;
l_cluster = Definitions.compinfo c ;
l_lemma = Lang.F.(p_lt e_zero (e_fun size []))
@@ -266,7 +267,7 @@ and length_of_field f = length_of_typ f.ftype
and length_of_comp c =
match c.cfields with
| None ->
- Lang.F.e_fun (OPAQUE_COMP_SIZE.get c) []
+ Lang.F.e_fun (OPAQUE_COMP_LENGTH.get c) []
| Some fields ->
(* union field are considered as struct field *)
e_sum (List.map length_of_field fields)
@@ -644,7 +645,11 @@ let allocated sigma l = F.e_get (Sigma.value sigma T_alloc) (a_base l)
let base_addr l = a_addr (a_base l) e_zero
let base_offset l = a_base_offset (a_base l) (a_offset l)
let block_length sigma obj l =
- e_fact (Ctypes.sizeof_object obj) (allocated sigma l)
+ match obj with
+ | C_comp ({ cfields = None } as c) ->
+ e_mul (Cvalues.bytes_length_of_opaque_comp c) (allocated sigma l)
+ | _ ->
+ e_fact (Ctypes.sizeof_object obj) (allocated sigma l)
(* -------------------------------------------------------------------------- *)
(* --- Cast --- *)
diff --git a/src/plugins/wp/MemVar.ml b/src/plugins/wp/MemVar.ml
index 4d4b5c1c850..ddaef66c490 100644
--- a/src/plugins/wp/MemVar.ml
+++ b/src/plugins/wp/MemVar.ml
@@ -683,14 +683,18 @@ struct
| Loc l -> M.block_length sigma.mem obj l
| Ref x -> noref ~op:"block-length of" x
| Val(m,x,_) ->
- let obj = Ctypes.object_of (vtype m x) in
- let size =
- if Ctypes.sizeof_defined obj
- then Ctypes.sizeof_object obj
- else if Wp_parameters.ExternArrays.get ()
- then max_int
- else Warning.error ~source:"MemVar" "Unknown array-size"
- in F.e_int size
+ begin match Ctypes.object_of (vtype m x) with
+ | C_comp ({ cfields = None } as c) ->
+ Cvalues.bytes_length_of_opaque_comp c
+ | obj ->
+ let size =
+ if Ctypes.sizeof_defined obj
+ then Ctypes.sizeof_object obj
+ else if Wp_parameters.ExternArrays.get ()
+ then max_int
+ else Warning.error ~source:"MemVar" "Unknown array-size"
+ in F.e_int size
+ end
let cast obj l = Loc(M.cast obj (mloc_of_loc l))
let loc_of_int e a = Loc(M.loc_of_int e a)
diff --git a/src/plugins/wp/tests/wp_acsl/opaque_struct.i b/src/plugins/wp/tests/wp_acsl/opaque_struct.i
index 5be55cbc018..208ef861206 100644
--- a/src/plugins/wp/tests/wp_acsl/opaque_struct.i
+++ b/src/plugins/wp/tests/wp_acsl/opaque_struct.i
@@ -4,8 +4,9 @@ extern struct S S1;
extern struct S S2;
/*@ axiomatic test{
- @ check lemma should_fail : S1 == S2;
- @ check lemma should_succeed : S1 == S1;
+ @ check lemma fail: S1 == S2;
+ @ check lemma succeed_L1: S1 == S1;
+ @ check lemma succeed_L2: \block_length(&S1) >= 0;
}*/
/*@ assigns S1; */
@@ -13,8 +14,8 @@ void f(void);
void assigns(void){
f();
- /*@ check should_fail: S1 == \at(S1,Pre);*/
- /*@ check should_succeed: S2 == \at(S2,Pre);*/
+ //@ check fail: S1 == \at(S1,Pre);
+ //@ check succeed: S2 == \at(S2,Pre);
}
struct S* p ;
@@ -22,10 +23,17 @@ struct S* p ;
//@ assigns *p ;
void g(void);
-/*@ requires \initialized(p); */
+/*@ requires \initialized(p);
+ requires \valid(p);
+*/
void initialized_assigns(void){
g();
- //@ check should_succeed: \initialized(p);
+ //@ check succeed: \initialized(p);
+ //@ check succeed: \block_length(p) >= 0;
+
+ // while it can be proved in Coq, this is currently
+ // too indirect for solvers.
+ // @ check succeed: \block_length(p) >= \block_length(&S1);
}
/*@ requires ! \initialized(p); */
@@ -36,6 +44,22 @@ void uninitialized_assigns(void){
- it is still uninitialized,
- it has been initialized.
*/
- //@ check should_fail: ! \initialized(p);
- //@ check should_fail: \initialized(p);
+ //@ check fail: ! \initialized(p);
+ //@ check fail: \initialized(p);
+}
+
+void assigned_via_pointer(void){
+ g();
+ //@ check fail: \at(*p, Here) == \at(*p, Pre);
+}
+
+//@ assigns *a ;
+void assign(struct S *a);
+
+//@ requires \separated(a, c);
+void assigns_effect(int* p, float* q, char* c, struct S *a){
+ assign(a);
+ //@ check fail: *p == \at(*p, Pre);
+ //@ check fail: *q == \at(*q, Pre);
+ //@ check succeed: *c == \at(*c, Pre);
}
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/opaque_struct.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/opaque_struct.res.oracle
index a8efa3e97f1..28a1c218766 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/opaque_struct.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/opaque_struct.res.oracle
@@ -6,51 +6,139 @@
Axiomatic 'test'
------------------------------------------------------------
-Lemma should_fail:
+Lemma fail:
Prove: (EqS1_S S1_0 S2_0)
------------------------------------------------------------
-Lemma should_succeed:
+Lemma succeed_L1:
Prove: true
+------------------------------------------------------------
+
+Lemma succeed_L2:
+Prove: 0<=BytesLength_of_S1_S
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function assigned_via_pointer
+------------------------------------------------------------
+
+Goal Check 'fail' (file tests/wp_acsl/opaque_struct.i, line 53):
+Assume {
+ (* Heap *)
+ Type: (region(p.base) <= 0) /\ framed(Mptr_0) /\ sconst(Mchar_0).
+}
+Prove: EqS1_S(Load_S1_S(p, havoc(Mchar_undef_0, Mchar_0, p, Length_of_S1_S),
+ havoc(Mint_undef_0, Mint_0, p, Length_of_S1_S),
+ havoc(Mint_undef_1, Mint_1, p, Length_of_S1_S),
+ havoc(Mint_undef_2, Mint_2, p, Length_of_S1_S),
+ havoc(Mint_undef_3, Mint_3, p, Length_of_S1_S),
+ havoc(Mint_undef_4, Mint_4, p, Length_of_S1_S),
+ havoc(Mint_undef_5, Mint_5, p, Length_of_S1_S),
+ havoc(Mint_undef_6, Mint_6, p, Length_of_S1_S),
+ havoc(Mint_undef_7, Mint_7, p, Length_of_S1_S),
+ havoc(Mint_undef_8, Mint_8, p, Length_of_S1_S),
+ havoc(Mf32_undef_0, Mf32_0, p, Length_of_S1_S),
+ havoc(Mf64_undef_0, Mf64_0, p, Length_of_S1_S),
+ havoc(Mptr_undef_0, Mptr_0, p, Length_of_S1_S)),
+ Load_S1_S(p, Mchar_0, Mint_0, Mint_1, Mint_2, Mint_3, Mint_4,
+ Mint_5, Mint_6, Mint_7, Mint_8, Mf32_0, Mf64_0, Mptr_0)).
+
------------------------------------------------------------
------------------------------------------------------------
Function assigns
------------------------------------------------------------
-Goal Check 'should_fail' (file tests/wp_acsl/opaque_struct.i, line 16):
+Goal Check 'fail' (file tests/wp_acsl/opaque_struct.i, line 17):
Prove: EqS1_S(S1_0, S1_1).
------------------------------------------------------------
-Goal Check 'should_succeed' (file tests/wp_acsl/opaque_struct.i, line 17):
+Goal Check 'succeed' (file tests/wp_acsl/opaque_struct.i, line 18):
Prove: true.
+------------------------------------------------------------
+------------------------------------------------------------
+ Function assigns_effect
+------------------------------------------------------------
+
+Goal Check 'fail' (file tests/wp_acsl/opaque_struct.i, line 62):
+Let x = Mint_0[p].
+Let a_1 = havoc(Mint_undef_0, Mint_0, a, Length_of_S1_S)[p].
+Assume {
+ Type: is_sint32(x) /\ is_sint32(a_1).
+ (* Heap *)
+ Type: (region(a.base) <= 0) /\ (region(c.base) <= 0) /\
+ (region(p.base) <= 0).
+ (* Pre-condition *)
+ Have: separated(a, Length_of_S1_S, c, 1).
+}
+Prove: a_1 = x.
+
+------------------------------------------------------------
+
+Goal Check 'fail' (file tests/wp_acsl/opaque_struct.i, line 63):
+Assume {
+ (* Heap *)
+ Type: (region(a.base) <= 0) /\ (region(c.base) <= 0) /\
+ (region(q.base) <= 0).
+ (* Pre-condition *)
+ Have: separated(a, Length_of_S1_S, c, 1).
+}
+Prove: of_f32(havoc(Mf32_undef_0, Mf32_0, a, Length_of_S1_S)[q])
+ = of_f32(Mf32_0[q]).
+
+------------------------------------------------------------
+
+Goal Check 'succeed' (file tests/wp_acsl/opaque_struct.i, line 64):
+Let x = Mchar_0[c].
+Let a_1 = havoc(Mchar_undef_0, Mchar_0, a, Length_of_S1_S)[c].
+Assume {
+ Type: is_sint8(x) /\ is_sint8(a_1).
+ (* Heap *)
+ Type: (region(a.base) <= 0) /\ (region(c.base) <= 0) /\ sconst(Mchar_0).
+ (* Pre-condition *)
+ Have: separated(a, Length_of_S1_S, c, 1).
+}
+Prove: a_1 = x.
+
------------------------------------------------------------
------------------------------------------------------------
Function initialized_assigns
------------------------------------------------------------
-Goal Check 'should_succeed' (file tests/wp_acsl/opaque_struct.i, line 28):
-Let a = havoc(Init_undef_0, Init_0, p, Size_of_S1_S).
+Goal Check 'succeed' (file tests/wp_acsl/opaque_struct.i, line 31):
+Let a = havoc(Init_undef_0, Init_0, p, Length_of_S1_S).
Assume {
(* Heap *)
- Type: (region(p.base) <= 0) /\ cinits(Init_0).
+ Type: (region(p.base) <= 0) /\ linked(Malloc_0) /\ cinits(Init_0).
(* Pre-condition *)
- Have: IsInit_S1_S(p, Init_0).
+ Have: IsInit_S1_S(p, Init_0) /\ valid_rw(Malloc_0, p, Length_of_S1_S).
(* Call Effects *)
Have: monotonic_init(Init_0, a).
}
Prove: IsInit_S1_S(p, a).
+------------------------------------------------------------
+
+Goal Check 'succeed' (file tests/wp_acsl/opaque_struct.i, line 32):
+Let x = p.base.
+Assume {
+ (* Heap *)
+ Type: (region(x) <= 0) /\ linked(Malloc_0).
+ (* Pre-condition *)
+ Have: valid_rw(Malloc_0, p, Length_of_S1_S).
+}
+Prove: 0 <= (BytesLength_of_S1_S * Malloc_0[x]).
+
------------------------------------------------------------
------------------------------------------------------------
Function uninitialized_assigns
------------------------------------------------------------
-Goal Check 'should_fail' (file tests/wp_acsl/opaque_struct.i, line 39):
-Let a = havoc(Init_undef_0, Init_0, p, Size_of_S1_S).
+Goal Check 'fail' (file tests/wp_acsl/opaque_struct.i, line 47):
+Let a = havoc(Init_undef_0, Init_0, p, Length_of_S1_S).
Assume {
(* Heap *)
Type: (region(p.base) <= 0) /\ cinits(Init_0).
@@ -63,8 +151,8 @@ Prove: !IsInit_S1_S(p, a).
------------------------------------------------------------
-Goal Check 'should_fail' (file tests/wp_acsl/opaque_struct.i, line 40):
-Let a = havoc(Init_undef_0, Init_0, p, Size_of_S1_S).
+Goal Check 'fail' (file tests/wp_acsl/opaque_struct.i, line 48):
+Let a = havoc(Init_undef_0, Init_0, p, Length_of_S1_S).
Assume {
(* Heap *)
Type: (region(p.base) <= 0) /\ cinits(Init_0).
@@ -76,8 +164,23 @@ Assume {
Prove: IsInit_S1_S(p, a).
------------------------------------------------------------
-[wp] tests/wp_acsl/opaque_struct.i:23: Warning:
+[wp] tests/wp_acsl/opaque_struct.i:24: Warning:
Memory model hypotheses for function 'g':
/*@ behavior wp_typed:
requires \separated(p, &S1, &S2, &p); */
void g(void);
+[wp] tests/wp_acsl/opaque_struct.i:57: Warning:
+ Memory model hypotheses for function 'assign':
+ /*@ behavior wp_typed:
+ requires \separated(a, &S1, &S2); */
+ void assign(struct S *a);
+[wp] tests/wp_acsl/opaque_struct.i:60: Warning:
+ Memory model hypotheses for function 'assigns_effect':
+ /*@
+ behavior wp_typed:
+ requires \separated(a, &S1, &S2);
+ requires \separated(c, &S1, &S2);
+ requires \separated(p_0, &S1, &S2);
+ requires \separated(q, &S1, &S2);
+ */
+ void assigns_effect(int *p_0, float *q, char *c, struct S *a);
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/opaque_struct.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/opaque_struct.res.oracle
index a0b9b493076..d8a3007152e 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/opaque_struct.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/opaque_struct.res.oracle
@@ -2,28 +2,51 @@
[kernel] Parsing tests/wp_acsl/opaque_struct.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
-[wp] 7 goals scheduled
-[wp] [Alt-Ergo] Goal typed_check_lemma_should_fail : Unsuccess
-[wp] [Qed] Goal typed_check_lemma_should_succeed : Valid
-[wp] [Alt-Ergo] Goal typed_assigns_check_should_fail : Unsuccess
-[wp] [Qed] Goal typed_assigns_check_should_succeed : Valid
-[wp] [Alt-Ergo] Goal typed_initialized_assigns_check_should_succeed : Valid
-[wp] [Alt-Ergo] Goal typed_uninitialized_assigns_check_should_fail : Unsuccess
-[wp] [Alt-Ergo] Goal typed_uninitialized_assigns_check_should_fail_2 : Unsuccess
-[wp] Proved goals: 3 / 7
+[wp] 13 goals scheduled
+[wp] [Alt-Ergo] Goal typed_check_lemma_fail : Unsuccess
+[wp] [Qed] Goal typed_check_lemma_succeed_L1 : Valid
+[wp] [Alt-Ergo] Goal typed_check_lemma_succeed_L2 : Valid
+[wp] [Alt-Ergo] Goal typed_assigns_check_fail : Unsuccess
+[wp] [Qed] Goal typed_assigns_check_succeed : Valid
+[wp] [Alt-Ergo] Goal typed_initialized_assigns_check_succeed : Valid
+[wp] [Alt-Ergo] Goal typed_initialized_assigns_check_succeed_2 : Valid
+[wp] [Alt-Ergo] Goal typed_uninitialized_assigns_check_fail : Unsuccess
+[wp] [Alt-Ergo] Goal typed_uninitialized_assigns_check_fail_2 : Unsuccess
+[wp] [Alt-Ergo] Goal typed_assigned_via_pointer_check_fail : Unsuccess
+[wp] [Alt-Ergo] Goal typed_assigns_effect_check_fail : Unsuccess
+[wp] [Alt-Ergo] Goal typed_assigns_effect_check_fail_2 : Unsuccess
+[wp] [Alt-Ergo] Goal typed_assigns_effect_check_succeed : Valid
+[wp] Proved goals: 6 / 13
Qed: 2
- Alt-Ergo: 1 (unsuccess: 4)
+ Alt-Ergo: 4 (unsuccess: 7)
------------------------------------------------------------
Axiomatics WP Alt-Ergo Total Success
- Axiomatic test 1 - 2 50.0%
+ Axiomatic test 1 1 3 66.7%
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
assigns 1 - 2 50.0%
- initialized_assigns - 1 1 100%
+ initialized_assigns - 2 2 100%
uninitialized_assigns - - 2 0.0%
+ assigned_via_pointer - - 1 0.0%
+ assigns_effect - 1 3 33.3%
------------------------------------------------------------
-[wp] tests/wp_acsl/opaque_struct.i:23: Warning:
+[wp] tests/wp_acsl/opaque_struct.i:24: Warning:
Memory model hypotheses for function 'g':
/*@ behavior wp_typed:
requires \separated(p, &S1, &S2, &p); */
void g(void);
+[wp] tests/wp_acsl/opaque_struct.i:57: Warning:
+ Memory model hypotheses for function 'assign':
+ /*@ behavior wp_typed:
+ requires \separated(a, &S1, &S2); */
+ void assign(struct S *a);
+[wp] tests/wp_acsl/opaque_struct.i:60: Warning:
+ Memory model hypotheses for function 'assigns_effect':
+ /*@
+ behavior wp_typed:
+ requires \separated(a, &S1, &S2);
+ requires \separated(c, &S1, &S2);
+ requires \separated(p_0, &S1, &S2);
+ requires \separated(q, &S1, &S2);
+ */
+ void assigns_effect(int *p_0, float *q, char *c, struct S *a);
--
GitLab