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

[ACSL] bug with the precedence of \in

parent 27ac101a
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 3 additions and 0 deletions
tests/spec/tsets.c
+ 3
− 0
View file @ 79ca5ef8
...@@ -68,3 +68,6 @@ int *AA(void); ...@@ -68,3 +68,6 @@ int *AA(void);
//@ logic set<integer> Sadd_elem_1(set<integer> s, integer e) = \union(s,e) ; //@ 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}) ; //@ 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 ;
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