From c965f4e1ba2a1951d6b2bb0511a8197ff92583e8 Mon Sep 17 00:00:00 2001
From: Patrick Baudin <patrick.baudin@cea.fr>
Date: Wed, 19 Jun 2019 13:22:50 +0200
Subject: [PATCH] [ACSL] bug with the precedence of \in
---
tests/spec/tsets.c | 10 ++++++++--
1 file changed, 8 insertions(+), 2 deletions(-)
diff --git a/tests/spec/tsets.c b/tests/spec/tsets.c
index 61d8e7f4689..12a6f9763b7 100644
--- a/tests/spec/tsets.c
+++ b/tests/spec/tsets.c
@@ -68,6 +68,12 @@ int *AA(void);
//@ logic set<integer> Sadd_elem_1(set<integer> s, integer e) = \union(s,e) ;
//@ logic set<integer> Sadd_elem_2(set<integer> s, integer e) = \union(s,{e}) ;
-//@ predicate Smember_and(set<integer> s, integer v1, integer v2) = v1 & v2 \in s ;
-//@ predicate Smember_or (set<integer> s, integer v1, integer v2) = v1 | v2 \in s ;
+//@ predicate rejected_Smember_and(set<integer> s, integer v1, integer v2) = v1 & v2 \in s ;
+//@ predicate rejected_Smember_or (set<integer> s, integer v1, integer v2) = v1 | v2 \in s ;
+//@ predicate rejected_Smember_and_or (set<integer> s, integer v1, integer v2) = v1 & v2 \in s && v1 | v2 \in s ;
+//@ predicate Smember_and(set<integer> s, integer v1, integer v2) = (v1 & v2) \in s ;
+//@ predicate Smember_or (set<integer> s, integer v1, integer v2) = (v1 | v2) \in s ;
+//@ predicate Smember_and_or (set<integer> s, integer v1, integer v2) = (v1 & v2) \in s && (v1 | v2) \in s ;
+
+//@ logic set<integer> Scomprehension(set<integer> s, integer mask ) = { (k | 1) | int k ; (k | mask) \in s };
--
GitLab