From 8557ec52f75423e54a465e5685d1d9d48a7b5127 Mon Sep 17 00:00:00 2001 From: Daniel Sainati Date: Wed, 28 Aug 2024 12:50:44 -0400 Subject: [PATCH] use == instead of ptr_eq to compare u32 values (#83) --- src/examples/slf_incr2.c | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/src/examples/slf_incr2.c b/src/examples/slf_incr2.c index 94de75c6..cd4b9c23 100644 --- 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); @*/