diff --git a/src/plugins/wp/MemTyped.ml b/src/plugins/wp/MemTyped.ml
index 5320e25967110d07731d5cba700eddbd3e061e58..c8d82ca1aeeb11174fb1401795a77d809c7abeab 100644
--- a/src/plugins/wp/MemTyped.ml
+++ b/src/plugins/wp/MemTyped.ml
@@ -1062,14 +1062,15 @@ module Layout : sig
val fits: dst:c_object -> src:c_object -> bool
(* returns [true] in these cases:
- - [dst] fits into [src]
- - [dst] equals [src] *)
+ - [dst] fits into [src] (exists cobj; [src] = [dst] concat cobj)
+ - [dst] equals [src] ([dst] = [src]) *)
end =
struct
- type atom = P of typ | I of c_int | F of c_float
+ type atom = P of typ | I of c_int | F of c_float | U of Cil_types.compinfo
let pp_atom fmt = function
+ | U ci -> Format.fprintf fmt "union %a" Printer.pp_compinfo ci
| P ty -> Printer.pp_typ fmt (TPtr(ty,[]))
| I i -> Ctypes.pp_int fmt i
| F f -> Ctypes.pp_float fmt f
@@ -1077,7 +1078,10 @@ struct
let eqatom a1 a2 =
match a1 , a2 with
| P _ , P _ -> true
- | _ -> (a1 = a2)
+ | U u1 , U u2 -> Compinfo.equal u1 u2
+ | I i1 , I i2 -> i1 = i2
+ | F f1 , F f2 -> f1 = f2
+ | _ -> false
type block =
| Str of atom * int
@@ -1124,12 +1128,13 @@ struct
| C_int i -> add_atom (I i) w
| C_float f -> add_atom (F f) w
| C_pointer t -> add_atom (P t) w
+ | C_comp { cfields = [f] } ->
+ flayout w f (* unions containing only one field are
+ considered as structures *)
| C_comp c ->
if c.cstruct
then List.fold_left flayout w c.cfields
- else
- (* TODO: can be the longest common prefix *)
- add_block Garbled w
+ else add_atom (U c) w (* unions with several fields *)
| C_array { arr_flat = Some a } ->
let ly = rlayout [] (Ctypes.object_of a.arr_cell) in
if a.arr_cell_nbr = 1
@@ -1146,21 +1151,34 @@ struct
let layout (obj : c_object) : layout = List.rev (rlayout [] obj)
- type comparison = Fit | Equal | Mismatch
+ let add_compound (c: Cil_types.compinfo) w : layout =
+ List.fold_left flayout w (List.rev c.cfields)
+
+ let ulayout (c: Cil_types.compinfo) : layout = add_compound c []
+
+ type comparison = Srem of layout | Drem of layout | Equal | Mismatch
let add_array ly n w =
if n=1 then ly @ w else add_many ly n w
- let rec compare ~dst ~src =
+ let rec equal_atom a b =
+ (eqatom a b) ||
+ (match a,b with
+ | U u1, U u2 -> (* for union, the layouts must be equal *)
+ (match compare ~dst:(ulayout u1) ~src:(ulayout u2) with
+ | Equal -> true
+ | _ -> false)
+ | _, _ -> false)
+ and compare ~dst ~src =
match dst , src with
| [] , [] -> Equal (* src = dst *)
- | [] , _ -> Fit (* exists obj ; src = dst concat obj *)
- | _ , [] -> Mismatch
+ | [] , obj -> Srem obj (* src = dst @ obj *)
+ | obj , [] -> Drem obj (* dst = src @ obj *)
| p::w1 , q::w2 ->
match p , q with
| Garbled , _ | _ , Garbled -> Mismatch
| Str(a,n) , Str(b,m) ->
- if eqatom a b then
+ if equal_atom a b then
if n < m then
let w2 = Str(a,m-n)::w2 in
compare w1 w2
@@ -1175,7 +1193,14 @@ struct
begin
match compare ~dst:u ~src:v with
| Mismatch -> Mismatch
- | Fit -> 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
+ | Srem v' ->
+ 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
@@ -1200,8 +1225,8 @@ struct
| C_pointer _ , C_pointer _ -> true
| _ ->
match compare ~dst:(layout dst) ~src:(layout src) with
- | Equal | Fit -> true
- | Mismatch -> false
+ | Equal | Srem _ -> true
+ | Drem _ | Mismatch -> false
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_typed/oracle/cast_fits.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/cast_fits.0.res.oracle
index d9d935d41738a286acc33595f24e8552f1593e8f..56beccaf01fa52665901dd19e21253de0b119058 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/cast_fits.0.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/cast_fits.0.res.oracle
@@ -3,12 +3,6 @@
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
-[wp] tests/wp_typed/cast_fits.i:39: Warning:
- Cast with incompatible pointers types (source: __anonstruct_L5_5*)
- (target: __anonstruct_L6_6*)
-[wp] tests/wp_typed/cast_fits.i:47: Warning:
- Cast with incompatible pointers types (source: __anonunion_L7_7*)
- (target: sint32*)
[wp] tests/wp_typed/cast_fits.i:13: Warning:
Cast with incompatible pointers types (source: __anonstruct_L2_2*)
(target: sint32*)
@@ -70,11 +64,7 @@ Prove: x_1 = x.
------------------------------------------------------------
Goal Post-condition (file tests/wp_typed/cast_fits.i, line 37) in 'fits4':
-tests/wp_typed/cast_fits.i:39: warning from Typed Model:
- - Warning: Hide sub-term definition
- Reason: Cast with incompatible pointers types (source: __anonstruct_L5_5*)
- (target: __anonstruct_L6_6*)
-Let x = Mchar_0[shiftfield_F6_c6(q)].
+Let x = Mchar_0[shiftfield_F6_c6(p)].
Let x_1 = Mchar_0
[shiftfield_F3_c3(shift___anonstruct_L3_3(shiftfield_F5_ci5(p),
1))].
@@ -91,11 +81,7 @@ Prove: x_1 = x.
------------------------------------------------------------
Goal Post-condition (file tests/wp_typed/cast_fits.i, line 45) in 'fits5':
-tests/wp_typed/cast_fits.i:47: warning from Typed Model:
- - Warning: Hide sub-term definition
- Reason: Cast with incompatible pointers types (source: __anonunion_L7_7*)
- (target: sint32*)
-Let x = Mint_0[q].
+Let x = Mint_0[p].
Let x_1 = Mint_0[shiftfield_F7_u7(p)].
Assume {
Type: is_sint32(x) /\ is_sint32(x_1).
diff --git a/src/plugins/wp/tests/wp_typed/oracle/cast_fits.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/cast_fits.1.res.oracle
index 0fe3ebad7424b28bd8090d4916f8f1246f982ee9..cc8072d61ce0f259dd2e73a19b11d96f46c2512d 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/cast_fits.1.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/cast_fits.1.res.oracle
@@ -3,12 +3,6 @@
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
-[wp] tests/wp_typed/cast_fits.i:39: Warning:
- Cast with incompatible pointers types (source: __anonstruct_L5_5*)
- (target: __anonstruct_L6_6*)
-[wp] tests/wp_typed/cast_fits.i:47: Warning:
- Cast with incompatible pointers types (source: __anonunion_L7_7*)
- (target: sint32*)
[wp] tests/wp_typed/cast_fits.i:13: Warning:
Cast with incompatible pointers types (source: __anonstruct_L2_2*)
(target: sint32*)
@@ -70,11 +64,7 @@ Prove: x_1 = x.
------------------------------------------------------------
Goal Post-condition (file tests/wp_typed/cast_fits.i, line 37) in 'fits4':
-tests/wp_typed/cast_fits.i:39: warning from Typed Model:
- - Warning: Hide sub-term definition
- Reason: Cast with incompatible pointers types (source: __anonstruct_L5_5*)
- (target: __anonstruct_L6_6*)
-Let x = Mchar_0[shiftfield_F6_c6(q)].
+Let x = Mchar_0[shiftfield_F6_c6(p)].
Let x_1 = Mchar_0
[shiftfield_F3_c3(shift___anonstruct_L3_3(shiftfield_F5_ci5(p),
1))].
@@ -91,11 +81,7 @@ Prove: x_1 = x.
------------------------------------------------------------
Goal Post-condition (file tests/wp_typed/cast_fits.i, line 45) in 'fits5':
-tests/wp_typed/cast_fits.i:47: warning from Typed Model:
- - Warning: Hide sub-term definition
- Reason: Cast with incompatible pointers types (source: __anonunion_L7_7*)
- (target: sint32*)
-Let x = Mint_0[q].
+Let x = Mint_0[p].
Let x_1 = Mint_0[shiftfield_F7_u7(p)].
Assume {
Type: is_sint32(x) /\ is_sint32(x_1).
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/cast_fits.0.report.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/cast_fits.0.report.json
index 3003aaa8a860a03d7085e8098f82494f7239592f..193b5d5e58bebc238a27b6c45e343141affb683a 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/cast_fits.0.report.json
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/cast_fits.0.report.json
@@ -1,7 +1,7 @@
-{ "wp:global": { "alt-ergo": { "total": 8, "valid": 3, "unknown": 5,
- "rank": 7 },
- "wp:main": { "total": 8, "valid": 3, "unknown": 5,
- "rank": 7 } },
+{ "wp:global": { "alt-ergo": { "total": 8, "valid": 5, "unknown": 3,
+ "rank": 8 },
+ "wp:main": { "total": 8, "valid": 5, "unknown": 3,
+ "rank": 8 } },
"wp:functions": { "fits1": { "fits1_ensures": { "alt-ergo": { "total": 1,
"valid": 1,
"rank": 6 },
@@ -49,21 +49,29 @@
"valid": 1,
"rank": 7 } } },
"fits4": { "fits4_ensures": { "alt-ergo": { "total": 1,
- "unknown": 1 },
+ "valid": 1,
+ "rank": 8 },
"wp:main": { "total": 1,
- "unknown": 1 } },
+ "valid": 1,
+ "rank": 8 } },
"wp:section": { "alt-ergo": { "total": 1,
- "unknown": 1 },
+ "valid": 1,
+ "rank": 8 },
"wp:main": { "total": 1,
- "unknown": 1 } } },
+ "valid": 1,
+ "rank": 8 } } },
"fits5": { "fits5_ensures": { "alt-ergo": { "total": 1,
- "unknown": 1 },
+ "valid": 1,
+ "rank": 6 },
"wp:main": { "total": 1,
- "unknown": 1 } },
+ "valid": 1,
+ "rank": 6 } },
"wp:section": { "alt-ergo": { "total": 1,
- "unknown": 1 },
+ "valid": 1,
+ "rank": 6 },
"wp:main": { "total": 1,
- "unknown": 1 } } },
+ "valid": 1,
+ "rank": 6 } } },
"mismatch2": { "mismatch2_ensures": { "alt-ergo":
{ "total": 1,
"unknown": 1 },
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/cast_fits.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/cast_fits.res.oracle
index 41a7947cd45a046af542b6bca6c43d115baa713c..6bc88bcb22a2bf7acb1f1acca3ffc64da2dca480 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/cast_fits.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/cast_fits.res.oracle
@@ -3,12 +3,6 @@
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
-[wp] tests/wp_typed/cast_fits.i:39: Warning:
- Cast with incompatible pointers types (source: __anonstruct_L5_5*)
- (target: __anonstruct_L6_6*)
-[wp] tests/wp_typed/cast_fits.i:47: Warning:
- Cast with incompatible pointers types (source: __anonunion_L7_7*)
- (target: sint32*)
[wp] tests/wp_typed/cast_fits.i:13: Warning:
Cast with incompatible pointers types (source: __anonstruct_L2_2*)
(target: sint32*)
@@ -22,14 +16,14 @@
[wp] [Alt-Ergo] Goal typed_fits1_ensures : Valid
[wp] [Alt-Ergo] Goal typed_fits2_ensures : Valid
[wp] [Alt-Ergo] Goal typed_fits3_ensures : Valid
-[wp] [Alt-Ergo] Goal typed_fits4_ensures : Unsuccess (Stronger)
-[wp] [Alt-Ergo] Goal typed_fits5_ensures : Unsuccess (Stronger)
+[wp] [Alt-Ergo] Goal typed_fits4_ensures : Valid
+[wp] [Alt-Ergo] Goal typed_fits5_ensures : Valid
[wp] [Alt-Ergo] Goal typed_mismatch1_ensures : Unsuccess (Stronger)
[wp] [Alt-Ergo] Goal typed_mismatch2_ensures : Unsuccess (Stronger)
[wp] [Alt-Ergo] Goal typed_mismatch3_ensures : Unsuccess (Stronger)
-[wp] Proved goals: 3 / 8
+[wp] Proved goals: 5 / 8
Qed: 0
- Alt-Ergo: 3 (unsuccess: 5)
+ Alt-Ergo: 5 (unsuccess: 3)
[wp] Report in: 'tests/wp_typed/oracle_qualif/cast_fits.0.report.json'
[wp] Report out: 'tests/wp_typed/result_qualif/cast_fits.0.report.json'
-------------------------------------------------------------
@@ -38,8 +32,8 @@ fits1 - 1 (20..32) 1 100%
mismatch1 - - 1 0.0%
fits2 - 1 (20..32) 1 100%
fits3 - 1 (24..36) 1 100%
-fits4 - - 1 0.0%
-fits5 - - 1 0.0%
+fits4 - 1 (28..40) 1 100%
+fits5 - 1 (20..32) 1 100%
mismatch2 - - 1 0.0%
mismatch3 - - 1 0.0%
-------------------------------------------------------------