From 12b43205c813202e65e56a5652dd55d057b32dc8 Mon Sep 17 00:00:00 2001
From: Patrick Baudin <patrick.baudin@cea.fr>
Date: Thu, 20 Jan 2022 09:37:34 +0100
Subject: [PATCH] [WP] fixes Cint.is_positive_or_null about modulo
---
src/plugins/wp/Cint.ml | 10 +++++++++-
src/plugins/wp/tests/wp_acsl/bitwise.i | 2 +-
2 files changed, 10 insertions(+), 2 deletions(-)
diff --git a/src/plugins/wp/Cint.ml b/src/plugins/wp/Cint.ml
index 16c04fc09ca..b2f0dd887bc 100644
--- a/src/plugins/wp/Cint.ml
+++ b/src/plugins/wp/Cint.ml
@@ -136,6 +136,12 @@ let match_mod t =
| Logic.Mod (e1, e2) -> e1, e2
| _ -> raise Not_found
+(* integration with qed should be improved! *)
+let is_positive t =
+ match F.repr t with
+ | Logic.Kint c -> Integer.le Integer.one c
+ | _ -> false
+
(* integration with qed should be improved! *)
let rec is_positive_or_null e = match F.repr e with
| Logic.Fun( f , [e] ) when Fun.equal f f_lnot -> is_negative e
@@ -147,7 +153,9 @@ let rec is_positive_or_null e = match F.repr e with
| _ -> (* try some improvement first then ask to qed *)
let improved_is_positive_or_null e = match F.repr e with
| Logic.Add es -> List.for_all is_positive_or_null es
- | Logic.Mod(e1,_) -> is_positive_or_null e1
+ | Logic.Mod(e1,e2) when is_positive e2 || is_negative e2 ->
+ (* e2<>0 ==> ( 0<=(e1 % e2) <=> 0<=e1 ) *)
+ is_positive_or_null e1
| _ -> false
in if improved_is_positive_or_null e then true
else match F.is_true (F.e_leq e_zero e) with
diff --git a/src/plugins/wp/tests/wp_acsl/bitwise.i b/src/plugins/wp/tests/wp_acsl/bitwise.i
index b2e5594f270..931ba45bd5a 100644
--- a/src/plugins/wp/tests/wp_acsl/bitwise.i
+++ b/src/plugins/wp/tests/wp_acsl/bitwise.i
@@ -115,7 +115,7 @@ void lemma(unsigned a, unsigned b, unsigned k) {
/* note: a5 is not simplified because Qed cannot infer that a&b is positive
*/
- //@ check ( a & (85 % b) & 0xFF ) == ( (a & (85 % b)) % 0x100 );
+ //@ check ( a & ((b & 0xFFFF) % 55) & 0xFF ) == ( (a & ((b & 0xFFFF) % 55)) % 0x100 );
//@ check zbit: a5: ( a & b & 77 & ((1 << k)-1) ) == ( (a & b & 77) % (1 << k) );
/* note: a4 is not simplified because Qed cannot infer that k is positive
--
GitLab