use == instead of ptr_eq to compare u32 values (#83)

rems-project · Aug 28, 2024 · 8557ec5 · 8557ec5
1 parent fe2d682
commit 8557ec5
Showing 1 changed file with 2 additions and 4 deletions.
diff --git a/src/examples/slf_incr2.c b/src/examples/slf_incr2.c
@@ -16,10 +16,8 @@ predicate { u32 pv, u32 qv } BothOwned (pointer p, pointer q)
 void incr2 (unsigned int *p, unsigned int *q)
 /*@ requires take vs = BothOwned(p,q);
     ensures take vs_ = BothOwned(p,q);
-            ptr_eq (vs_.pv,
-                    (!ptr_eq(p,q)) ? (vs.pv + 1u32) : (vs.pv + 2u32));
-            ptr_eq (vs_.qv,
-                    (!ptr_eq(p,q)) ? (vs.qv + 1u32) : vs_.pv);
+            vs_.pv == (!ptr_eq(p,q) ? (vs.pv + 1u32) : (vs.pv + 2u32));
+            vs_.qv == (!ptr_eq(p,q) ? (vs.qv + 1u32) : vs_.pv);
 @*/
 {
   /*@ split_case ptr_eq(p,q); @*/