diff --git a/src/plugins/wp/MemTyped.ml b/src/plugins/wp/MemTyped.ml
index c8d82ca1aeeb11174fb1401795a77d809c7abeab..63c759f0498dc1021c47c79fc16be245a1fbaad4 100644
--- a/src/plugins/wp/MemTyped.ml
+++ b/src/plugins/wp/MemTyped.ml
@@ -1194,13 +1194,13 @@ struct
match compare ~dst:u ~src:v with
| Mismatch -> Mismatch
| Drem u' ->
- let w1 = u' @ add_array u (n-1) w1 in
- let w2 = add_array v (m-1) w2 in
- compare w1 w2
+ let w1 = u' @ add_array u (n-1) w1 in
+ let w2 = add_array v (m-1) w2 in
+ compare w1 w2
| Srem v' ->
- let w1 = add_array u (n-1) w1 in
- let w2 = v' @ add_array v (m-1) w2 in
- compare w1 w2
+ let w1 = add_array u (n-1) w1 in
+ let w2 = v' @ add_array v (m-1) w2 in
+ compare w1 w2
| Equal ->
if n < m then
let w2 = add_array v (m-n) w2 in
@@ -1217,6 +1217,39 @@ struct
| Str _ , Arr(v,n) ->
compare ~dst ~src:(v @ add_array v (n-1) w2)
+ let rec repeated ~dst ~src =
+ match dst , src with
+ | [] , [] -> true (* src = dst *)
+ | _ , [] -> false (* empty source layout *)
+ | [] , _ -> false (* empty destination layout *)
+ | [p] , [q] -> begin
+ match p , q with
+ | Garbled , _ | _ , Garbled -> false
+ | Str(a,n) , Str(b,m) -> (* dst =?= repeated(src,n/m) *)
+ equal_atom a b && n >= m && (n mod m = 0)
+ | Arr(u,n) , Arr(v,m) ->
+ begin
+ match compare ~dst:u ~src:v with
+ | Mismatch -> false
+ | Drem u' ->
+ let w1 = u' @ add_array u (n-1) [] in
+ let w2 = add_array v (m-1) [] in
+ let cmp = compare ~dst:w1 ~src:w2 in
+ repeated_result ~src cmp
+ | Srem _ ->
+ false
+ | Equal -> (* dst =?= repeated(src,n/m) *)
+ n >= m && (n mod m = 0)
+ end
+ | _ , _ -> repeated_compare ~dst ~src
+ end
+ | _ , _ -> repeated_compare ~dst ~src
+ and repeated_compare ~dst ~src = repeated_result ~src (compare ~dst ~src)
+ and repeated_result ~src = function
+ | Equal -> true
+ | Mismatch | Srem _ -> false
+ | Drem dst -> repeated ~dst ~src
+
let fits ~dst ~src =
match dst , src with
| C_int i1 , C_int i2 -> i1 = i2
@@ -1224,9 +1257,11 @@ struct
| C_comp c , C_comp d when Compinfo.equal c d -> true
| C_pointer _ , C_pointer _ -> true
| _ ->
- match compare ~dst:(layout dst) ~src:(layout src) with
+ let src = layout src in
+ match compare ~dst:(layout dst) ~src with
| Equal | Srem _ -> true
- | Drem _ | Mismatch -> false
+ | Mismatch -> false
+ | Drem dst -> repeated dst src
let rec pretty fmt = function
| C_pointer ty -> Format.fprintf fmt "%a*" pretty (Ctypes.object_of ty)
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/logic.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/logic.res.oracle
index fe7f03a505d3ef3994930b9f69594c10c4126b1a..96e9d783dee19dc190706ff0af7dd5432c8e29d6 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/logic.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/logic.res.oracle
@@ -3,15 +3,9 @@
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
-[wp] tests/wp_acsl/logic.i:16: Warning:
- Cast with incompatible pointers types (source: __anonstruct_Point_1*)
- (target: __anonstruct_Point_1[3]*)
[wp] tests/wp_acsl/logic.i:65: Warning:
Cast with incompatible pointers types (source: __anonstruct_Buint_4*)
(target: uint32*)
-[wp] tests/wp_acsl/logic.i:48: Warning:
- Cast with incompatible pointers types (source: __anonstruct_Point_1*)
- (target: __anonstruct_Point_1[3]*)
[wp] tests/wp_acsl/logic.i:49: Warning:
Logic cast from struct (Tint2) not implemented yet
[wp] tests/wp_acsl/logic.i:50: Warning:
@@ -45,28 +39,16 @@
------------------------------------------------------------
Goal Post-condition (file tests/wp_acsl/logic.i, line 21) in 'h':
-tests/wp_acsl/logic.i:16: warning from Typed Model:
- - Warning: Keep pointer value
- Reason: Cast with incompatible pointers types (source: __anonstruct_Point_1*)
- (target: __anonstruct_Point_1[3]*)
Prove: true.
------------------------------------------------------------
Goal Assigns nothing in 'h':
-tests/wp_acsl/logic.i:16: warning from Typed Model:
- - Warning: Keep pointer value
- Reason: Cast with incompatible pointers types (source: __anonstruct_Point_1*)
- (target: __anonstruct_Point_1[3]*)
Prove: true.
------------------------------------------------------------
Goal Assigns nothing in 'h':
-tests/wp_acsl/logic.i:16: warning from Typed Model:
- - Warning: Keep pointer value
- Reason: Cast with incompatible pointers types (source: __anonstruct_Point_1*)
- (target: __anonstruct_Point_1[3]*)
Prove: true.
------------------------------------------------------------
@@ -154,10 +136,6 @@ Prove: P_P(m).
------------------------------------------------------------
Goal Pre-condition 'qed_ok' in 'main':
-tests/wp_acsl/logic.i:48: warning from Typed Model:
- - Warning: Keep pointer value
- Reason: Cast with incompatible pointers types (source: __anonstruct_Point_1*)
- (target: __anonstruct_Point_1[3]*)
Let a = global(G_tr_31).
Let a_1 = shift___anonstruct_Point_1(a, 2).
Let a_2 = shift___anonstruct_Point_1(a, 1).
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/logic.0.report.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/logic.0.report.json
index badcee8deb06c806b1e1fba397198f03ad075183..ab5fc8563a85e73fde964694df6276391d9aa62d 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/logic.0.report.json
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/logic.0.report.json
@@ -1,21 +1,17 @@
-{ "wp:global": { "alt-ergo": { "total": 18, "valid": 2, "unknown": 16,
+{ "wp:global": { "alt-ergo": { "total": 17, "valid": 3, "unknown": 14,
"rank": 16 },
- "qed": { "total": 3, "valid": 3 },
- "wp:main": { "total": 21, "valid": 5, "unknown": 16,
+ "qed": { "total": 4, "valid": 4 },
+ "wp:main": { "total": 21, "valid": 7, "unknown": 14,
"rank": 16 } },
"wp:functions": { "h": { "h_assigns": { "qed": { "total": 2, "valid": 2 },
"wp:main": { "total": 2,
"valid": 2 } },
- "h_ensures": { "alt-ergo": { "total": 1,
- "unknown": 1 },
+ "h_ensures": { "qed": { "total": 1, "valid": 1 },
"wp:main": { "total": 1,
- "unknown": 1 } },
- "wp:section": { "alt-ergo": { "total": 1,
- "unknown": 1 },
- "qed": { "total": 2, "valid": 2 },
+ "valid": 1 } },
+ "wp:section": { "qed": { "total": 3, "valid": 3 },
"wp:main": { "total": 3,
- "valid": 2,
- "unknown": 1 } } },
+ "valid": 3 } } },
"main": { "main_requires_qed_ok_18": { "alt-ergo":
{ "total": 1,
"unknown": 1 },
@@ -102,10 +98,12 @@
"unknown": 1 } },
"main_requires_qed_ok_4": { "alt-ergo":
{ "total": 1,
- "unknown": 1 },
+ "valid": 1,
+ "rank": 16 },
"wp:main":
{ "total": 1,
- "unknown": 1 } },
+ "valid": 1,
+ "rank": 16 } },
"main_requires_qed_ok_3": { "alt-ergo":
{ "total": 1,
"valid": 1,
@@ -127,12 +125,12 @@
"wp:main": { "total": 1,
"valid": 1 } },
"wp:section": { "alt-ergo": { "total": 17,
- "valid": 2,
- "unknown": 15,
+ "valid": 3,
+ "unknown": 14,
"rank": 16 },
"qed": { "total": 1,
"valid": 1 },
"wp:main": { "total": 18,
- "valid": 3,
- "unknown": 15,
+ "valid": 4,
+ "unknown": 14,
"rank": 16 } } } } }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/logic.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/logic.res.oracle
index 6df7d6c5cdf988c53380e765f67453ff61a9f1e8..8f4e0382edf2329f69008efbaffa228b870a50d4 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/logic.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/logic.res.oracle
@@ -3,15 +3,9 @@
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
-[wp] tests/wp_acsl/logic.i:16: Warning:
- Cast with incompatible pointers types (source: __anonstruct_Point_1*)
- (target: __anonstruct_Point_1[3]*)
[wp] tests/wp_acsl/logic.i:65: Warning:
Cast with incompatible pointers types (source: __anonstruct_Buint_4*)
(target: uint32*)
-[wp] tests/wp_acsl/logic.i:48: Warning:
- Cast with incompatible pointers types (source: __anonstruct_Point_1*)
- (target: __anonstruct_Point_1[3]*)
[wp] tests/wp_acsl/logic.i:49: Warning:
Logic cast from struct (Tint2) not implemented yet
[wp] tests/wp_acsl/logic.i:50: Warning:
@@ -47,7 +41,7 @@
[wp] [Qed] Goal typed_cast_main_requires_qed_ok : Valid
[wp] [Alt-Ergo] Goal typed_cast_main_requires_qed_ok_2 : Unsuccess
[wp] [Alt-Ergo] Goal typed_cast_main_requires_qed_ok_3 : Unsuccess
-[wp] [Alt-Ergo] Goal typed_cast_main_requires_qed_ok_4 : Unsuccess (Stronger)
+[wp] [Alt-Ergo] Goal typed_cast_main_requires_qed_ok_4 : Unsuccess
[wp] [Alt-Ergo] Goal typed_cast_main_requires_qed_ok_5 : Unsuccess (Stronger)
[wp] [Alt-Ergo] Goal typed_cast_main_requires_qed_ok_6 : Unsuccess (Stronger)
[wp] [Alt-Ergo] Goal typed_cast_main_requires_qed_ok_7 : Unsuccess (Stronger)