From 8ad5c2876974d1f876c0bc4a2f490d051e20cbb0 Mon Sep 17 00:00:00 2001
From: Patrick Baudin <patrick.baudin@cea.fr>
Date: Mon, 25 Mar 2019 16:39:32 +0100
Subject: [PATCH] [WP] detection of non significative casts (from/to the same
array type)
---
src/plugins/wp/LogicSemantics.ml | 4 ++++
1 file changed, 4 insertions(+)
diff --git a/src/plugins/wp/LogicSemantics.ml b/src/plugins/wp/LogicSemantics.ml
index 8f0c5dd0358..9deb0c43059 100644
--- a/src/plugins/wp/LogicSemantics.ml
+++ b/src/plugins/wp/LogicSemantics.ml
@@ -543,6 +543,10 @@ struct
to a deref of a cast to a pointer `*(T( * )[])(p)` *)
let cast = cast_ptr dst_ctype t0 in
L.load (C.current env) (Ctypes.object_of dst_ctype) cast
+ | C_array dst_arr_info, L_array src_arr_info
+ when Ctypes.AinfoComparable.equal dst_arr_info src_arr_info ->
+ (* cast from/to the same type *)
+ C.logic env t
| C_array {arr_flat=Some _}, (L_integer|L_cint _|L_bool|L_real|L_cfloat _|L_array _) ->
Warning.error "@[Logic cast to sized array (%a) from (%a) not implemented yet@]"
Printer.pp_typ dst_ctype Printer.pp_logic_type t.term_type
--
GitLab