From 6a3d36ae8ae304818e7b242bb49c77b7a417a13b Mon Sep 17 00:00:00 2001
From: Patrick Baudin <patrick.baudin@cea.fr>
Date: Mon, 10 Feb 2020 14:02:15 +0100
Subject: [PATCH] [wp] more tests for issue 751
---
src/plugins/wp/tests/wp_bts/issue_751.i | 29 +++++++++++++++++++++++++
1 file changed, 29 insertions(+)
diff --git a/src/plugins/wp/tests/wp_bts/issue_751.i b/src/plugins/wp/tests/wp_bts/issue_751.i
index 35486922525..0032c1b3a36 100644
--- a/src/plugins/wp/tests/wp_bts/issue_751.i
+++ b/src/plugins/wp/tests/wp_bts/issue_751.i
@@ -13,3 +13,32 @@ void acquire(int R,int Nb,int * Data)
}
}
}
+
+/*@ requires pos_max: k>0 && (0 <= a || 0 <= b) ==> ( a/k <= b <==> a < b*k + k ) ;
+ @ requires neg_max: k>0 && (a <= 0 || b < 0) ==> ( a/k <= b <==> a <= b*k ) ;
+ @ requires pos_min: k>0 && (0 <= a || 0 < b) ==> ( b <= a/k <==> b*k <= a ) ;
+ @ requires neg_min: k>0 && (a <= 0 || b <= 0) ==> ( b <= a/k <==> b*k - k < a ) ;
+ @ requires strict_pos_max: k>0 && (0 <= a || 0 < b) ==> ( a/k < b <==> a < b*k ) ;
+ @ requires strict_neg_max: k>0 && (a <= 0 || b <= 0) ==> ( a/k < b <==> a <= b*k - k );
+ @ requires strict_pos_min: k>0 && (0 <= a || 0 <= b) ==> ( b < a/k <==> b*k + k <= a );
+ @ requires strict_neg_min: k>0 && (a <= 0 || b < 0) ==> ( b < a/k <==> b*k < a ) ;
+ @ assigns \nothing;
+*/
+int checks (int a, int b, int k) ;
+
+int issue_751(int V)
+{ int n = 2;
+ int k = 1<<n;
+ //@ check (V >> n) <= 16 <==> V < 16*k + k;
+ //@ check (V >> n) <= -16 <==> V <= -16*k;
+ //@ check 16 <= (V >> n) <==> 16*k <= V;
+ //@ check -16 <= (V >> n) <==> -16*k - k < V;
+
+ checks ( 21, V, 3);
+ checks (-27, V, 7);
+
+ checks (V, 5, 19);
+ checks (V, -7, 23);
+
+ return V;
+}
--
GitLab