Skip to content
Snippets Groups Projects
Commit 3c0bc02a authored by Patrick Baudin's avatar Patrick Baudin
Browse files

[wp] better fitting detection for C casts (source: T target:T[N])

parent 6be3084d
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
src/plugins/wp/MemTyped.ml
+ 43
− 8
View file @ 3c0bc02a
......@@ -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)
......
src/plugins/wp/tests/wp_acsl/oracle/logic.res.oracle
+ 0
− 22
View file @ 3c0bc02a
......@@ -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).
......
src/plugins/wp/tests/wp_acsl/oracle_qualif/logic.0.report.json
+ 15
− 17
View file @ 3c0bc02a
{ "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 } } } } }
src/plugins/wp/tests/wp_acsl/oracle_qualif/logic.res.oracle
+ 1
− 7
View file @ 3c0bc02a
......@@ -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)
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment