diff --git a/src/plugins/wp/MemTyped.ml b/src/plugins/wp/MemTyped.ml
index 6de0a92ea470f46ac2559dbef0a92a60dd5edc15..63c759f0498dc1021c47c79fc16be245a1fbaad4 100644
--- a/src/plugins/wp/MemTyped.ml
+++ b/src/plugins/wp/MemTyped.ml
@@ -1057,12 +1057,20 @@ let block_length sigma obj l =
(* --- Cast --- *)
(* -------------------------------------------------------------------------- *)
-module Layout =
+module Layout : sig
+ val pretty : Format.formatter -> c_object -> unit
+
+ val fits: dst:c_object -> src:c_object -> bool
+ (* returns [true] in these cases:
+ - [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
@@ -1070,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
@@ -1117,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
@@ -1139,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 l1 l2 =
- match l1 , l2 with
- | [] , [] -> Equal
- | [] , _ -> Fit
- | _ , [] -> Mismatch
+ 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 *)
+ | [] , 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
@@ -1166,9 +1191,16 @@ struct
else Mismatch
| Arr(u,n) , Arr(v,m) ->
begin
- match compare u v with
+ 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
@@ -1181,20 +1213,55 @@ struct
compare w1 w2
end
| Arr(v,n) , Str _ ->
- compare (v @ add_array v (n-1) w1) l2
+ compare ~dst:(v @ add_array v (n-1) w1) ~src
| Str _ , Arr(v,n) ->
- compare l1 (v @ add_array v (n-1) w2)
-
- let fits obj1 obj2 =
- match obj1 , obj2 with
+ 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
| C_float f1 , C_float f2 -> f1 = f2
| C_comp c , C_comp d when Compinfo.equal c d -> true
| C_pointer _ , C_pointer _ -> true
| _ ->
- match compare (layout obj1) (layout obj2) with
- | Equal | Fit -> true
+ let src = layout src in
+ match compare ~dst:(layout dst) ~src with
+ | Equal | Srem _ -> true
| Mismatch -> false
+ | Drem dst -> repeated dst src
let rec pretty fmt = function
| C_pointer ty -> Format.fprintf fmt "%a*" pretty (Ctypes.object_of ty)
@@ -1223,10 +1290,10 @@ let cast s l =
match Context.get pointer with
| NoCast -> Warning.error ~source:"Typed Model" "%a" pp_mismatch s
| Fits ->
- if Layout.fits s.post s.pre then l else
+ if Layout.fits ~dst:s.post ~src:s.pre then l else
Warning.error ~source:"Typed Model" "%a" pp_mismatch s
| Unsafe ->
- if not (Layout.fits s.post s.pre) then
+ if not (Layout.fits ~dst:s.post ~src:s.pre) then
Warning.emit ~severe:false ~source:"Typed Model"
~effect:"Keep pointer value"
"%a" pp_mismatch s ; l
diff --git a/src/plugins/wp/ctypes.ml b/src/plugins/wp/ctypes.ml
index 04cd9701c91426a98d40259689f9c518e9d46d0a..bde88014eff652f7934de930b483c41815ff837d 100644
--- a/src/plugins/wp/ctypes.ml
+++ b/src/plugins/wp/ctypes.ml
@@ -464,9 +464,12 @@ let sizeof_object = function
WpLog.fatal ~current:true "Sizeof unknown-size array"
let field_offset fd =
- let ctype = TComp(fd.fcomp,Cil.empty_size_cache(),[]) in
- let offset = Field(fd,NoOffset) in
- fst (Cil.bitsOffset ctype offset) / 8
+ if fd.fcomp.cstruct then (* C struct *)
+ let ctype = TComp(fd.fcomp,Cil.empty_size_cache(),[]) in
+ let offset = Field(fd,NoOffset) in
+ fst (Cil.bitsOffset ctype offset) / 8
+ else (* CIL invariant: all C union fields start at offset 0 *)
+ 0
(* Conforms to C-ISO 6.3.1.8 *)
(* If same sign => greater rank. *)
diff --git a/src/plugins/wp/tests/wp_acsl/logic.i b/src/plugins/wp/tests/wp_acsl/logic.i
index 3d6f566be3ac4dba97d7a9aa6df2e28480e6f99a..7a54adc27e1d6764c96cef25f3bdd3facdfbedbe 100644
--- a/src/plugins/wp/tests/wp_acsl/logic.i
+++ b/src/plugins/wp/tests/wp_acsl/logic.i
@@ -1,9 +1,9 @@
/* run.config
- OPT: -wp-model Typed+cast
-*//* run.config_qualif
- OPT: -wp -wp-model Typed+cast -wp-steps 50
+ OPT: -wp-model Typed
+*/
+/* run.config_qualif
+ OPT: -wp -wp-model Typed -wp-steps 50
*/
-
// Test logic types defined from C types
//--------------------------------------
typedef struct { int x ; int y ; } Point ;
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..a3547cdccf7acb41cb77c368f97cbefbca8ec98c 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/logic.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/logic.res.oracle
@@ -1,17 +1,11 @@
-# frama-c -wp -wp-model 'Typed (Cast)' [...]
+# frama-c -wp [...]
[kernel] Parsing tests/wp_acsl/logic.i (no preprocessing)
[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.
------------------------------------------------------------
@@ -84,19 +66,18 @@ Let a = global(G_tr_31).
Let a_1 = shift___anonstruct_Point_1(a, 2).
Let a_2 = shift___anonstruct_Point_1(a, 1).
Let a_3 = shift___anonstruct_Point_1(a, 0).
-Let a_4 = global(G_buint_37).
-Let a_5 = shiftfield_F4_bytes(a_4).
+Let a_4 = shiftfield_F4_bytes(global(G_buint_37)).
Let m = Array1_S1(a_3, 3, Mint_0).
Assume {
- Type: is_uint32(Mint_0[a_4]) /\ IsArray1S1(m).
+ Type: IsArray1S1(m).
(* Initializer *)
- Init: Mint_0[shift_uint8(a_5, 0)] = 1.
+ Init: Mint_0[shift_uint8(a_4, 0)] = 1.
(* Initializer *)
- Init: Mint_0[shift_uint8(a_5, 1)] = 2.
+ Init: Mint_0[shift_uint8(a_4, 1)] = 2.
(* Initializer *)
- Init: Mint_0[shift_uint8(a_5, 2)] = 4.
+ Init: Mint_0[shift_uint8(a_4, 2)] = 4.
(* Initializer *)
- Init: Mint_0[shift_uint8(a_5, 3)] = 8.
+ Init: Mint_0[shift_uint8(a_4, 3)] = 8.
(* Initializer *)
Init: Mint_0[shiftfield_F1_x(a_3)] = 10.
(* Initializer *)
@@ -121,19 +102,18 @@ Let a = global(G_tr_31).
Let a_1 = shift___anonstruct_Point_1(a, 2).
Let a_2 = shift___anonstruct_Point_1(a, 1).
Let a_3 = shift___anonstruct_Point_1(a, 0).
-Let a_4 = global(G_buint_37).
-Let a_5 = shiftfield_F4_bytes(a_4).
+Let a_4 = shiftfield_F4_bytes(global(G_buint_37)).
Let m = Array1_S1(a_3, 3, Mint_0).
Assume {
- Type: is_uint32(Mint_0[a_4]) /\ IsArray1S1(m).
+ Type: IsArray1S1(m).
(* Initializer *)
- Init: Mint_0[shift_uint8(a_5, 0)] = 1.
+ Init: Mint_0[shift_uint8(a_4, 0)] = 1.
(* Initializer *)
- Init: Mint_0[shift_uint8(a_5, 1)] = 2.
+ Init: Mint_0[shift_uint8(a_4, 1)] = 2.
(* Initializer *)
- Init: Mint_0[shift_uint8(a_5, 2)] = 4.
+ Init: Mint_0[shift_uint8(a_4, 2)] = 4.
(* Initializer *)
- Init: Mint_0[shift_uint8(a_5, 3)] = 8.
+ Init: Mint_0[shift_uint8(a_4, 3)] = 8.
(* Initializer *)
Init: Mint_0[shiftfield_F1_x(a_3)] = 10.
(* Initializer *)
@@ -154,27 +134,22 @@ 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).
Let a_3 = shift___anonstruct_Point_1(a, 0).
-Let a_4 = global(G_buint_37).
-Let a_5 = shiftfield_F4_bytes(a_4).
+Let a_4 = shiftfield_F4_bytes(global(G_buint_37)).
Let m = Array1_S1(a_3, 3, Mint_0).
Assume {
- Type: is_uint32(Mint_0[a_4]) /\ IsArray1S1(m).
+ Type: IsArray1S1(m).
(* Initializer *)
- Init: Mint_0[shift_uint8(a_5, 0)] = 1.
+ Init: Mint_0[shift_uint8(a_4, 0)] = 1.
(* Initializer *)
- Init: Mint_0[shift_uint8(a_5, 1)] = 2.
+ Init: Mint_0[shift_uint8(a_4, 1)] = 2.
(* Initializer *)
- Init: Mint_0[shift_uint8(a_5, 2)] = 4.
+ Init: Mint_0[shift_uint8(a_4, 2)] = 4.
(* Initializer *)
- Init: Mint_0[shift_uint8(a_5, 3)] = 8.
+ Init: Mint_0[shift_uint8(a_4, 3)] = 8.
(* Initializer *)
Init: Mint_0[shiftfield_F1_x(a_3)] = 10.
(* Initializer *)
@@ -260,7 +235,7 @@ Let a_4 = global(G_buint_37).
Let a_5 = shiftfield_F4_bytes(a_4).
Let a_6 = Load_S4(a_4, Mint_0).
Assume {
- Type: is_uint32(Mint_0[a_4]) /\ IsS4(a_6).
+ Type: IsS4(a_6).
(* Initializer *)
Init: Mint_0[shift_uint8(a_5, 0)] = 1.
(* Initializer *)
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 a5be47ac2193ae3620930ed953b31516bf056d01..225cf1c40b801ddb410faaf397268ef0e62ef1e3 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
@@ -1,17 +1,11 @@
-# frama-c -wp -wp-timeout 90 -wp-steps 1500 [...]
+# frama-c -wp -wp-timeout 90 -wp-steps 50 [...]
[kernel] Parsing tests/wp_acsl/logic.i (no preprocessing)
[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:
@@ -41,13 +35,13 @@
[wp] tests/wp_acsl/logic.i:62: Warning:
Logic cast to struct (Tint2) from (int [6]) not implemented yet
[wp] 21 goals scheduled
-[wp] [Alt-Ergo] Goal typed_h_ensures : Unsuccess (Stronger)
+[wp] [Qed] Goal typed_h_ensures : Valid
[wp] [Qed] Goal typed_h_assigns_exit : Valid
[wp] [Qed] Goal typed_h_assigns_normal : Valid
[wp] [Qed] Goal typed_main_requires_qed_ok : Valid
-[wp] [Alt-Ergo] Goal typed_main_requires_qed_ok_2 : Valid
-[wp] [Alt-Ergo] Goal typed_main_requires_qed_ok_3 : Valid
-[wp] [Alt-Ergo] Goal typed_main_requires_qed_ok_4 : Unsuccess (Stronger)
+[wp] [Alt-Ergo] Goal typed_main_requires_qed_ok_2 : Unsuccess
+[wp] [Alt-Ergo] Goal typed_main_requires_qed_ok_3 : Unsuccess
+[wp] [Alt-Ergo] Goal typed_main_requires_qed_ok_4 : Unsuccess
[wp] [Alt-Ergo] Goal typed_main_requires_qed_ok_5 : Unsuccess (Stronger)
[wp] [Alt-Ergo] Goal typed_main_requires_qed_ok_6 : Unsuccess (Stronger)
[wp] [Alt-Ergo] Goal typed_main_requires_qed_ok_7 : Unsuccess (Stronger)
@@ -62,13 +56,13 @@
[wp] [Alt-Ergo] Goal typed_main_requires_qed_ok_16 : Unsuccess (Stronger)
[wp] [Alt-Ergo] Goal typed_main_requires_qed_ok_17 : Unsuccess (Stronger)
[wp] [Alt-Ergo] Goal typed_main_requires_qed_ok_18 : Unsuccess (Stronger)
-[wp] Proved goals: 5 / 21
- Qed: 3
- Alt-Ergo: 2 (unsuccess: 16)
+[wp] Proved goals: 4 / 21
+ Qed: 4
+ Alt-Ergo: 0 (unsuccess: 17)
[wp] Report in: 'tests/wp_acsl/oracle_qualif/logic.0.report.json'
[wp] Report out: 'tests/wp_acsl/result_qualif/logic.0.report.json'
-------------------------------------------------------------
Functions WP Alt-Ergo Total Success
-h 2 - 3 66.7%
-main 1 2 (56..80) 18 16.7%
+h 3 - 3 100%
+main 1 - 18 5.6%
-------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_typed/cast_fits.i b/src/plugins/wp/tests/wp_typed/cast_fits.i
new file mode 100644
index 0000000000000000000000000000000000000000..8c0fcba18e0ea93237fea667cf06a76012ee0840
--- /dev/null
+++ b/src/plugins/wp/tests/wp_typed/cast_fits.i
@@ -0,0 +1,62 @@
+typedef struct { int i1; char c1; } L1 ;
+
+//@ ensures \result == p->i1;
+int fits1(L1 * p) {
+ int * q = (int *) p;
+ return *q;
+}
+
+typedef struct { char c2; int i2; } L2;
+
+//@ ensures \result == p->c2;
+int mismatch1(L2 * p) {
+ int * q = (int *) p;
+ return *q;
+}
+
+typedef struct { char c3; L1 ic3; int i3; } L3 ;
+
+//@ ensures \result == p->ic3.i1;
+int fits2(L3 * p) {
+ L2 * q = (L2 *) p;
+ return q->i2;
+}
+
+typedef struct { char c4; L1 ic4[2]; int i4; } L4 ;
+
+//@ ensures \result == p->ic4[0].i1;
+int fits3(L4 * p) {
+ L2 * q = (L2 *) p;
+ return q->i2;
+}
+
+typedef struct { L3 ci5[2]; } L5 ;
+
+typedef struct { L2 ci6[2]; char c6; } L6 ;
+
+//@ ensures \result == p->ci5[1].c3;
+int fits4(L5 * p) {
+ L6 * q = (L6 *) p;
+ return q->c6;
+}
+
+typedef union { int u7; } L7 ;
+
+//@ ensures \result == p->u7;
+int fits5(L7 * p) {
+ int * q = (int *) p;
+ return *q;
+}
+
+typedef union { int i8; char u8; double d8;} L8 ;
+//@ ensures \result == p->i8;
+int mismatch2(L8 * p) {
+ int * q = (int *) p;
+ return *q;
+}
+
+//@ ensures \result == *p;
+int mismatch3(int * p) {
+ L8 * q = (L8 *) p;
+ return q->i8;
+}
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
new file mode 100644
index 0000000000000000000000000000000000000000..56beccaf01fa52665901dd19e21253de0b119058
--- /dev/null
+++ b/src/plugins/wp/tests/wp_typed/oracle/cast_fits.0.res.oracle
@@ -0,0 +1,150 @@
+# frama-c -wp [...]
+[kernel] Parsing tests/wp_typed/cast_fits.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Loading driver 'share/wp.driver'
+[wp] Warning: Missing RTE guards
+[wp] tests/wp_typed/cast_fits.i:13: Warning:
+ Cast with incompatible pointers types (source: __anonstruct_L2_2*)
+ (target: sint32*)
+[wp] tests/wp_typed/cast_fits.i:54: Warning:
+ Cast with incompatible pointers types (source: __anonunion_L8_8*)
+ (target: sint32*)
+[wp] tests/wp_typed/cast_fits.i:60: Warning:
+ Cast with incompatible pointers types (source: sint32*)
+ (target: __anonunion_L8_8*)
+------------------------------------------------------------
+ Function fits1
+------------------------------------------------------------
+
+Goal Post-condition (file tests/wp_typed/cast_fits.i, line 3) in 'fits1':
+Let x = Mint_0[p].
+Let x_1 = Mint_0[shiftfield_F1_i1(p)].
+Assume {
+ Type: is_sint32(x) /\ is_sint32(x_1).
+ (* Heap *)
+ Have: region(p.base) <= 0.
+}
+Prove: x_1 = x.
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function fits2
+------------------------------------------------------------
+
+Goal Post-condition (file tests/wp_typed/cast_fits.i, line 19) in 'fits2':
+Let x = Mint_0[shiftfield_F2_i2(p)].
+Let x_1 = Mint_0[shiftfield_F1_i1(shiftfield_F3_ic3(p))].
+Assume {
+ Type: is_sint32(x) /\ is_sint32(x_1).
+ (* Heap *)
+ Have: region(p.base) <= 0.
+}
+Prove: x_1 = x.
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function fits3
+------------------------------------------------------------
+
+Goal Post-condition (file tests/wp_typed/cast_fits.i, line 27) in 'fits3':
+Let x = Mint_0[shiftfield_F2_i2(p)].
+Let x_1 = Mint_0
+ [shiftfield_F1_i1(shift___anonstruct_L1_1(shiftfield_F4_ic4(p),
+ 0))].
+Assume {
+ Type: is_sint32(x) /\ is_sint32(x_1).
+ (* Heap *)
+ Have: region(p.base) <= 0.
+}
+Prove: x_1 = x.
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function fits4
+------------------------------------------------------------
+
+Goal Post-condition (file tests/wp_typed/cast_fits.i, line 37) in 'fits4':
+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))].
+Assume {
+ Type: is_sint8(x) /\ is_sint32(x) /\ is_sint8(x_1).
+ (* Heap *)
+ Have: (region(p.base) <= 0) /\ sconst(Mchar_0).
+}
+Prove: x_1 = x.
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function fits5
+------------------------------------------------------------
+
+Goal Post-condition (file tests/wp_typed/cast_fits.i, line 45) in 'fits5':
+Let x = Mint_0[p].
+Let x_1 = Mint_0[shiftfield_F7_u7(p)].
+Assume {
+ Type: is_sint32(x) /\ is_sint32(x_1).
+ (* Heap *)
+ Have: region(p.base) <= 0.
+}
+Prove: x_1 = x.
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function mismatch1
+------------------------------------------------------------
+
+Goal Post-condition (file tests/wp_typed/cast_fits.i, line 11) in 'mismatch1':
+tests/wp_typed/cast_fits.i:13: warning from Typed Model:
+ - Warning: Hide sub-term definition
+ Reason: Cast with incompatible pointers types (source: __anonstruct_L2_2*)
+ (target: sint32*)
+Let x = Mint_0[q].
+Let x_1 = Mchar_0[shiftfield_F2_c2(p)].
+Assume {
+ Type: is_sint32(x) /\ is_sint8(x_1).
+ (* Heap *)
+ Have: (region(p.base) <= 0) /\ sconst(Mchar_0).
+}
+Prove: x_1 = x.
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function mismatch2
+------------------------------------------------------------
+
+Goal Post-condition (file tests/wp_typed/cast_fits.i, line 52) in 'mismatch2':
+tests/wp_typed/cast_fits.i:54: warning from Typed Model:
+ - Warning: Hide sub-term definition
+ Reason: Cast with incompatible pointers types (source: __anonunion_L8_8*)
+ (target: sint32*)
+Let x = Mint_0[q].
+Let x_1 = Mint_0[shiftfield_F8_i8(p)].
+Assume {
+ Type: is_sint32(x) /\ is_sint32(x_1).
+ (* Heap *)
+ Have: region(p.base) <= 0.
+}
+Prove: x_1 = x.
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function mismatch3
+------------------------------------------------------------
+
+Goal Post-condition (file tests/wp_typed/cast_fits.i, line 58) in 'mismatch3':
+tests/wp_typed/cast_fits.i:60: warning from Typed Model:
+ - Warning: Hide sub-term definition
+ Reason: Cast with incompatible pointers types (source: sint32*)
+ (target: __anonunion_L8_8*)
+Let x = Mint_0[p].
+Let x_1 = Mint_0[shiftfield_F8_i8(q)].
+Assume {
+ Type: is_sint32(x) /\ is_sint32(x_1).
+ (* Heap *)
+ Have: region(p.base) <= 0.
+}
+Prove: x_1 = x.
+
+------------------------------------------------------------
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
new file mode 100644
index 0000000000000000000000000000000000000000..cc8072d61ce0f259dd2e73a19b11d96f46c2512d
--- /dev/null
+++ b/src/plugins/wp/tests/wp_typed/oracle/cast_fits.1.res.oracle
@@ -0,0 +1,150 @@
+# frama-c -wp -wp-model 'Typed (Ref)' [...]
+[kernel] Parsing tests/wp_typed/cast_fits.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Loading driver 'share/wp.driver'
+[wp] Warning: Missing RTE guards
+[wp] tests/wp_typed/cast_fits.i:13: Warning:
+ Cast with incompatible pointers types (source: __anonstruct_L2_2*)
+ (target: sint32*)
+[wp] tests/wp_typed/cast_fits.i:54: Warning:
+ Cast with incompatible pointers types (source: __anonunion_L8_8*)
+ (target: sint32*)
+[wp] tests/wp_typed/cast_fits.i:60: Warning:
+ Cast with incompatible pointers types (source: sint32*)
+ (target: __anonunion_L8_8*)
+------------------------------------------------------------
+ Function fits1
+------------------------------------------------------------
+
+Goal Post-condition (file tests/wp_typed/cast_fits.i, line 3) in 'fits1':
+Let x = Mint_0[p].
+Let x_1 = Mint_0[shiftfield_F1_i1(p)].
+Assume {
+ Type: is_sint32(x) /\ is_sint32(x_1).
+ (* Heap *)
+ Have: region(p.base) <= 0.
+}
+Prove: x_1 = x.
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function fits2
+------------------------------------------------------------
+
+Goal Post-condition (file tests/wp_typed/cast_fits.i, line 19) in 'fits2':
+Let x = Mint_0[shiftfield_F2_i2(p)].
+Let x_1 = Mint_0[shiftfield_F1_i1(shiftfield_F3_ic3(p))].
+Assume {
+ Type: is_sint32(x) /\ is_sint32(x_1).
+ (* Heap *)
+ Have: region(p.base) <= 0.
+}
+Prove: x_1 = x.
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function fits3
+------------------------------------------------------------
+
+Goal Post-condition (file tests/wp_typed/cast_fits.i, line 27) in 'fits3':
+Let x = Mint_0[shiftfield_F2_i2(p)].
+Let x_1 = Mint_0
+ [shiftfield_F1_i1(shift___anonstruct_L1_1(shiftfield_F4_ic4(p),
+ 0))].
+Assume {
+ Type: is_sint32(x) /\ is_sint32(x_1).
+ (* Heap *)
+ Have: region(p.base) <= 0.
+}
+Prove: x_1 = x.
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function fits4
+------------------------------------------------------------
+
+Goal Post-condition (file tests/wp_typed/cast_fits.i, line 37) in 'fits4':
+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))].
+Assume {
+ Type: is_sint8(x) /\ is_sint32(x) /\ is_sint8(x_1).
+ (* Heap *)
+ Have: (region(p.base) <= 0) /\ sconst(Mchar_0).
+}
+Prove: x_1 = x.
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function fits5
+------------------------------------------------------------
+
+Goal Post-condition (file tests/wp_typed/cast_fits.i, line 45) in 'fits5':
+Let x = Mint_0[p].
+Let x_1 = Mint_0[shiftfield_F7_u7(p)].
+Assume {
+ Type: is_sint32(x) /\ is_sint32(x_1).
+ (* Heap *)
+ Have: region(p.base) <= 0.
+}
+Prove: x_1 = x.
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function mismatch1
+------------------------------------------------------------
+
+Goal Post-condition (file tests/wp_typed/cast_fits.i, line 11) in 'mismatch1':
+tests/wp_typed/cast_fits.i:13: warning from Typed Model:
+ - Warning: Hide sub-term definition
+ Reason: Cast with incompatible pointers types (source: __anonstruct_L2_2*)
+ (target: sint32*)
+Let x = Mint_0[q].
+Let x_1 = Mchar_0[shiftfield_F2_c2(p)].
+Assume {
+ Type: is_sint32(x) /\ is_sint8(x_1).
+ (* Heap *)
+ Have: (region(p.base) <= 0) /\ sconst(Mchar_0).
+}
+Prove: x_1 = x.
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function mismatch2
+------------------------------------------------------------
+
+Goal Post-condition (file tests/wp_typed/cast_fits.i, line 52) in 'mismatch2':
+tests/wp_typed/cast_fits.i:54: warning from Typed Model:
+ - Warning: Hide sub-term definition
+ Reason: Cast with incompatible pointers types (source: __anonunion_L8_8*)
+ (target: sint32*)
+Let x = Mint_0[q].
+Let x_1 = Mint_0[shiftfield_F8_i8(p)].
+Assume {
+ Type: is_sint32(x) /\ is_sint32(x_1).
+ (* Heap *)
+ Have: region(p.base) <= 0.
+}
+Prove: x_1 = x.
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function mismatch3
+------------------------------------------------------------
+
+Goal Post-condition (file tests/wp_typed/cast_fits.i, line 58) in 'mismatch3':
+tests/wp_typed/cast_fits.i:60: warning from Typed Model:
+ - Warning: Hide sub-term definition
+ Reason: Cast with incompatible pointers types (source: sint32*)
+ (target: __anonunion_L8_8*)
+Let x = Mint_0[p].
+Let x_1 = Mint_0[shiftfield_F8_i8(q)].
+Assume {
+ Type: is_sint32(x) /\ is_sint32(x_1).
+ (* Heap *)
+ Have: region(p.base) <= 0.
+}
+Prove: x_1 = x.
+
+------------------------------------------------------------
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
new file mode 100644
index 0000000000000000000000000000000000000000..193b5d5e58bebc238a27b6c45e343141affb683a
--- /dev/null
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/cast_fits.0.report.json
@@ -0,0 +1,94 @@
+{ "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 },
+ "wp:main": { "total": 1,
+ "valid": 1,
+ "rank": 6 } },
+ "wp:section": { "alt-ergo": { "total": 1,
+ "valid": 1,
+ "rank": 6 },
+ "wp:main": { "total": 1,
+ "valid": 1,
+ "rank": 6 } } },
+ "mismatch1": { "mismatch1_ensures": { "alt-ergo":
+ { "total": 1,
+ "unknown": 1 },
+ "wp:main":
+ { "total": 1,
+ "unknown": 1 } },
+ "wp:section": { "alt-ergo": { "total": 1,
+ "unknown": 1 },
+ "wp:main": { "total": 1,
+ "unknown": 1 } } },
+ "fits2": { "fits2_ensures": { "alt-ergo": { "total": 1,
+ "valid": 1,
+ "rank": 6 },
+ "wp:main": { "total": 1,
+ "valid": 1,
+ "rank": 6 } },
+ "wp:section": { "alt-ergo": { "total": 1,
+ "valid": 1,
+ "rank": 6 },
+ "wp:main": { "total": 1,
+ "valid": 1,
+ "rank": 6 } } },
+ "fits3": { "fits3_ensures": { "alt-ergo": { "total": 1,
+ "valid": 1,
+ "rank": 7 },
+ "wp:main": { "total": 1,
+ "valid": 1,
+ "rank": 7 } },
+ "wp:section": { "alt-ergo": { "total": 1,
+ "valid": 1,
+ "rank": 7 },
+ "wp:main": { "total": 1,
+ "valid": 1,
+ "rank": 7 } } },
+ "fits4": { "fits4_ensures": { "alt-ergo": { "total": 1,
+ "valid": 1,
+ "rank": 8 },
+ "wp:main": { "total": 1,
+ "valid": 1,
+ "rank": 8 } },
+ "wp:section": { "alt-ergo": { "total": 1,
+ "valid": 1,
+ "rank": 8 },
+ "wp:main": { "total": 1,
+ "valid": 1,
+ "rank": 8 } } },
+ "fits5": { "fits5_ensures": { "alt-ergo": { "total": 1,
+ "valid": 1,
+ "rank": 6 },
+ "wp:main": { "total": 1,
+ "valid": 1,
+ "rank": 6 } },
+ "wp:section": { "alt-ergo": { "total": 1,
+ "valid": 1,
+ "rank": 6 },
+ "wp:main": { "total": 1,
+ "valid": 1,
+ "rank": 6 } } },
+ "mismatch2": { "mismatch2_ensures": { "alt-ergo":
+ { "total": 1,
+ "unknown": 1 },
+ "wp:main":
+ { "total": 1,
+ "unknown": 1 } },
+ "wp:section": { "alt-ergo": { "total": 1,
+ "unknown": 1 },
+ "wp:main": { "total": 1,
+ "unknown": 1 } } },
+ "mismatch3": { "mismatch3_ensures": { "alt-ergo":
+ { "total": 1,
+ "unknown": 1 },
+ "wp:main":
+ { "total": 1,
+ "unknown": 1 } },
+ "wp:section": { "alt-ergo": { "total": 1,
+ "unknown": 1 },
+ "wp:main": { "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
new file mode 100644
index 0000000000000000000000000000000000000000..6bc88bcb22a2bf7acb1f1acca3ffc64da2dca480
--- /dev/null
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/cast_fits.res.oracle
@@ -0,0 +1,39 @@
+# frama-c -wp -wp-timeout 90 -wp-steps 1500 [...]
+[kernel] Parsing tests/wp_typed/cast_fits.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Loading driver 'share/wp.driver'
+[wp] Warning: Missing RTE guards
+[wp] tests/wp_typed/cast_fits.i:13: Warning:
+ Cast with incompatible pointers types (source: __anonstruct_L2_2*)
+ (target: sint32*)
+[wp] tests/wp_typed/cast_fits.i:54: Warning:
+ Cast with incompatible pointers types (source: __anonunion_L8_8*)
+ (target: sint32*)
+[wp] tests/wp_typed/cast_fits.i:60: Warning:
+ Cast with incompatible pointers types (source: sint32*)
+ (target: __anonunion_L8_8*)
+[wp] 8 goals scheduled
+[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 : 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: 5 / 8
+ Qed: 0
+ 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'
+-------------------------------------------------------------
+Functions WP Alt-Ergo Total Success
+fits1 - 1 (20..32) 1 100%
+mismatch1 - - 1 0.0%
+fits2 - 1 (20..32) 1 100%
+fits3 - 1 (24..36) 1 100%
+fits4 - 1 (28..40) 1 100%
+fits5 - 1 (20..32) 1 100%
+mismatch2 - - 1 0.0%
+mismatch3 - - 1 0.0%
+-------------------------------------------------------------