From 51d9524a9b1967eb1118d3b9c8a5b2bd7226ae1e Mon Sep 17 00:00:00 2001 From: Christopher Pulte Date: Mon, 30 Jun 2025 14:45:21 +0100 Subject: [PATCH] fix predicate definition --- .../simple-examples/working/pred_2.c | 13 +++++++------ 1 file changed, 7 insertions(+), 6 deletions(-) diff --git a/src/example-archive/simple-examples/working/pred_2.c b/src/example-archive/simple-examples/working/pred_2.c index aba7b5e..211cb49 100644 --- a/src/example-archive/simple-examples/working/pred_2.c +++ b/src/example-archive/simple-examples/working/pred_2.c @@ -31,12 +31,6 @@ void pred_2_var1(int *p) // Variant 2 - this works: /*@ -predicate (i32) TestMemoryEqZero_2_var2(pointer p) { - take PVal = RW(p); - take rval = TestMemoryEqZero_2_Helper(p, PVal); - return rval; -} - predicate (i32) TestMemoryEqZero_2_Helper(pointer p, i32 x) { if (x == 0i32) { return 1i32; @@ -44,6 +38,13 @@ predicate (i32) TestMemoryEqZero_2_Helper(pointer p, i32 x) { return 0i32; } } + + +predicate (i32) TestMemoryEqZero_2_var2(pointer p) { + take PVal = RW(p); + take rval = TestMemoryEqZero_2_Helper(p, PVal); + return rval; +} @*/ void pred_2_var2(int *p)