From a7ad23171344d5e06b9c1f84d6ec3841c684883e Mon Sep 17 00:00:00 2001 From: Dhruv Makwana Date: Wed, 12 Mar 2025 18:45:49 +0000 Subject: [PATCH 1/2] Update deprecated keywords Owned -> RW Block -> W extract -> focus rems-project/cerberus#854 (commit 0832c78) deprecated some keywords in favour of new replacements and this commit updates the tutorial examples to use them to be less noisy in the CI. The tutorial docs also need to be updated. --- .../error-proof/00004-simple-lifetimes.c | 8 ++--- .../error-proof/00006-lifetimes-broken.c | 4 +-- .../SAW/broken/error-cerberus/00001.swap.c | 30 ++++++++--------- .../SAW/broken/error-proof/00003.point.c | 32 +++++++++---------- .../error-proof/00004.tutorial-dotprod.c | 14 ++++---- .../broken/error-proof/00077.err1.c | 6 ++-- .../broken/error-timeout/00182.timeout.c | 2 +- .../c-testsuite/working/00015.working.c | 4 +-- .../c-testsuite/working/00016.working.c | 2 +- .../c-testsuite/working/00032.c | 4 +-- .../c-testsuite/working/00033.working.c | 8 ++--- .../c-testsuite/working/00037.working.c | 2 +- .../c-testsuite/working/00072.working.c | 2 +- .../c-testsuite/working/00078.working.c | 4 +-- .../c-testsuite/working/00090.working.c | 6 ++-- .../dafny-tutorial/working/binary_search.c | 8 ++--- .../dafny-tutorial/working/linear_search.c | 8 ++--- .../dafny-tutorial/working/multiple_returns.c | 4 +-- .../00008_overload_dyn_method.c | 12 +++---- .../broken/error-proof/00002_side_effects.c | 8 ++--- .../broken/error-proof/00003_break.c | 4 +-- .../broken/error-proof/00006_callbacks.c | 8 ++--- .../broken/error-proof/00007_static_init.c | 8 ++--- .../working/00004_exceptions.c | 8 ++--- src/example-archive/open-sut/working/mps_1.c | 16 +++++----- .../broken/error-proof/ownership_neg_1.c | 4 +-- .../broken/error-proof/ownership_neg_2.c | 4 +-- .../broken/error-proof/ownership_neg_3.c | 8 ++--- .../should-fail/working/c_sequencing_race.c | 4 +-- .../broken/error-cerberus/pred_1.c | 4 +-- .../broken/error-proof/ownership_1.c | 6 ++-- .../error-timeout/overflow_timeout_3var.c | 8 ++--- .../error-timeout/overflow_timeout_4var.c | 8 ++--- .../simple-examples/working/array_1.c | 6 ++-- .../simple-examples/working/array_2.c | 6 ++-- .../simple-examples/working/array_3.c | 8 ++--- .../simple-examples/working/array_read.c | 8 ++--- .../simple-examples/working/assert_2.c | 8 ++--- .../simple-examples/working/assert_3.c | 12 +++---- .../simple-examples/working/cast_4.c | 4 +-- .../simple-examples/working/cn_function_1.c | 2 +- .../simple-examples/working/effect_1.c | 8 ++--- .../simple-examples/working/free_1.c | 8 ++--- .../simple-examples/working/list_2.c | 2 +- .../simple-examples/working/list_3.c | 4 +-- .../simple-examples/working/malloc_1.c | 4 +-- .../simple-examples/working/pred_2.c | 12 +++---- .../simple-examples/working/struct_1.c | 4 +-- .../simple-examples/working/swap_1.c | 8 ++--- .../simple-examples/working/write_1.c | 4 +-- .../simple-examples/working/write_2.c | 8 ++--- .../simple-examples/working/write_3.c | 4 +-- .../simple-examples/working/write_4.c | 8 ++--- .../simple-examples/working/write_5.c | 16 +++++----- src/examples/abs_mem.c | 4 +-- src/examples/abs_mem_struct.c | 8 ++--- src/examples/add_read.c | 8 ++--- src/examples/add_two_array.c | 8 ++--- src/examples/array_load.broken.c | 4 +-- src/examples/array_load.c | 6 ++-- src/examples/array_load2.c | 6 ++-- src/examples/bcp_framerule.c | 12 +++---- src/examples/dll/remove.c | 2 +- src/examples/init_array.c | 8 ++--- src/examples/init_array2.c | 12 +++---- src/examples/init_array_rev.c | 12 +++---- src/examples/init_point.c | 8 ++--- src/examples/queue/pop_unified.c | 6 ++-- src/examples/queue/push_induction.c | 6 ++-- src/examples/read.broken.c | 2 +- src/examples/read.c | 4 +-- src/examples/read2.c | 4 +-- src/examples/slf0_basic_incr.c | 4 +-- src/examples/slf0_basic_incr.signed.broken.c | 4 +-- src/examples/slf0_basic_incr.signed.c | 4 +-- src/examples/slf0_incr.broken.c | 4 +-- src/examples/slf10_basic_ref.c | 2 +- src/examples/slf11_basic_ref_greater.c | 6 ++-- .../slf12_basic_ref_greater_abstract.c | 6 ++-- src/examples/slf13_basic_ref_with_frame.c | 6 ++-- src/examples/slf17_get_and_free.c | 2 +- src/examples/slf3_basic_inplace_double.c | 4 +-- src/examples/slf4_basic_incr_two.c | 8 ++--- src/examples/slf5_basic_aliased_call.broken.c | 4 +-- .../slf6_basic_incr_two_aliased_call.c | 8 ++--- src/examples/slf7_basic_incr_first.c | 12 +++---- src/examples/slf8_basic_transfer.c | 8 ++--- src/examples/slf9_basic_transfer_aliased.c | 4 +-- src/examples/slf_incr2.c | 20 ++++++------ src/examples/slf_incr2_alias.c | 20 ++++++------ src/examples/slf_incr2_noalias.c | 8 ++--- src/examples/slf_length_acc.c | 4 +-- src/examples/slf_quadruple_mem.c | 4 +-- src/examples/slf_ref_greater.c | 6 ++-- src/examples/slf_sized_stack.c | 6 ++-- src/examples/swap.c | 8 ++--- src/examples/swap_array.c | 8 ++--- src/examples/transpose.broken.c | 4 +-- src/examples/transpose.c | 4 +-- src/examples/transpose2.c | 12 +++---- src/examples/zero.c | 4 +-- src/underconstruction/bst/getter.c | 16 +++++----- 102 files changed, 366 insertions(+), 366 deletions(-) diff --git a/src/example-archive/Rust/broken/error-proof/00004-simple-lifetimes.c b/src/example-archive/Rust/broken/error-proof/00004-simple-lifetimes.c index 169400d4..8a8154a7 100644 --- a/src/example-archive/Rust/broken/error-proof/00004-simple-lifetimes.c +++ b/src/example-archive/Rust/broken/error-proof/00004-simple-lifetimes.c @@ -5,8 +5,8 @@ is inside the scope of `x` so things work out. However the lifetime usage is not very interesting. - BROKEN PROOF: The proof goes through by replacing the Blocks with - Owneds works. But that's not the right spec for borrow! + BROKEN PROOF: The proof goes through by replacing the Ws with + RWs works. But that's not the right spec for borrow! How to prove this if, for example, borrow was a library call with that given spec? @@ -30,8 +30,8 @@ fn borrow<'a>(input: &'a i32) -> &'a i32 { // Function to "borrow" an integer pointer int* borrow(int* input) - /*@ requires take v1 = Block(input); - ensures take v2 = Block(input); + /*@ requires take v1 = W(input); + ensures take v2 = W(input); return == input; @*/ { diff --git a/src/example-archive/Rust/broken/error-proof/00006-lifetimes-broken.c b/src/example-archive/Rust/broken/error-proof/00006-lifetimes-broken.c index e6f3b6dc..1b8d8f95 100644 --- a/src/example-archive/Rust/broken/error-proof/00006-lifetimes-broken.c +++ b/src/example-archive/Rust/broken/error-proof/00006-lifetimes-broken.c @@ -32,8 +32,8 @@ fn borrow<'a>(input: &'a i32) -> &'a i32 { int global_int = 0; int* borrow(const int* input) - /*@ requires take v1 = Owned(input); - ensures take v2 = Owned(input); + /*@ requires take v1 = RW(input); + ensures take v2 = RW(input); return == input; @*/ { diff --git a/src/example-archive/SAW/broken/error-cerberus/00001.swap.c b/src/example-archive/SAW/broken/error-cerberus/00001.swap.c index d9ceae6b..19384c19 100644 --- a/src/example-archive/SAW/broken/error-cerberus/00001.swap.c +++ b/src/example-archive/SAW/broken/error-cerberus/00001.swap.c @@ -140,10 +140,10 @@ llvm_verify swapmod "wacky_sort" #include void swap(uint32_t *x, uint32_t *y) -/*@ requires take xv0 = Owned(x); - take yv0 = Owned(y); - ensures take xv1 = Owned(x); - take yv1 = Owned(y); +/*@ requires take xv0 = RW(x); + take yv0 = RW(y); + ensures take xv1 = RW(x); + take yv1 = RW(y); xv1 == yv0; yv1 == xv0; @*/ @@ -154,10 +154,10 @@ void swap(uint32_t *x, uint32_t *y) } void xor_swap(uint32_t *x, uint32_t *y) -/*@ requires take xv0 = Owned(x); - take yv0 = Owned(y); - ensures take xv1 = Owned(x); - take yv1 = Owned(y); +/*@ requires take xv0 = RW(x); + take yv0 = RW(y); + ensures take xv1 = RW(x); + take yv1 = RW(y); xv1 == yv0; yv1 == xv0; @*/ @@ -169,22 +169,22 @@ void xor_swap(uint32_t *x, uint32_t *y) // selection sort void selection_sort(uint32_t *a, size_t len) -/*@ requires take av0 = each(size_t j; 0u64 <= j && j < len) { Owned(array_shift(a,j)) }; - ensures take av1 = each(size_t j; 0u64 <= j && j < len) { Owned(array_shift(a,j)) }; +/*@ requires take av0 = each(size_t j; 0u64 <= j && j < len) { RW(array_shift(a,j)) }; + ensures take av1 = each(size_t j; 0u64 <= j && j < len) { RW(array_shift(a,j)) }; @*/ { for (size_t i = 0; i < len - 1; ++i) - /*@ inv take avl = each(u64 k; 0u64 <= k && k < i) { Owned(array_shift(a,k)) }; - take avr = each(u64 k; i <= k && k < len) { Owned(array_shift(a,k)) } ; + /*@ inv take avl = each(u64 k; 0u64 <= k && k < i) { RW(array_shift(a,k)) }; + take avr = each(u64 k; i <= k && k < len) { RW(array_shift(a,k)) } ; {a} unchanged; {len} unchanged; i <= len; @*/ { size_t j_min = i; for (size_t j = i; j < len; ++j) - /*@ inv take avl = each(u64 k; 0u64 <= k && k < i) { Owned(array_shift(a,k)) }; - take avr = each(u64 k; i <= k && k < j) { Owned(array_shift(a,k)) }; - take avr = each(u64 k; j <= k && k < len) { Owned(array_shift(a,k)) }; + /*@ inv take avl = each(u64 k; 0u64 <= k && k < i) { RW(array_shift(a,k)) }; + take avr = each(u64 k; i <= k && k < j) { RW(array_shift(a,k)) }; + take avr = each(u64 k; j <= k && k < len) { RW(array_shift(a,k)) }; {a} unchanged; {len} unchanged; j <= len; @*/ diff --git a/src/example-archive/SAW/broken/error-proof/00003.point.c b/src/example-archive/SAW/broken/error-proof/00003.point.c index 0ed4341e..7f478dfd 100644 --- a/src/example-archive/SAW/broken/error-proof/00003.point.c +++ b/src/example-archive/SAW/broken/error-proof/00003.point.c @@ -101,10 +101,10 @@ point ZERO = {0, 0}; // Check whether two points are equal bool point_eq(const point *p1, const point *p2) -/*@ requires take vp10 = Owned(p1); - take vp20 = Owned(p2); - ensures take vp11 = Owned(p1); - take vp21 = Owned(p2); +/*@ requires take vp10 = RW(p1); + take vp20 = RW(p2); + ensures take vp11 = RW(p1); + take vp21 = RW(p2); vp10 == vp11 ; vp20 == vp21; if (vp11.x == vp21.x && vp11.y == vp21.x) { return == 1u8 @@ -118,13 +118,13 @@ bool point_eq(const point *p1, const point *p2) /*@ spec malloc(); requires true; - ensures take v = Block(return); + ensures take v = W(return); @*/ // Allocate and return a new point point* point_new(uint32_t x, uint32_t y) /*@ requires true; - ensures take vp1 = Owned(return); + ensures take vp1 = RW(return); vp1.x == x ; vp1.y == y; @*/ { @@ -136,9 +136,9 @@ point* point_new(uint32_t x, uint32_t y) // Return a new point containing a copy of `p` point* point_copy(const point* p) -/*@ requires take vp0 = Owned(p); - ensures take vp1 = Owned(p); - take vr1 = Owned(return); +/*@ requires take vp0 = RW(p); + ensures take vp1 = RW(p); + take vr1 = RW(return); vp0.x == vp1.x ; vp0.y == vp1.y; vr1.x == vp1.x ; vr1.y == vp1.y; @*/ @@ -148,14 +148,14 @@ point* point_copy(const point* p) // Add two points point* point_add(const point *p1, const point *p2) -/*@ requires take vp10 = Owned(p1); - take vp20 = Owned(p2); - take vZ0 = Owned(&ZERO); +/*@ requires take vp10 = RW(p1); + take vp20 = RW(p2); + take vZ0 = RW(&ZERO); vZ0.x == 0u32 ; vZ0.y == 0u32; - ensures take vp11 = Owned(p1); - take vp21 = Owned(p2); - take vZ1 = Owned(&ZERO); - take vr1 = Owned(return); + ensures take vp11 = RW(p1); + take vp21 = RW(p2); + take vZ1 = RW(&ZERO); + take vr1 = RW(return); vr1.x == vp11.x + vp21.x ; vr1.y == vp11.y + vp21.y; @*/ { diff --git a/src/example-archive/SAW/broken/error-proof/00004.tutorial-dotprod.c b/src/example-archive/SAW/broken/error-proof/00004.tutorial-dotprod.c index f275e693..17f8320e 100644 --- a/src/example-archive/SAW/broken/error-proof/00004.tutorial-dotprod.c +++ b/src/example-archive/SAW/broken/error-proof/00004.tutorial-dotprod.c @@ -48,10 +48,10 @@ function [rec] (u32) dotprod_spec(map x,map y, uint32_t size @*/ uint32_t dotprod(uint32_t *x, uint32_t *y, uint32_t size) -/*@ requires take ax0 = each(u32 j; 0u32 <= j && j < size) { Owned(array_shift(x,j)) }; - take ay0 = each(u32 j; 0u32 <= j && j < size) { Owned(array_shift(y,j)) } - ensures take ax1 = each(u32 j; 0u32 <= j && j < size) { Owned(array_shift(x,j)) }; - take ay1 = each(u32 j; 0u32 <= j && j < size) { Owned(array_shift(y,j)) }; +/*@ requires take ax0 = each(u32 j; 0u32 <= j && j < size) { RW(array_shift(x,j)) }; + take ay0 = each(u32 j; 0u32 <= j && j < size) { RW(array_shift(y,j)) } + ensures take ax1 = each(u32 j; 0u32 <= j && j < size) { RW(array_shift(x,j)) }; + take ay1 = each(u32 j; 0u32 <= j && j < size) { RW(array_shift(y,j)) }; return == dotprod_spec(ax1,ay1,size) @*/ { @@ -59,14 +59,14 @@ uint32_t dotprod(uint32_t *x, uint32_t *y, uint32_t size) /*@ unfold dotprod_spec(ax0,ay0,0u32); @*/ /*@ assert(0u32 == dotprod_spec(ax0,ay0,0u32)); @*/ for(size_t i = 0; i < size; i++) - /*@ inv take axi = each(u32 j; 0u32 <= j && j < size) { Owned(array_shift(x,j)) }; - take ayi = each(u32 j; 0u32 <= j && j < size) { Owned(array_shift(y,j)) }; + /*@ inv take axi = each(u32 j; 0u32 <= j && j < size) { RW(array_shift(x,j)) }; + take ayi = each(u32 j; 0u32 <= j && j < size) { RW(array_shift(y,j)) }; {x} unchanged; {y} unchanged; 0u64<=i; res == dotprod_spec(axi,ayi,(u32)i) @*/ { - /*@ extract Owned, i; @*/ + /*@ focus RW, i; @*/ res += x[i] * y[i]; /*@ unfold dotprod_spec(axi,ayi,(u32)i); @*/ } diff --git a/src/example-archive/c-testsuite/broken/error-proof/00077.err1.c b/src/example-archive/c-testsuite/broken/error-proof/00077.err1.c index 9f98f52c..963b79d4 100644 --- a/src/example-archive/c-testsuite/broken/error-proof/00077.err1.c +++ b/src/example-archive/c-testsuite/broken/error-proof/00077.err1.c @@ -3,12 +3,12 @@ int foo(int x[100]) /*@ requires - take PreX = each (u64 j; 0u64 <= j && j < 100u64) {Owned(x + j)}; @*/ + take PreX = each (u64 j; 0u64 <= j && j < 100u64) {RW(x + j)}; @*/ { int y[100]; int *p; - /*@ extract Block, 0u64; @*/ + /*@ focus W, 0u64; @*/ y[0] = 2000; if(x[0] != 1000) @@ -49,7 +49,7 @@ main() { int x[100]; assert(0); - /*@ extract Block, 0u64; @*/ + /*@ focus W, 0u64; @*/ x[0] = 1000; return foo(x); diff --git a/src/example-archive/c-testsuite/broken/error-timeout/00182.timeout.c b/src/example-archive/c-testsuite/broken/error-timeout/00182.timeout.c index 5596cbfd..33cb9ee8 100644 --- a/src/example-archive/c-testsuite/broken/error-timeout/00182.timeout.c +++ b/src/example-archive/c-testsuite/broken/error-timeout/00182.timeout.c @@ -182,7 +182,7 @@ void print_led(unsigned long x, char *buf) static int d[MAX_DIGITS]; - /* extract digits from x */ + /* focus digits from x */ n = ( x == 0L ? 1 : 0 ); /* 0 is a digit, hence a special case */ diff --git a/src/example-archive/c-testsuite/working/00015.working.c b/src/example-archive/c-testsuite/working/00015.working.c index 2259a5ae..20208686 100644 --- a/src/example-archive/c-testsuite/working/00015.working.c +++ b/src/example-archive/c-testsuite/working/00015.working.c @@ -4,9 +4,9 @@ main() { int arr[2]; - /*@ extract Block, 0u64; @*/ + /*@ focus W, 0u64; @*/ arr[0] = 1; - /*@ extract Block, 1u64; @*/ + /*@ focus W, 1u64; @*/ arr[1] = 2; return arr[0] + arr[1] - 3; diff --git a/src/example-archive/c-testsuite/working/00016.working.c b/src/example-archive/c-testsuite/working/00016.working.c index 7d9ae877..c02b8df3 100644 --- a/src/example-archive/c-testsuite/working/00016.working.c +++ b/src/example-archive/c-testsuite/working/00016.working.c @@ -5,7 +5,7 @@ main() int arr[2]; int *p; - /*@ extract Block, 1u64; @*/ + /*@ focus W, 1u64; @*/ p = &arr[1]; *p = 0; return arr[1]; diff --git a/src/example-archive/c-testsuite/working/00032.c b/src/example-archive/c-testsuite/working/00032.c index 1867ba73..6d2462ca 100644 --- a/src/example-archive/c-testsuite/working/00032.c +++ b/src/example-archive/c-testsuite/working/00032.c @@ -7,9 +7,9 @@ main() int arr[2]; int *p; - /*@ extract Block, 0u64; @*/ + /*@ focus W, 0u64; @*/ arr[0] = 2; - /*@ extract Block, 1u64; @*/ + /*@ focus W, 1u64; @*/ arr[1] = 3; p = &arr[0]; if(*(p++) != 2) diff --git a/src/example-archive/c-testsuite/working/00033.working.c b/src/example-archive/c-testsuite/working/00033.working.c index 15f73962..f47f648e 100644 --- a/src/example-archive/c-testsuite/working/00033.working.c +++ b/src/example-archive/c-testsuite/working/00033.working.c @@ -3,9 +3,9 @@ int g; int effect() /*@ requires - take Pre = Owned(&g); @*/ + take Pre = RW(&g); @*/ /*@ ensures - take Post = Owned(&g); + take Post = RW(&g); Post == 1i32; return == 1i32; @*/ { @@ -16,9 +16,9 @@ effect() int main() /*@ requires - take Pre = Owned(&g); @*/ + take Pre = RW(&g); @*/ /*@ ensures - take Post = Owned(&g); @*/ + take Post = RW(&g); @*/ /*@ ensures return == 0i32; @*/ { int x; diff --git a/src/example-archive/c-testsuite/working/00037.working.c b/src/example-archive/c-testsuite/working/00037.working.c index 6a854eea..5840aa47 100644 --- a/src/example-archive/c-testsuite/working/00037.working.c +++ b/src/example-archive/c-testsuite/working/00037.working.c @@ -4,7 +4,7 @@ main() { int x[2]; int *p; - /*@ extract Block, 1u64; @*/ + /*@ focus W, 1u64; @*/ x[1] = 7; p = &x[0]; p = p + 1; diff --git a/src/example-archive/c-testsuite/working/00072.working.c b/src/example-archive/c-testsuite/working/00072.working.c index 998cef86..34ee6500 100644 --- a/src/example-archive/c-testsuite/working/00072.working.c +++ b/src/example-archive/c-testsuite/working/00072.working.c @@ -4,7 +4,7 @@ main() { int arr[2]; int *p; - /*@ extract Block, 1u64; @*/ + /*@ focus W, 1u64; @*/ p = &arr[0]; p += 1; *p = 123; diff --git a/src/example-archive/c-testsuite/working/00078.working.c b/src/example-archive/c-testsuite/working/00078.working.c index 1ffc92c5..90678dea 100644 --- a/src/example-archive/c-testsuite/working/00078.working.c +++ b/src/example-archive/c-testsuite/working/00078.working.c @@ -1,9 +1,9 @@ int f1(char *p) /*@ requires - take PreP = Owned(p); @*/ + take PreP = RW(p); @*/ /*@ ensures - take PostP = Owned(p); + take PostP = RW(p); return == 1i32 + (i32) PreP; @*/ { return *p+1; diff --git a/src/example-archive/c-testsuite/working/00090.working.c b/src/example-archive/c-testsuite/working/00090.working.c index f4ff0a4d..f9e29452 100644 --- a/src/example-archive/c-testsuite/working/00090.working.c +++ b/src/example-archive/c-testsuite/working/00090.working.c @@ -12,9 +12,9 @@ main() @*/ /*@ ensures return == 0i32; @*/ { - /*@ extract Owned, 0u64; @*/ - /*@ extract Owned, 1u64; @*/ - /*@ extract Owned, 2u64; @*/ + /*@ focus RW, 0u64; @*/ + /*@ focus RW, 1u64; @*/ + /*@ focus RW, 2u64; @*/ if (a[0] != 0) return 1; if (a[1] != 1) diff --git a/src/example-archive/dafny-tutorial/working/binary_search.c b/src/example-archive/dafny-tutorial/working/binary_search.c index e83786a4..62c3cb74 100644 --- a/src/example-archive/dafny-tutorial/working/binary_search.c +++ b/src/example-archive/dafny-tutorial/working/binary_search.c @@ -8,10 +8,10 @@ int binary_search(int *a, int length, int value) 0i32 <= length; (2i64 * (i64) length) <= MAXi32; take IndexPre = each (i32 j; 0i32 <= j && j < length) - {Owned(a + j)}; @*/ + {RW(a + j)}; @*/ /*@ ensures take IndexPost = each (i32 j; 0i32 <= j && j < length) - {Owned(a + j)}; + {RW(a + j)}; IndexPost == IndexPre; (return < 0i32) || (IndexPost[return] == value); @*/ { @@ -26,11 +26,11 @@ int binary_search(int *a, int length, int value) high <= length; ((i64) low + (i64) high) <= MAXi32; take IndexInv = each (i32 j; 0i32 <= j && j < length) - {Owned(a + j)}; + {RW(a + j)}; IndexInv == IndexPre; @*/ { int mid = (low + high) / 2; - /*@ extract Owned, mid; @*/ + /*@ focus RW, mid; @*/ /*@ instantiate good, mid; @*/ if (a[mid] < value) { diff --git a/src/example-archive/dafny-tutorial/working/linear_search.c b/src/example-archive/dafny-tutorial/working/linear_search.c index 17b42980..71409722 100644 --- a/src/example-archive/dafny-tutorial/working/linear_search.c +++ b/src/example-archive/dafny-tutorial/working/linear_search.c @@ -4,10 +4,10 @@ int linear_search(int *a, int length, int key) /*@ requires 0i32 < length; take IndexPre = each (i32 j; 0i32 <= j && j < length) - {Owned(a + j)}; @*/ + {RW(a + j)}; @*/ /*@ ensures take IndexPost = each (i32 j; 0i32 <= j && j < length) - {Owned(a + j)}; + {RW(a + j)}; (return < 0i32) || (IndexPost[return] == key); each (i32 j; 0i32 <= j && j < length) {return >= 0i32 || IndexPre[j] != key}; @@ -21,11 +21,11 @@ int linear_search(int *a, int length, int key) 0i32 <= idx; idx <= length; take IndexInv = each (i32 j; 0i32 <= j && j < length) - {Owned(a + j)}; + {RW(a + j)}; IndexInv == IndexPre; each (i32 j; 0i32 <= j && j < idx) {IndexPre[j] != key}; @*/ { - /*@ extract Owned, idx; @*/ + /*@ focus RW, idx; @*/ if (*(a + idx) == key) { return idx; diff --git a/src/example-archive/dafny-tutorial/working/multiple_returns.c b/src/example-archive/dafny-tutorial/working/multiple_returns.c index 8b2e20fd..6e419f0d 100644 --- a/src/example-archive/dafny-tutorial/working/multiple_returns.c +++ b/src/example-archive/dafny-tutorial/working/multiple_returns.c @@ -13,13 +13,13 @@ void multiple_returns(int x, int y, struct int_pair *ret) let MAXi32 = (i64) 2147483647i64; let MINi32 = (i64) -2147483647i64; - take PairPre = Owned(ret); + take PairPre = RW(ret); MINi32 <= (i64) x + (i64) y; (i64) x + (i64) y <= MAXi32; MINi32 <= (i64) x - (i64) y; (i64) x - (i64) y <= MAXi32; @*/ /*@ ensures - take PairPost = Owned(ret); + take PairPost = RW(ret); PairPost.fst == x + y; PairPost.snd == x - y; @*/ { diff --git a/src/example-archive/java_program_verification_challenges/broken/error-cerberus/00008_overload_dyn_method.c b/src/example-archive/java_program_verification_challenges/broken/error-cerberus/00008_overload_dyn_method.c index 1080d940..233f3b2b 100644 --- a/src/example-archive/java_program_verification_challenges/broken/error-cerberus/00008_overload_dyn_method.c +++ b/src/example-archive/java_program_verification_challenges/broken/error-cerberus/00008_overload_dyn_method.c @@ -36,15 +36,15 @@ processing a method invocation at compile-time ([13, Section //#include /*@ -predicate { u32 pv, u32 qv } BothOwned (pointer p, pointer q) +predicate { u32 pv, u32 qv } BothRW (pointer p, pointer q) { if (p == q) { - take pv = Owned(p); + take pv = RW(p); return {pv: pv, qv: pv}; } else { - take pv = Owned(p); - take qv = Owned(q); + take pv = RW(p); + take qv = RW(q); return {pv: pv, qv: qv}; } } @@ -71,8 +71,8 @@ int ColorPoint_equal(ColorPoint *self, ColorPoint *other) { // Wrapper functions for handling inheritance int Point_equal_wrapper(Point *self, Point *other) - /*@ requires take vs0 = BothOwned(self,other); - ensures take vs1 = BothOwned(self,other); + /*@ requires take vs0 = BothRW(self,other); + ensures take vs1 = BothRW(self,other); @*/ { // Direct call to the function based on actual type diff --git a/src/example-archive/java_program_verification_challenges/broken/error-proof/00002_side_effects.c b/src/example-archive/java_program_verification_challenges/broken/error-proof/00002_side_effects.c index 170f8cee..f1a7731a 100644 --- a/src/example-archive/java_program_verification_challenges/broken/error-proof/00002_side_effects.c +++ b/src/example-archive/java_program_verification_challenges/broken/error-proof/00002_side_effects.c @@ -60,10 +60,10 @@ void m() { } int main() - /*@ requires take vr0 = Block(result1); - take vr0 = Block(result2) - ensures take vp1 = Block(result1); - take vb1 = Block(result2) + /*@ requires take vr0 = W(result1); + take vr0 = W(result2) + ensures take vp1 = W(result1); + take vb1 = W(result2) @*/ { m(); // Execute the function m diff --git a/src/example-archive/java_program_verification_challenges/broken/error-proof/00003_break.c b/src/example-archive/java_program_verification_challenges/broken/error-proof/00003_break.c index 1127d696..53437b7f 100644 --- a/src/example-archive/java_program_verification_challenges/broken/error-proof/00003_break.c +++ b/src/example-archive/java_program_verification_challenges/broken/error-proof/00003_break.c @@ -53,8 +53,8 @@ void negateFirst() { } int main() - /*@ requires take vl0 = Owned(&ia_length) - ensures take vp1 = Owned(&ia_length) + /*@ requires take vl0 = RW(&ia_length) + ensures take vp1 = RW(&ia_length) @*/ { // Example usage diff --git a/src/example-archive/java_program_verification_challenges/broken/error-proof/00006_callbacks.c b/src/example-archive/java_program_verification_challenges/broken/error-proof/00006_callbacks.c index 982c3cc5..b9ccdb78 100644 --- a/src/example-archive/java_program_verification_challenges/broken/error-proof/00006_callbacks.c +++ b/src/example-archive/java_program_verification_challenges/broken/error-proof/00006_callbacks.c @@ -72,11 +72,11 @@ struct A { * @ ensures k == \old(k) - 1 && m == \old(m) + 1; */ void decrement_k(A *a) - /*@ requires take va0 = Owned(a); + /*@ requires take va0 = RW(a); va0.m < 2147483647i32; -2147483648i32 < va0.k; va0.k + va0.m == 0i32 - ensures take va1 = Owned(a); + ensures take va1 = RW(a); va1.k == va0.k-1i32; va1.m == va0.m+1i32; va1.k + va1.m == 0i32 @@ -97,12 +97,12 @@ void decrement_k(A *a) * @ ensures true; */ void increment_k(A *a) - /*@ requires take va0 = Owned(a); + /*@ requires take va0 = RW(a); va0.k < 2147483647i32; va0.m < 2147483647i32; -2147483648i32 < va0.m; va0.k + va0.m == 0i32 - ensures take va1 = Owned(a); + ensures take va1 = RW(a); va1.k == va0.k; va1.m == va0.m; va1.k + va1.m == 0i32 diff --git a/src/example-archive/java_program_verification_challenges/broken/error-proof/00007_static_init.c b/src/example-archive/java_program_verification_challenges/broken/error-proof/00007_static_init.c index e72ef63c..3e41fedc 100644 --- a/src/example-archive/java_program_verification_challenges/broken/error-proof/00007_static_init.c +++ b/src/example-archive/java_program_verification_challenges/broken/error-proof/00007_static_init.c @@ -78,10 +78,10 @@ void initialize() { * @ ensures result1 && !result2 && result3 && result4 */ void m() - /*@ requires take vbl0 = Owned(bl); - take vdl0 = Owned(dl); - take vb20 = Owned(b2); - take vd20 = Owned(d2) + /*@ requires take vbl0 = RW(bl); + take vdl0 = RW(dl); + take vb20 = RW(b2); + take vd20 = RW(d2) ensures true @*/ { diff --git a/src/example-archive/java_program_verification_challenges/working/00004_exceptions.c b/src/example-archive/java_program_verification_challenges/working/00004_exceptions.c index 94a50bf5..e6e1f5e5 100644 --- a/src/example-archive/java_program_verification_challenges/working/00004_exceptions.c +++ b/src/example-archive/java_program_verification_challenges/working/00004_exceptions.c @@ -38,10 +38,10 @@ int m; // Global variable m * && m == \old(m) + 10; */ int returnfinally(int d) - /*@ requires take vp0 = Owned(&m); + /*@ requires take vp0 = RW(&m); let m10 = (i64)vp0 + 10i64; m10 <= 2147483647i64; - ensures take vp1 = Owned(&m); + ensures take vp1 = RW(&m); @*/ { int result; @@ -58,8 +58,8 @@ int returnfinally(int d) } int main() - /*@ requires take vp0 = Owned(&m); - ensures take vp1 = Block(&m); + /*@ requires take vp0 = RW(&m); + ensures take vp1 = W(&m); return == 0i32; @*/ { diff --git a/src/example-archive/open-sut/working/mps_1.c b/src/example-archive/open-sut/working/mps_1.c index 9f64148c..a26919c0 100644 --- a/src/example-archive/open-sut/working/mps_1.c +++ b/src/example-archive/open-sut/working/mps_1.c @@ -35,19 +35,19 @@ typedef uint8_t w8; w1 Coincidence_2_4(w8 trips[4]) /*@ requires - take ta = Owned(array_shift(trips, 0i32)); - take tb = Owned(array_shift(trips, 1i32)); - take tc = Owned(array_shift(trips, 2i32)); - take td = Owned(array_shift(trips, 3i32)); + take ta = RW(array_shift(trips, 0i32)); + take tb = RW(array_shift(trips, 1i32)); + take tc = RW(array_shift(trips, 2i32)); + take td = RW(array_shift(trips, 3i32)); let a = ta != 0u8; let b = tb != 0u8; let c = tc != 0u8; let d = td != 0u8; ensures - take ta_out = Owned(array_shift(trips, 0i32)); - take tb_out = Owned(array_shift(trips, 1i32)); - take tc_out = Owned(array_shift(trips, 2i32)); - take td_out = Owned(array_shift(trips, 3i32)); + take ta_out = RW(array_shift(trips, 0i32)); + take tb_out = RW(array_shift(trips, 1i32)); + take tc_out = RW(array_shift(trips, 2i32)); + take td_out = RW(array_shift(trips, 3i32)); return == Bool_to_u8(P_Coincidence_2_4(a, b, c, d)); @*/ { diff --git a/src/example-archive/should-fail/broken/error-proof/ownership_neg_1.c b/src/example-archive/should-fail/broken/error-proof/ownership_neg_1.c index 7b788719..2903b829 100644 --- a/src/example-archive/should-fail/broken/error-proof/ownership_neg_1.c +++ b/src/example-archive/should-fail/broken/error-proof/ownership_neg_1.c @@ -1,9 +1,9 @@ // Negative test case: proof should fail -// Precondition includes access to the resource Owned(p), which disappears in +// Precondition includes access to the resource RW(p), which disappears in // the postcondition void ownership_neg_1(int *p) -/*@ requires take P = Owned(p); @*/ +/*@ requires take P = RW(p); @*/ /*@ ensures true; @*/ { ; diff --git a/src/example-archive/should-fail/broken/error-proof/ownership_neg_2.c b/src/example-archive/should-fail/broken/error-proof/ownership_neg_2.c index 42f8044b..b375b5d7 100644 --- a/src/example-archive/should-fail/broken/error-proof/ownership_neg_2.c +++ b/src/example-archive/should-fail/broken/error-proof/ownership_neg_2.c @@ -1,10 +1,10 @@ // Negative test case: proof should fail // Precondition takes ownership of no resources, but then the postcondition -// claims ownership of Owned(p) +// claims ownership of RW(p) void ownership_neg_2(int *p) /*@ requires true; @*/ -/*@ ensures take P_ = Owned(p); @*/ +/*@ ensures take P_ = RW(p); @*/ { ; } \ No newline at end of file diff --git a/src/example-archive/should-fail/broken/error-proof/ownership_neg_3.c b/src/example-archive/should-fail/broken/error-proof/ownership_neg_3.c index b0bff2d3..4a0fba43 100644 --- a/src/example-archive/should-fail/broken/error-proof/ownership_neg_3.c +++ b/src/example-archive/should-fail/broken/error-proof/ownership_neg_3.c @@ -1,12 +1,12 @@ // Negative test case: proof should fail -// Precondition includes access to the resource Owned(p), which is duplicated in +// Precondition includes access to the resource RW(p), which is duplicated in // the postcondition void ownership_neg_3(int *p) -/*@ requires take P = Owned(p); @*/ +/*@ requires take P = RW(p); @*/ /*@ ensures - take P_ = Owned(p); - take Q_ = Owned(p); @*/ + take P_ = RW(p); + take Q_ = RW(p); @*/ { ; } \ No newline at end of file diff --git a/src/example-archive/should-fail/working/c_sequencing_race.c b/src/example-archive/should-fail/working/c_sequencing_race.c index c91abf15..0babc927 100644 --- a/src/example-archive/should-fail/working/c_sequencing_race.c +++ b/src/example-archive/should-fail/working/c_sequencing_race.c @@ -2,9 +2,9 @@ int f (int *x) -/*@ requires take xv = Owned(x); @*/ +/*@ requires take xv = RW(x); @*/ /*@ requires 0i32 <= xv && xv < 500i32; @*/ -/*@ ensures take xv2 = Owned(x); @*/ +/*@ ensures take xv2 = RW(x); @*/ { return ((*x) + (*x)); } diff --git a/src/example-archive/simple-examples/broken/error-cerberus/pred_1.c b/src/example-archive/simple-examples/broken/error-cerberus/pred_1.c index 80c71112..137a95ba 100644 --- a/src/example-archive/simple-examples/broken/error-cerberus/pred_1.c +++ b/src/example-archive/simple-examples/broken/error-cerberus/pred_1.c @@ -3,7 +3,7 @@ /*@ predicate (i32) TestMemoryEqZero_1(pointer p) { - take PVal = Owned(p); + take PVal = RW(p); if (PVal == 0i32) { return 1i32; } else { @@ -14,7 +14,7 @@ predicate (i32) TestMemoryEqZero_1(pointer p) { void pred_1(int *p) /*@ requires - take PreP = Owned(p); + take PreP = RW(p); PreP == 0i32; @*/ /*@ ensures take TestP = TestMemoryEqZero_1(p); diff --git a/src/example-archive/simple-examples/broken/error-proof/ownership_1.c b/src/example-archive/simple-examples/broken/error-proof/ownership_1.c index 62b7f3e9..d8bdaba1 100644 --- a/src/example-archive/simple-examples/broken/error-proof/ownership_1.c +++ b/src/example-archive/simple-examples/broken/error-proof/ownership_1.c @@ -1,12 +1,12 @@ -// This example should be provable because Owned locations should be +// This example should be provable because RW locations should be // disjoint. But CN currently doesn't enforce this property. // See: https://github.com/rems-project/cerberus/issues/295 void ownership_1(int *a, int *b) /*@ requires - take P1 = Owned(a); - take P2 = Owned(b); + take P1 = RW(a); + take P2 = RW(b); ensures a != b; @*/ diff --git a/src/example-archive/simple-examples/broken/error-timeout/overflow_timeout_3var.c b/src/example-archive/simple-examples/broken/error-timeout/overflow_timeout_3var.c index 481a5a85..1b8ef064 100644 --- a/src/example-archive/simple-examples/broken/error-timeout/overflow_timeout_3var.c +++ b/src/example-archive/simple-examples/broken/error-timeout/overflow_timeout_3var.c @@ -18,10 +18,10 @@ typedef struct { } example_t; int overflow_timeout_3var(example_t* p1,example_t* p2) /*@ - requires take x = Owned(p1); - take y = Owned(p2); - ensures take x2 = Owned(p1); - take y2 = Owned(p2); + requires take x = RW(p1); + take y = RW(p2); + ensures take x2 = RW(p1); + take y2 = RW(p2); @*/ { int distance = 0; diff --git a/src/example-archive/simple-examples/broken/error-timeout/overflow_timeout_4var.c b/src/example-archive/simple-examples/broken/error-timeout/overflow_timeout_4var.c index 44ee9a84..a7b787ab 100644 --- a/src/example-archive/simple-examples/broken/error-timeout/overflow_timeout_4var.c +++ b/src/example-archive/simple-examples/broken/error-timeout/overflow_timeout_4var.c @@ -18,10 +18,10 @@ typedef struct { } example_t; int overflow_timeout_4var(example_t* p1,example_t* p2) /*@ - requires take x = Owned(p1); - take y = Owned(p2); - ensures take x2 = Owned(p1); - take y2 = Owned(p2); + requires take x = RW(p1); + take y = RW(p2); + ensures take x2 = RW(p1); + take y2 = RW(p2); @*/ { int distance = 0; diff --git a/src/example-archive/simple-examples/working/array_1.c b/src/example-archive/simple-examples/working/array_1.c index c09c35b1..2435926c 100644 --- a/src/example-archive/simple-examples/working/array_1.c +++ b/src/example-archive/simple-examples/working/array_1.c @@ -2,13 +2,13 @@ void array_1(int *arr, int size, int off) /*@ requires - take arrayStart = each (i32 j; 0i32 <= j && j < size) {Owned(arr + j)}; + take arrayStart = each (i32 j; 0i32 <= j && j < size) {RW(arr + j)}; 0i32 <= off; off < size; @*/ -/*@ ensures take arrayEnd = each (i32 j; 0i32 <= j && j < size) {Owned(arr + j)}; @*/ +/*@ ensures take arrayEnd = each (i32 j; 0i32 <= j && j < size) {RW(arr + j)}; @*/ { int i = off; - /*@ extract Owned, i; @*/ // <-- required to read / write + /*@ focus RW, i; @*/ // <-- required to read / write arr[off] = 7; i++; return; diff --git a/src/example-archive/simple-examples/working/array_2.c b/src/example-archive/simple-examples/working/array_2.c index 6aa849ed..accb09e0 100644 --- a/src/example-archive/simple-examples/working/array_2.c +++ b/src/example-archive/simple-examples/working/array_2.c @@ -2,16 +2,16 @@ int array_2(int *arr, int size, int off) /*@ requires - take arrayStart = each (i32 j; 0i32 <= j && j < size) {Owned(arr + j)}; + take arrayStart = each (i32 j; 0i32 <= j && j < size) {RW(arr + j)}; 0i32 <= off; off < size; arrayStart[off] != 0i32; @*/ /*@ ensures - take arrayEnd = each (i32 j; 0i32 <= j && j < size) {Owned(arr + j)}; + take arrayEnd = each (i32 j; 0i32 <= j && j < size) {RW(arr + j)}; arrayEnd[off] == 7i32; return == arrayStart[off]; @*/ { - /*@ extract Owned, off; @*/ + /*@ focus RW, off; @*/ int tmp = arr[off]; arr[off] = 7; return tmp; diff --git a/src/example-archive/simple-examples/working/array_3.c b/src/example-archive/simple-examples/working/array_3.c index 18ed2241..a45e9ba1 100644 --- a/src/example-archive/simple-examples/working/array_3.c +++ b/src/example-archive/simple-examples/working/array_3.c @@ -5,9 +5,9 @@ void array_3(int *arr, int n) /*@ requires 0i32 < n; - take arrayStart = each (i32 j; 0i32 <= j && j < n) {Owned(arr + j)}; @*/ + take arrayStart = each (i32 j; 0i32 <= j && j < n) {RW(arr + j)}; @*/ /*@ ensures - take arrayEnd = each (i32 j; 0i32 <= j && j < n) {Owned(arr + j)}; + take arrayEnd = each (i32 j; 0i32 <= j && j < n) {RW(arr + j)}; each (i32 j; 0i32 <= j && j < n) {arrayEnd[j] == 7i32}; @*/ { int i = 0; @@ -16,10 +16,10 @@ void array_3(int *arr, int n) {arr}unchanged; 0i32 <= i; i <= n; - take arrayInv = each (i32 j; 0i32 <= j && j < n) {Owned(arr + j)}; + take arrayInv = each (i32 j; 0i32 <= j && j < n) {RW(arr + j)}; each (i32 j; 0i32 <= j && j < i) {arrayInv[j] == 7i32}; @*/ { - /*@ extract Owned, i; @*/ + /*@ focus RW, i; @*/ *(arr + i) = 7; i++; }; diff --git a/src/example-archive/simple-examples/working/array_read.c b/src/example-archive/simple-examples/working/array_read.c index 5ae6fbe4..e53e886c 100644 --- a/src/example-archive/simple-examples/working/array_read.c +++ b/src/example-archive/simple-examples/working/array_read.c @@ -3,7 +3,7 @@ int head(int *arr, unsigned long len) /*@ requires take arr_in = each(u64 i; i < len) { - Owned(array_shift(arr, i)) + RW(array_shift(arr, i)) }; each(u64 i; i < len) { arr_in[i] == 0i32 @@ -12,7 +12,7 @@ requires ensures take arr_out = each(u64 i; i < len) { - Owned(array_shift(arr, i)) + RW(array_shift(arr, i)) }; each(u64 i; i < len) { arr_out[i] == 0i32 @@ -22,10 +22,10 @@ ensures { unsigned long idx = 0; - // First, we apply `extract` to direct CN to the relevant element of the + // First, we apply `focus` to direct CN to the relevant element of the // iterated resource `arr_in`, which it needs in order to verify the // following read: - /*@ extract Owned, idx; @*/ + /*@ focus RW, idx; @*/ int hd = arr[idx]; diff --git a/src/example-archive/simple-examples/working/assert_2.c b/src/example-archive/simple-examples/working/assert_2.c index 9fb7f147..9c18097b 100644 --- a/src/example-archive/simple-examples/working/assert_2.c +++ b/src/example-archive/simple-examples/working/assert_2.c @@ -2,12 +2,12 @@ void assert_2(int *x, int *y) /*@ requires - take Xpre = Owned(x); - take Ypre = Owned(y); + take Xpre = RW(x); + take Ypre = RW(y); *x == 7i32; *y == 7i32; @*/ /*@ ensures - take Xpost = Owned(x); - take Ypost = Owned(y); + take Xpost = RW(x); + take Ypost = RW(y); *x == 0i32; *y == 0i32; @*/ { *x = 0; diff --git a/src/example-archive/simple-examples/working/assert_3.c b/src/example-archive/simple-examples/working/assert_3.c index ab251f66..7e5c7b89 100644 --- a/src/example-archive/simple-examples/working/assert_3.c +++ b/src/example-archive/simple-examples/working/assert_3.c @@ -4,20 +4,20 @@ // Define a lemma that asserts ownership of a particular memory cell /*@ lemma assert_own (pointer p) - requires take x0 = Owned(p); + requires take x0 = RW(p); ensures - take x1 = Owned(p); + take x1 = RW(p); x1 == x0; // <-- Note, otherwise the lemma havocs the memory contents @*/ void assert_3(int *x, int *y) /*@ requires - take Xpre = Owned(x); - take Ypre = Owned(y); + take Xpre = RW(x); + take Ypre = RW(y); *x == 7i32; *y == 7i32; @*/ /*@ ensures - take Xpost = Owned(x); - take Ypost = Owned(y); + take Xpost = RW(x); + take Ypost = RW(y); *x == 0i32; *y == 0i32; @*/ { *x = 0; diff --git a/src/example-archive/simple-examples/working/cast_4.c b/src/example-archive/simple-examples/working/cast_4.c index 5510b6c5..e94c051f 100644 --- a/src/example-archive/simple-examples/working/cast_4.c +++ b/src/example-archive/simple-examples/working/cast_4.c @@ -5,8 +5,8 @@ #define OFFSET 374328 int cast_4(int *ptr_original) -/*@ requires take Pre = Block(ptr_original); @*/ -/*@ ensures take Post = Owned(ptr_original); +/*@ requires take Pre = W(ptr_original); @*/ +/*@ ensures take Post = RW(ptr_original); return == 7i32; @*/ { *ptr_original = 7; diff --git a/src/example-archive/simple-examples/working/cn_function_1.c b/src/example-archive/simple-examples/working/cn_function_1.c index 2a8c5ad2..809f5da2 100644 --- a/src/example-archive/simple-examples/working/cn_function_1.c +++ b/src/example-archive/simple-examples/working/cn_function_1.c @@ -1,5 +1,5 @@ // Example of the `cn_function` feature for extracting spec-level functions. -// This example extracts a ternary bitwise-OR +// This example focuss a ternary bitwise-OR // Give the CN-level signature for bitwise-OR /*@ diff --git a/src/example-archive/simple-examples/working/effect_1.c b/src/example-archive/simple-examples/working/effect_1.c index 2b3833f0..7528da5c 100644 --- a/src/example-archive/simple-examples/working/effect_1.c +++ b/src/example-archive/simple-examples/working/effect_1.c @@ -7,9 +7,9 @@ int g; void write_g_to_1() /*@ requires - take Pre = Block(&g); @*/ + take Pre = W(&g); @*/ /*@ ensures - take Post = Owned(&g); + take Post = RW(&g); Post == 1i32; @*/ { g = 1; @@ -19,9 +19,9 @@ write_g_to_1() int effect_1() /*@ requires - take Pre = Block(&g); @*/ + take Pre = W(&g); @*/ /*@ ensures - take Post = Owned(&g); + take Post = RW(&g); return == 1i32; @*/ { int x; diff --git a/src/example-archive/simple-examples/working/free_1.c b/src/example-archive/simple-examples/working/free_1.c index 1c07f886..9879d011 100644 --- a/src/example-archive/simple-examples/working/free_1.c +++ b/src/example-archive/simple-examples/working/free_1.c @@ -5,14 +5,14 @@ void my_free_int(int *target) /*@ trusted; @*/ -/*@ requires take ToFree = Owned(target); @*/ +/*@ requires take ToFree = RW(target); @*/ {} void free_1(int *x, int *y) /*@ requires - take Xpre = Owned(x); - take Ypre = Owned(y); @*/ -/*@ ensures take Ypost = Owned(y); @*/ + take Xpre = RW(x); + take Ypre = RW(y); @*/ +/*@ ensures take Ypost = RW(y); @*/ { *x = 7; my_free_int(x); diff --git a/src/example-archive/simple-examples/working/list_2.c b/src/example-archive/simple-examples/working/list_2.c index bb51d081..07b1157d 100644 --- a/src/example-archive/simple-examples/working/list_2.c +++ b/src/example-archive/simple-examples/working/list_2.c @@ -12,7 +12,7 @@ /*@ lemma IntListSeqSnoc(pointer p, pointer tail) requires take l1 = IntListSeg(p, tail); - take v = Owned(tail); + take v = RW(tail); ensures take l2 = IntListSeg(p, v.next); l2 == append(l1, Seq_Cons { val: v.val, next: Seq_Nil {} }); @*/ diff --git a/src/example-archive/simple-examples/working/list_3.c b/src/example-archive/simple-examples/working/list_3.c index 09e948fc..38a90f80 100644 --- a/src/example-archive/simple-examples/working/list_3.c +++ b/src/example-archive/simple-examples/working/list_3.c @@ -11,7 +11,7 @@ predicate (datatype seq) IntListSegVal(pointer p, pointer tail, i32 tval) { if (addr_eq(p,tail)) { return Seq_Nil{}; } else { - take H = Owned(p); + take H = RW(p); assert (is_null(H.next) || H.next != NULL); assert (H.val == tval); take tl = IntListSeg(H.next, tail); @@ -22,7 +22,7 @@ predicate (datatype seq) IntListSegVal(pointer p, pointer tail, i32 tval) { /*@ lemma IntListSeqSnocVal(pointer p, pointer tail, i32 tval) requires take l1 = IntListSegVal(p, tail, tval); - take v = Owned(tail); + take v = RW(tail); v.val == tval; ensures take l2 = IntListSegVal(p, v.next, tval); l2 == append(l1, Seq_Cons { val: v.val, next: Seq_Nil {} }); diff --git a/src/example-archive/simple-examples/working/malloc_1.c b/src/example-archive/simple-examples/working/malloc_1.c index 9259c221..86d80e79 100644 --- a/src/example-archive/simple-examples/working/malloc_1.c +++ b/src/example-archive/simple-examples/working/malloc_1.c @@ -5,12 +5,12 @@ int *my_malloc__int() /*@ trusted; @*/ -/*@ ensures take New = Block(return); @*/ +/*@ ensures take New = W(return); @*/ {} int *malloc__1() /*@ ensures - take New = Owned(return); + take New = RW(return); New == 7i32; *return == 7i32; @*/ // <-- Alternative syntax { diff --git a/src/example-archive/simple-examples/working/pred_2.c b/src/example-archive/simple-examples/working/pred_2.c index cee0756f..27eaf079 100644 --- a/src/example-archive/simple-examples/working/pred_2.c +++ b/src/example-archive/simple-examples/working/pred_2.c @@ -4,7 +4,7 @@ // Variant 1 - this works: /*@ predicate (i32) TestMemoryEqZero_2_var1(pointer p) { - take PVal = Owned(p); + take PVal = RW(p); let rval = test_if_zero(PVal); return rval; } @@ -20,7 +20,7 @@ function (i32) test_if_zero(i32 x) { void pred_2_var1(int *p) /*@ requires - take PreP = Owned(p); + take PreP = RW(p); PreP == 0i32; @*/ /*@ ensures take TestP = TestMemoryEqZero_2_var1(p); @@ -32,7 +32,7 @@ void pred_2_var1(int *p) // Variant 2 - this works: /*@ predicate (i32) TestMemoryEqZero_2_var2(pointer p) { - take PVal = Owned(p); + take PVal = RW(p); take rval = TestMemoryEqZero_2_Helper(p, PVal); return rval; } @@ -48,7 +48,7 @@ predicate (i32) TestMemoryEqZero_2_Helper(pointer p, i32 x) { void pred_2_var2(int *p) /*@ requires - take PreP = Owned(p); + take PreP = RW(p); PreP == 0i32; @*/ /*@ ensures take TestP = TestMemoryEqZero_2_var2(p); @@ -60,7 +60,7 @@ void pred_2_var2(int *p) // Variant 3 - this works: /*@ predicate (i32) TestMemoryEqZero_2_var3(pointer p) { - take PVal = Owned(p); + take PVal = RW(p); let rval = (PVal == 0i32 ? 1i32 : 0i32); return rval; } @@ -68,7 +68,7 @@ predicate (i32) TestMemoryEqZero_2_var3(pointer p) { void pred_2_var3(int *p) /*@ requires - take PreP = Owned(p); + take PreP = RW(p); PreP == 0i32; @*/ /*@ ensures take TestP = TestMemoryEqZero_2_var3(p); diff --git a/src/example-archive/simple-examples/working/struct_1.c b/src/example-archive/simple-examples/working/struct_1.c index 831ed01c..2465dd24 100644 --- a/src/example-archive/simple-examples/working/struct_1.c +++ b/src/example-archive/simple-examples/working/struct_1.c @@ -7,9 +7,9 @@ struct s }; void struct_1(struct s *p) -/*@ requires take StructPre = Owned(p); @*/ +/*@ requires take StructPre = RW(p); @*/ /*@ ensures - take StructPost = Owned(p); + take StructPost = RW(p); StructPre.x == StructPost.x; StructPost.y == 0i32; @*/ { diff --git a/src/example-archive/simple-examples/working/swap_1.c b/src/example-archive/simple-examples/working/swap_1.c index 6bdb45cd..483547f2 100644 --- a/src/example-archive/simple-examples/working/swap_1.c +++ b/src/example-archive/simple-examples/working/swap_1.c @@ -2,11 +2,11 @@ void swap_1(int *a, int *b) /*@ requires - take Pa = Owned(a); - take Pb = Owned(b); @*/ + take Pa = RW(a); + take Pb = RW(b); @*/ /*@ ensures - take Qa = Owned(a); - take Qb = Owned(b); + take Qa = RW(a); + take Qb = RW(b); Qb == Pa; Qa == Pb; @*/ { diff --git a/src/example-archive/simple-examples/working/write_1.c b/src/example-archive/simple-examples/working/write_1.c index 2ce303c9..bde260db 100644 --- a/src/example-archive/simple-examples/working/write_1.c +++ b/src/example-archive/simple-examples/working/write_1.c @@ -1,9 +1,9 @@ // Write into a memory cell void write_1(int *cell) -/*@ requires take CellPre = Owned(cell); @*/ +/*@ requires take CellPre = RW(cell); @*/ /*@ ensures - take CellPost = Owned(cell); + take CellPost = RW(cell); CellPost == 7i32; @*/ { *cell = 7; diff --git a/src/example-archive/simple-examples/working/write_2.c b/src/example-archive/simple-examples/working/write_2.c index d5ce2e9c..abc798f5 100644 --- a/src/example-archive/simple-examples/working/write_2.c +++ b/src/example-archive/simple-examples/working/write_2.c @@ -1,10 +1,10 @@ // Write into two memory cells void write_2(int *cell1, int *cell2) -/*@ requires take Cell1Pre = Owned(cell1); - take Cell2Pre = Owned(cell2); @*/ -/*@ ensures take Cell1Post = Owned(cell1); - take Cell2Post = Owned(cell2); +/*@ requires take Cell1Pre = RW(cell1); + take Cell2Pre = RW(cell2); @*/ +/*@ ensures take Cell1Post = RW(cell1); + take Cell2Post = RW(cell2); Cell1Post == 7i32; Cell2Post == 8i32; @*/ { *cell1 = 7; diff --git a/src/example-archive/simple-examples/working/write_3.c b/src/example-archive/simple-examples/working/write_3.c index fcd1dad9..342c7d39 100644 --- a/src/example-archive/simple-examples/working/write_3.c +++ b/src/example-archive/simple-examples/working/write_3.c @@ -2,10 +2,10 @@ void write_3(int *cell1, int *cell2) /*@ requires - take Cell1Pre = Owned(cell1); + take Cell1Pre = RW(cell1); cell1 == cell2; @*/ /*@ ensures - take Cell2Post = Owned(cell2); + take Cell2Post = RW(cell2); Cell2Post == 8i32; @*/ { *cell1 = 7; diff --git a/src/example-archive/simple-examples/working/write_4.c b/src/example-archive/simple-examples/working/write_4.c index 4f6eee24..9971bda0 100644 --- a/src/example-archive/simple-examples/working/write_4.c +++ b/src/example-archive/simple-examples/working/write_4.c @@ -4,11 +4,11 @@ static int *cell1, *cell2; void write_4() /*@ accesses cell1, cell2; requires - take Cell1Pre = Owned(cell1); - take Cell2Pre = Owned(cell2); + take Cell1Pre = RW(cell1); + take Cell2Pre = RW(cell2); ensures - take Cell1Post = Owned(cell1); - take Cell2Post = Owned(cell2); + take Cell1Post = RW(cell1); + take Cell2Post = RW(cell2); Cell1Post == 7i32; Cell2Post == 8i32; @*/ { diff --git a/src/example-archive/simple-examples/working/write_5.c b/src/example-archive/simple-examples/working/write_5.c index 2fe0c727..07d4e634 100644 --- a/src/example-archive/simple-examples/working/write_5.c +++ b/src/example-archive/simple-examples/working/write_5.c @@ -2,11 +2,11 @@ void write_5(int *pair) /*@ requires - take Cell1Pre = Owned(pair); - take Cell2Pre = Owned(pair + 1i32); @*/ + take Cell1Pre = RW(pair); + take Cell2Pre = RW(pair + 1i32); @*/ /*@ ensures - take Cell1Post = Owned(pair); - take Cell2Post = Owned(pair + 1i32); + take Cell1Post = RW(pair); + take Cell2Post = RW(pair + 1i32); Cell1Post == 7i32; Cell2Post == 8i32; @*/ { @@ -18,15 +18,15 @@ void write_5(int *pair) void write_5_alt(int *pair) /*@ requires - take PairPre = each (i32 j; j == 0i32 || j == 1i32) {Owned(pair + j)}; @*/ + take PairPre = each (i32 j; j == 0i32 || j == 1i32) {RW(pair + j)}; @*/ /*@ ensures - take PairPost = each (i32 j; j == 0i32 || j == 1i32) {Owned(pair + j)}; + take PairPost = each (i32 j; j == 0i32 || j == 1i32) {RW(pair + j)}; PairPost[0i32] == 7i32; PairPost[1i32] == 8i32; @*/ { - /*@ extract Owned, 0i32; @*/ + /*@ focus RW, 0i32; @*/ pair[0] = 7; - /*@ extract Owned, 1i32; @*/ + /*@ focus RW, 1i32; @*/ pair[1] = 8; } diff --git a/src/examples/abs_mem.c b/src/examples/abs_mem.c index 978fefa0..3a188c3f 100644 --- a/src/examples/abs_mem.c +++ b/src/examples/abs_mem.c @@ -1,8 +1,8 @@ int abs_mem (int *p) /* --BEGIN-- */ -/*@ requires take x = Owned(p); +/*@ requires take x = RW(p); MINi32() < x; - ensures take x_post = Owned(p); + ensures take x_post = RW(p); x == x_post; return == ((x >= 0i32) ? x : (0i32-x)); @*/ diff --git a/src/examples/abs_mem_struct.c b/src/examples/abs_mem_struct.c index 92a3005f..0bf68750 100644 --- a/src/examples/abs_mem_struct.c +++ b/src/examples/abs_mem_struct.c @@ -1,8 +1,8 @@ int abs_mem (int *p) /* --BEGIN-- */ -/*@ requires take x = Owned(p); +/*@ requires take x = RW(p); MINi32() < x; - ensures take x2 = Owned(p); + ensures take x2 = RW(p); x == x2; return == ((x >= 0i32) ? x : (0i32-x)); @*/ @@ -26,9 +26,9 @@ struct tuple { int abs_y (struct tuple *p) -/*@ requires take s = Owned(p); +/*@ requires take s = RW(p); MINi32() < s.y; - ensures take s2 = Owned(p); + ensures take s2 = RW(p); s == s2; return == ((s.y >= 0i32) ? s.y : (0i32-s.y)); @*/ diff --git a/src/examples/add_read.c b/src/examples/add_read.c index 2341bd04..bb93e867 100644 --- a/src/examples/add_read.c +++ b/src/examples/add_read.c @@ -1,8 +1,8 @@ unsigned int add (unsigned int *p, unsigned int *q) -/*@ requires take P = Owned(p); - take Q = Owned(q); - ensures take P_post = Owned(p); - take Q_post = Owned(q); +/*@ requires take P = RW(p); + take Q = RW(q); + ensures take P_post = RW(p); + take Q_post = RW(q); P == P_post && Q == Q_post; return == P + Q; @*/ diff --git a/src/examples/add_two_array.c b/src/examples/add_two_array.c index 70a8e5fc..8789bd22 100644 --- a/src/examples/add_two_array.c +++ b/src/examples/add_two_array.c @@ -1,23 +1,23 @@ unsigned int array_read_two (unsigned int *p, int n, int i, int j) /* --BEGIN-- */ /*@ requires take A = each(i32 k; 0i32 <= k && k < n) { - Owned(array_shift(p,k)) }; + RW(array_shift(p,k)) }; 0i32 <= i && i < n; 0i32 <= j && j < n; j != i; ensures take A_post = each(i32 k; 0i32 <= k && k < n) { - Owned(array_shift(p,k)) }; + RW(array_shift(p,k)) }; A == A_post; return == A[i] + A[j]; @*/ /* --END-- */ { /* --BEGIN-- */ - /*@ extract Owned, i; @*/ + /*@ focus RW, i; @*/ /* --END-- */ unsigned int tmp1 = p[i]; /* --BEGIN-- */ - /*@ extract Owned, j; @*/ + /*@ focus RW, j; @*/ /* --END-- */ unsigned int tmp2 = p[j]; return (tmp1 + tmp2); diff --git a/src/examples/array_load.broken.c b/src/examples/array_load.broken.c index 446072cf..618cc8ac 100644 --- a/src/examples/array_load.broken.c +++ b/src/examples/array_load.broken.c @@ -1,9 +1,9 @@ int read (int *p, int n, int i) /*@ requires take A = each(i32 j; 0i32 <= j && j < n) { - Owned(array_shift(p,j)) }; + RW(array_shift(p,j)) }; 0i32 <= i && i < n; ensures take A_post = each(i32 j; 0i32 <= j && j < n) { - Owned(array_shift(p,j)) }; + RW(array_shift(p,j)) }; @*/ { return p[i]; diff --git a/src/examples/array_load.c b/src/examples/array_load.c index 6cd87216..58e039a2 100644 --- a/src/examples/array_load.c +++ b/src/examples/array_load.c @@ -1,11 +1,11 @@ int read (int *p, int n, int i) /*@ requires take A = each(i32 j; 0i32 <= j && j < n) { - Owned(array_shift(p,j)) }; + RW(array_shift(p,j)) }; 0i32 <= i && i < n; ensures take A_post = each(i32 j; 0i32 <= j && j < n) { - Owned(array_shift(p,j)) }; + RW(array_shift(p,j)) }; @*/ { - /*@ extract Owned, i; @*/ + /*@ focus RW, i; @*/ return p[i]; } diff --git a/src/examples/array_load2.c b/src/examples/array_load2.c index 4f38a1f1..fdc98e88 100644 --- a/src/examples/array_load2.c +++ b/src/examples/array_load2.c @@ -1,11 +1,11 @@ int read (int *p, int n, int i) -/*@ requires take a1 = each(i32 j; 0i32 <= j && j < n) { Owned(array_shift(p,j)) }; +/*@ requires take a1 = each(i32 j; 0i32 <= j && j < n) { RW(array_shift(p,j)) }; 0i32 <= i && i < n; - ensures take a2 = each(i32 j; 0i32 <= j && j < n) { Owned(array_shift(p,j)) }; + ensures take a2 = each(i32 j; 0i32 <= j && j < n) { RW(array_shift(p,j)) }; a1 == a2; return == a1[i]; @*/ { - /*@ extract Owned, i; @*/ + /*@ focus RW, i; @*/ return p[i]; } diff --git a/src/examples/bcp_framerule.c b/src/examples/bcp_framerule.c index 1f5d3a10..d0a6caf3 100644 --- a/src/examples/bcp_framerule.c +++ b/src/examples/bcp_framerule.c @@ -1,6 +1,6 @@ void incr_first (unsigned int *p, unsigned int *q) -/*@ requires take pv = Owned(p); - ensures take pv_ = Owned(p); +/*@ requires take pv = RW(p); + ensures take pv_ = RW(p); pv_ == pv + 1u32; @*/ { @@ -10,10 +10,10 @@ void incr_first (unsigned int *p, unsigned int *q) } void incr_first_frame (unsigned int *p, unsigned int *q) -/*@ requires take pv = Owned(p); - take qv = Owned(q); - ensures take pv_ = Owned(p); - take qv_ = Owned(q); +/*@ requires take pv = RW(p); + take qv = RW(q); + ensures take pv_ = RW(p); + take qv_ = RW(q); pv_ == pv + 1u32; qv_ == qv; @*/ diff --git a/src/examples/dll/remove.c b/src/examples/dll/remove.c index 7c87360c..0d56a2b6 100644 --- a/src/examples/dll/remove.c +++ b/src/examples/dll/remove.c @@ -7,7 +7,7 @@ struct dllist_and_int *remove(struct dllist *n) /*@ requires !is_null(n); take Before = Dll_at(n); let Del = Node(Before); - ensures take Ret = Owned(return); + ensures take Ret = RW(return); take After = Dll_at(Ret.dllist); Ret.data == Del.data; (is_null(Del.prev) && is_null(Del.next)) diff --git a/src/examples/init_array.c b/src/examples/init_array.c index b288cb1c..f1609062 100644 --- a/src/examples/init_array.c +++ b/src/examples/init_array.c @@ -1,22 +1,22 @@ void init_array (char *p, unsigned int n) /*@ requires take A = each(u32 i; i < n) { - Owned( array_shift(p, i)) }; + RW( array_shift(p, i)) }; ensures take A_post = each(u32 i; i < n) { - Owned( array_shift(p, i)) }; + RW( array_shift(p, i)) }; @*/ { unsigned int j = 0; while (j < n) /* --BEGIN-- */ /*@ inv take Ai = each(u32 i; i < n) { - Owned( array_shift(p, i)) }; + RW( array_shift(p, i)) }; {p} unchanged; {n} unchanged; @*/ /* --END-- */ { /* --BEGIN-- */ - /*@ extract Owned, j; @*/ + /*@ focus RW, j; @*/ /* --END-- */ p[j] = 0; j++; diff --git a/src/examples/init_array2.c b/src/examples/init_array2.c index f447f553..5f49e1eb 100644 --- a/src/examples/init_array2.c +++ b/src/examples/init_array2.c @@ -1,25 +1,25 @@ void init_array2 (char *p, unsigned int n) /*@ requires take A = each(u32 i; i < n) { - Block( array_shift(p, i)) }; + W( array_shift(p, i)) }; ensures take A_post = each(u32 i; i < n) { - Owned( array_shift(p, i)) }; + RW( array_shift(p, i)) }; @*/ { unsigned int j = 0; while (j < n) /* --BEGIN-- */ /*@ inv take Al = each(u32 i; i < j) { - Owned( array_shift(p, i)) }; + RW( array_shift(p, i)) }; take Ar = each(u32 i; j <= i && i < n) { - Block( array_shift(p, i)) }; + W( array_shift(p, i)) }; {p} unchanged; {n} unchanged; j <= n; @*/ /* --END-- */ { /* --BEGIN-- */ - /*@ extract Block, j; @*/ - /*@ extract Owned, j; @*/ + /*@ focus W, j; @*/ + /*@ focus RW, j; @*/ /* --END-- */ p[j] = 0; j++; diff --git a/src/examples/init_array_rev.c b/src/examples/init_array_rev.c index e46b4f3f..dbf9e98d 100644 --- a/src/examples/init_array_rev.c +++ b/src/examples/init_array_rev.c @@ -1,26 +1,26 @@ void init_array_rev (char *p, unsigned int n) /*@ requires take A = each(u32 i; i < n) { - Block( array_shift(p, i)) }; + W( array_shift(p, i)) }; n > 0u32; ensures take A_post = each(u32 i; i < n) { - Owned( array_shift(p, i)) }; + RW( array_shift(p, i)) }; @*/ { unsigned int j = 0; while (j < n) /* --BEGIN-- */ /*@ inv take Al = each(u32 i; i < n-j) { - Block( array_shift(p, i)) }; + W( array_shift(p, i)) }; take Ar = each(u32 i; n-j <= i && i < n) { - Owned( array_shift(p, i)) }; + RW( array_shift(p, i)) }; {p} unchanged; {n} unchanged; 0u32 <= j && j <= n; @*/ /* --END-- */ { /* --BEGIN-- */ - /*@ extract Block, n-(j+1u32); @*/ - /*@ extract Owned, n-(j+1u32); @*/ + /*@ focus W, n-(j+1u32); @*/ + /*@ focus RW, n-(j+1u32); @*/ /* --END-- */ p[n-(j+1)] = 0; j++; diff --git a/src/examples/init_point.c b/src/examples/init_point.c index 4ecb67f3..e5ba7d63 100644 --- a/src/examples/init_point.c +++ b/src/examples/init_point.c @@ -1,6 +1,6 @@ void zero (int *coord) -/*@ requires take Coord = Block(coord); - ensures take Coord_post = Owned(coord); +/*@ requires take Coord = W(coord); + ensures take Coord_post = RW(coord); Coord_post == 0i32; @*/ { *coord = 0; @@ -9,8 +9,8 @@ void zero (int *coord) struct point { int x; int y; }; void init_point(struct point *p) -/*@ requires take P = Block(p); - ensures take P_post = Owned(p); +/*@ requires take P = W(p); + ensures take P_post = RW(p); P_post.x == 0i32; P_post.y == 0i32; @*/ diff --git a/src/examples/queue/pop_unified.c b/src/examples/queue/pop_unified.c index cecaa39b..db909209 100644 --- a/src/examples/queue/pop_unified.c +++ b/src/examples/queue/pop_unified.c @@ -7,7 +7,7 @@ predicate (result) Queue_pop_lemma(pointer front, pointer back, i32 popped) { if (is_null(front)) { return { after: Nil{}, before: Snoc(Nil{}, popped) }; } else { - take B = Owned(back); + take B = RW(back); assert (is_null(B.next)); take L = QueueAux (front, back); return { after: Snoc(L, B.first), before: Snoc(Cons {Head: popped, Tail: L}, B.first) }; @@ -19,10 +19,10 @@ void snoc_fact(struct queue_cell *front, struct queue_cell *back, int x) /*@ requires take Q = QueueAux(front, back); - take B = Owned(back); + take B = RW(back); ensures take Q_post = QueueAux(front, back); - take B_post = Owned(back); + take B_post = RW(back); Q == Q_post; B == B_post; let L = Snoc (Cons{Head: x, Tail: Q}, B.first); Hd(L) == x; diff --git a/src/examples/queue/push_induction.c b/src/examples/queue/push_induction.c index 06c0117f..807bf66b 100644 --- a/src/examples/queue/push_induction.c +++ b/src/examples/queue/push_induction.c @@ -7,13 +7,13 @@ void push_induction(struct queue_cell* front requires ptr_eq(front, second_last) || !addr_eq(front, second_last); take Q = QueueAux(front, second_last); - take Second_last = Owned(second_last); + take Second_last = RW(second_last); ptr_eq(Second_last.next, last); - take Last = Owned(last); + take Last = RW(last); ensures ptr_eq(front, last) || !addr_eq(front, last); take Q_post = QueueAux(front, last); - take Last2 = Owned(last); + take Last2 = RW(last); Q_post == Snoc(Q, Second_last.first); Last == Last2; @*/ diff --git a/src/examples/read.broken.c b/src/examples/read.broken.c index 1ec35621..8fd7ebaa 100644 --- a/src/examples/read.broken.c +++ b/src/examples/read.broken.c @@ -1,5 +1,5 @@ int read (int *p) -/*@ requires take v1 = Owned(p); @*/ +/*@ requires take v1 = RW(p); @*/ { return *p; } diff --git a/src/examples/read.c b/src/examples/read.c index 04892f56..b9cfe2d1 100644 --- a/src/examples/read.c +++ b/src/examples/read.c @@ -1,7 +1,7 @@ int read (int *p) /* --BEGIN-- */ -/*@ requires take P = Owned(p); - ensures take P_post = Owned(p); +/*@ requires take P = RW(p); + ensures take P_post = RW(p); @*/ /* --END-- */ { diff --git a/src/examples/read2.c b/src/examples/read2.c index 94ca64ea..376f1331 100644 --- a/src/examples/read2.c +++ b/src/examples/read2.c @@ -1,6 +1,6 @@ int read (int *p) -/*@ requires take P = Owned(p); - ensures take P_post = Owned(p); +/*@ requires take P = RW(p); + ensures take P_post = RW(p); return == P; P_post == P; @*/ diff --git a/src/examples/slf0_basic_incr.c b/src/examples/slf0_basic_incr.c index 51aa8f43..51105193 100644 --- a/src/examples/slf0_basic_incr.c +++ b/src/examples/slf0_basic_incr.c @@ -1,6 +1,6 @@ void incr (unsigned int *p) -/*@ requires take n1 = Owned(p); - ensures take n2 = Owned(p); +/*@ requires take n1 = RW(p); + ensures take n2 = RW(p); n2 == n1 + 1u32; @*/ { diff --git a/src/examples/slf0_basic_incr.signed.broken.c b/src/examples/slf0_basic_incr.signed.broken.c index 3fbd627d..6ade0b32 100644 --- a/src/examples/slf0_basic_incr.signed.broken.c +++ b/src/examples/slf0_basic_incr.signed.broken.c @@ -1,6 +1,6 @@ void incr (int *p) -/*@ requires take P = Block(p); - ensures take P_post = Owned(p); +/*@ requires take P = W(p); + ensures take P_post = RW(p); @*/ { *p = *p+1; diff --git a/src/examples/slf0_basic_incr.signed.c b/src/examples/slf0_basic_incr.signed.c index 2986c617..e8f04e84 100644 --- a/src/examples/slf0_basic_incr.signed.c +++ b/src/examples/slf0_basic_incr.signed.c @@ -1,7 +1,7 @@ void incr (int *p) -/*@ requires take P = Owned(p); +/*@ requires take P = RW(p); ((i64) P) + 1i64 <= (i64) MAXi32(); - ensures take P_post = Owned(p); + ensures take P_post = RW(p); P_post == P + 1i32; @*/ { diff --git a/src/examples/slf0_incr.broken.c b/src/examples/slf0_incr.broken.c index 995e5c0e..dc1567e2 100644 --- a/src/examples/slf0_incr.broken.c +++ b/src/examples/slf0_incr.broken.c @@ -1,7 +1,7 @@ void incr (int *p) /* --BEGIN-- */ -/*@ requires take v1 = Block(p); - ensures take v2 = Owned(p); +/*@ requires take v1 = W(p); + ensures take v2 = RW(p); v2 == v1+1i32; @*/ /* --END-- */ { diff --git a/src/examples/slf10_basic_ref.c b/src/examples/slf10_basic_ref.c index 49c2ad45..a516bb74 100644 --- a/src/examples/slf10_basic_ref.c +++ b/src/examples/slf10_basic_ref.c @@ -1,7 +1,7 @@ extern unsigned int *refUnsignedInt (unsigned int v); /*@ spec refUnsignedInt(u32 v); requires true; - ensures take vr = Owned(return); + ensures take vr = RW(return); vr == v; @*/ diff --git a/src/examples/slf11_basic_ref_greater.c b/src/examples/slf11_basic_ref_greater.c index 2ccf25eb..7f7d1e4d 100644 --- a/src/examples/slf11_basic_ref_greater.c +++ b/src/examples/slf11_basic_ref_greater.c @@ -2,9 +2,9 @@ unsigned int *ref_greater (unsigned int *p) /* --BEGIN-- */ -/*@ requires take n1 = Owned(p); - ensures take n2 = Owned(p); - take m2 = Owned(return); +/*@ requires take n1 = RW(p); + ensures take n2 = RW(p); + take m2 = RW(return); n2 == n1; m2 == n1 + 1u32; @*/ diff --git a/src/examples/slf12_basic_ref_greater_abstract.c b/src/examples/slf12_basic_ref_greater_abstract.c index cc499767..b057989f 100644 --- a/src/examples/slf12_basic_ref_greater_abstract.c +++ b/src/examples/slf12_basic_ref_greater_abstract.c @@ -2,10 +2,10 @@ unsigned int *ref_greater (unsigned int *p) /* --BEGIN-- */ -/*@ requires take n1 = Owned(p); +/*@ requires take n1 = RW(p); n1 < n1 + 1u32; - ensures take n2 = Owned(p); - take m2 = Owned(return); + ensures take n2 = RW(p); + take m2 = RW(return); n2 == n1; m2 > n1; @*/ diff --git a/src/examples/slf13_basic_ref_with_frame.c b/src/examples/slf13_basic_ref_with_frame.c index b8129a9d..44ff474d 100644 --- a/src/examples/slf13_basic_ref_with_frame.c +++ b/src/examples/slf13_basic_ref_with_frame.c @@ -2,10 +2,10 @@ unsigned int *triple_ref_with_frame(unsigned int *p_, unsigned int v) /* --BEGIN-- */ -/*@ requires take v_1 = Owned(p_); - ensures take v_2 = Owned(p_); +/*@ requires take v_1 = RW(p_); + ensures take v_2 = RW(p_); v_2 == v_1; - take vr = Owned(return); + take vr = RW(return); vr == v; @*/ /* --END-- */ diff --git a/src/examples/slf17_get_and_free.c b/src/examples/slf17_get_and_free.c index a2238315..a194f69b 100644 --- a/src/examples/slf17_get_and_free.c +++ b/src/examples/slf17_get_and_free.c @@ -1,7 +1,7 @@ #include "free.h" unsigned int get_and_free (unsigned int *p) -/*@ requires take P = Owned(p); +/*@ requires take P = RW(p); ensures return == P; @*/ { diff --git a/src/examples/slf3_basic_inplace_double.c b/src/examples/slf3_basic_inplace_double.c index ca7cddde..2fcd00f9 100644 --- a/src/examples/slf3_basic_inplace_double.c +++ b/src/examples/slf3_basic_inplace_double.c @@ -1,9 +1,9 @@ void inplace_double (int *p) /* --BEGIN-- */ -/*@ requires take P = Owned(p); +/*@ requires take P = RW(p); let M = 2i64 * ((i64) P); (i64) MINi32() <= M; M <= (i64) MAXi32(); - ensures take P_post = Owned(p); + ensures take P_post = RW(p); P_post == (i32) M; @*/ /* --END-- */ diff --git a/src/examples/slf4_basic_incr_two.c b/src/examples/slf4_basic_incr_two.c index e81f6054..ed1f7b36 100644 --- a/src/examples/slf4_basic_incr_two.c +++ b/src/examples/slf4_basic_incr_two.c @@ -1,10 +1,10 @@ #include "slf0_basic_incr.c" void incr_two (unsigned int *p, unsigned int *q) -/*@ requires take n1 = Owned(p); - take m1 = Owned(q); - ensures take n2 = Owned(p); - take m2 = Owned(q); +/*@ requires take n1 = RW(p); + take m1 = RW(q); + ensures take n2 = RW(p); + take m2 = RW(q); n2 == n1 + 1u32; m2 == m1 + 1u32; @*/ diff --git a/src/examples/slf5_basic_aliased_call.broken.c b/src/examples/slf5_basic_aliased_call.broken.c index 681ae115..413bffe3 100644 --- a/src/examples/slf5_basic_aliased_call.broken.c +++ b/src/examples/slf5_basic_aliased_call.broken.c @@ -1,8 +1,8 @@ #include "slf4_basic_incr_two.c" void aliased_call (unsigned int *p) -/*@ requires take n1 = Owned(p); - ensures take n2 = Owned(p); +/*@ requires take n1 = RW(p); + ensures take n2 = RW(p); n2 == n1 + 2u32; @*/ { incr_two(p, p); diff --git a/src/examples/slf6_basic_incr_two_aliased_call.c b/src/examples/slf6_basic_incr_two_aliased_call.c index 6d96c659..e18e39db 100644 --- a/src/examples/slf6_basic_incr_two_aliased_call.c +++ b/src/examples/slf6_basic_incr_two_aliased_call.c @@ -2,9 +2,9 @@ void incr_two (unsigned int *p, unsigned int *q) -/*@ requires take n1 = Owned(p); +/*@ requires take n1 = RW(p); ptr_eq(q,p); - ensures take n2 = Owned(p); + ensures take n2 = RW(p); n2 == n1 + 2u32; @*/ { @@ -15,8 +15,8 @@ void incr_two (unsigned int *p, unsigned int *q) void aliased_call (unsigned int *p) -/*@ requires take n1 = Owned(p); - ensures take n2 = Owned(p); +/*@ requires take n1 = RW(p); + ensures take n2 = RW(p); n2 == n1 + 2u32; @*/ { diff --git a/src/examples/slf7_basic_incr_first.c b/src/examples/slf7_basic_incr_first.c index cfe34d75..37f63d63 100644 --- a/src/examples/slf7_basic_incr_first.c +++ b/src/examples/slf7_basic_incr_first.c @@ -1,10 +1,10 @@ #include "slf0_basic_incr.c" void incr_first(unsigned int *p, unsigned int *q) -/*@ requires take n1 = Owned(p); - take m1 = Owned(q); - ensures take n2 = Owned(p); - take m2 = Owned(q); +/*@ requires take n1 = RW(p); + take m1 = RW(q); + ensures take n2 = RW(p); + take m2 = RW(q); n2 == n1 + 1u32; m2 == m1; @*/ @@ -14,8 +14,8 @@ void incr_first(unsigned int *p, unsigned int *q) void incr_first_(unsigned int *p, unsigned int *q) -/*@ requires take n1 = Owned(p); - ensures take n2 = Owned(p); +/*@ requires take n1 = RW(p); + ensures take n2 = RW(p); n2 == n1 + 1u32; @*/ { diff --git a/src/examples/slf8_basic_transfer.c b/src/examples/slf8_basic_transfer.c index 71a80c6a..409a0d0e 100644 --- a/src/examples/slf8_basic_transfer.c +++ b/src/examples/slf8_basic_transfer.c @@ -1,9 +1,9 @@ void transfer (unsigned int *p, unsigned int *q) /* --BEGIN-- */ -/*@ requires take P = Owned(p); - take Q = Owned(q); - ensures take P_post = Owned(p); - take Q_post = Owned(q); +/*@ requires take P = RW(p); + take Q = RW(q); + ensures take P_post = RW(p); + take Q_post = RW(q); P_post == P + Q; Q_post == 0u32; @*/ diff --git a/src/examples/slf9_basic_transfer_aliased.c b/src/examples/slf9_basic_transfer_aliased.c index a3ab3b73..53c4da63 100644 --- a/src/examples/slf9_basic_transfer_aliased.c +++ b/src/examples/slf9_basic_transfer_aliased.c @@ -1,7 +1,7 @@ void transfer (unsigned int *p, unsigned int *q) -/*@ requires take n1 = Owned(p); +/*@ requires take n1 = RW(p); ptr_eq(p,q); - ensures take n2 = Owned(p); + ensures take n2 = RW(p); n2 == 0u32; @*/ { diff --git a/src/examples/slf_incr2.c b/src/examples/slf_incr2.c index 6ed25927..a0efd759 100644 --- a/src/examples/slf_incr2.c +++ b/src/examples/slf_incr2.c @@ -1,21 +1,21 @@ /*@ -predicate { u32 P, u32 Q } BothOwned (pointer p, pointer q) +predicate { u32 P, u32 Q } BothRW (pointer p, pointer q) { if (ptr_eq(p,q)) { - take PX = Owned(p); + take PX = RW(p); return {P: PX, Q: PX}; } else { - take PX = Owned(p); - take QX = Owned(q); + take PX = RW(p); + take QX = RW(q); return {P: PX, Q: QX}; } } @*/ void incr2(unsigned int *p, unsigned int *q) -/*@ requires take PQ = BothOwned(p,q); - ensures take PQ_post = BothOwned(p,q); +/*@ requires take PQ = BothRW(p,q); + ensures take PQ_post = BothRW(p,q); PQ_post.P == (!ptr_eq(p,q) ? (PQ.P + 1u32) : (PQ.P + 2u32)); PQ_post.Q == (!ptr_eq(p,q) ? (PQ.Q + 1u32) : PQ_post.P); @*/ @@ -30,11 +30,11 @@ void incr2(unsigned int *p, unsigned int *q) } void call_both_better(unsigned int *p, unsigned int *q) -/*@ requires take P = Owned(p); - take Q = Owned(q); +/*@ requires take P = RW(p); + take Q = RW(q); !ptr_eq(p,q); - ensures take P_post = Owned(p); - take Q_post = Owned(q); + ensures take P_post = RW(p); + take Q_post = RW(q); P_post == P + 3u32; Q_post == Q + 1u32; @*/ diff --git a/src/examples/slf_incr2_alias.c b/src/examples/slf_incr2_alias.c index 2f8cd75c..f50484ab 100644 --- a/src/examples/slf_incr2_alias.c +++ b/src/examples/slf_incr2_alias.c @@ -1,9 +1,9 @@ // Increment two different pointers (same as above) void incr2a (unsigned int *p, unsigned int *q) -/*@ requires take P = Owned(p); - take Q = Owned(q); - ensures take P_post = Owned(p); - take Q_post = Owned(q); +/*@ requires take P = RW(p); + take Q = RW(q); + ensures take P_post = RW(p); + take Q_post = RW(q); P_post == P + 1u32; Q_post == Q + 1u32; @*/ @@ -18,9 +18,9 @@ void incr2a (unsigned int *p, unsigned int *q) // Increment the same pointer twice void incr2b (unsigned int *p, unsigned int *q) -/*@ requires take P = Owned(p); +/*@ requires take P = RW(p); ptr_eq(q,p); - ensures take P_post = Owned(p); + ensures take P_post = RW(p); ptr_eq(q,p); P_post == P + 2u32; @*/ @@ -34,10 +34,10 @@ void incr2b (unsigned int *p, unsigned int *q) } void call_both (unsigned int *p, unsigned int *q) -/*@ requires take pv = Owned(p); - take qv = Owned(q); - ensures take pv_ = Owned(p); - take qv_ = Owned(q); +/*@ requires take pv = RW(p); + take qv = RW(q); + ensures take pv_ = RW(p); + take qv_ = RW(q); pv_ == pv + 3u32; qv_ == qv + 1u32; @*/ diff --git a/src/examples/slf_incr2_noalias.c b/src/examples/slf_incr2_noalias.c index 7c7e2369..91dedd2d 100644 --- a/src/examples/slf_incr2_noalias.c +++ b/src/examples/slf_incr2_noalias.c @@ -1,8 +1,8 @@ void incr2a (unsigned int *p, unsigned int *q) -/*@ requires take P = Owned(p); - take Q = Owned(q); - ensures take P_post = Owned(p); - take Q_post = Owned(q); +/*@ requires take P = RW(p); + take Q = RW(q); + ensures take P_post = RW(p); + take Q_post = RW(q); P_post == P + 1u32; Q_post == Q + 1u32; @*/ diff --git a/src/examples/slf_length_acc.c b/src/examples/slf_length_acc.c index f3fa4389..4b5759e9 100644 --- a/src/examples/slf_length_acc.c +++ b/src/examples/slf_length_acc.c @@ -17,9 +17,9 @@ function [rec] (u32) length(datatype List xs) { void IntList_length_acc_aux (struct sllist *xs, unsigned int *p) /*@ requires take L1 = SLList_At(xs); - take P = Owned(p); + take P = RW(p); ensures take L1_post = SLList_At(xs); - take P_post = Owned(p); + take P_post = RW(p); L1 == L1_post; P_post == P + length(L1); @*/ diff --git a/src/examples/slf_quadruple_mem.c b/src/examples/slf_quadruple_mem.c index c7a86dc3..dd7f8ea0 100644 --- a/src/examples/slf_quadruple_mem.c +++ b/src/examples/slf_quadruple_mem.c @@ -1,9 +1,9 @@ int quadruple_mem (int *p) /* --BEGIN-- */ -/*@ requires take P = Owned(p); +/*@ requires take P = RW(p); let P64 = (i64) P; (i64)MINi32() <= P64 * 4i64; P64 * 4i64 <= (i64)MAXi32(); - ensures take P_post = Owned(p); + ensures take P_post = RW(p); P_post == P; return == 4i32 * P; @*/ diff --git a/src/examples/slf_ref_greater.c b/src/examples/slf_ref_greater.c index 96138e91..ca2a16fe 100644 --- a/src/examples/slf_ref_greater.c +++ b/src/examples/slf_ref_greater.c @@ -2,10 +2,10 @@ unsigned int *ref_greater_abstract (unsigned int *p) /* --BEGIN-- */ -/*@ requires take P = Owned(p); +/*@ requires take P = RW(p); P < 4294967295u32; - ensures take P_post = Owned(p); - take R = Owned(return); + ensures take P_post = RW(p); + take R = RW(return); P == P_post; P <= R; @*/ diff --git a/src/examples/slf_sized_stack.c b/src/examples/slf_sized_stack.c index 929d6bef..06ae0b81 100644 --- a/src/examples/slf_sized_stack.c +++ b/src/examples/slf_sized_stack.c @@ -11,7 +11,7 @@ struct sized_stack type_synonym SizedStack = {u32 Size, datatype List Data} predicate (SizedStack) SizedStack_At (pointer p) { - take P = Owned(p); + take P = RW(p); take D = SLList_At(P.data); assert(P.size == Length(D)); return { Size: P.size, Data: D }; @@ -22,13 +22,13 @@ extern struct sized_stack *malloc__sized_stack(); /*@ spec malloc__sized_stack(); requires true; - ensures take R = Block(return); + ensures take R = W(return); @*/ extern void *free__sized_stack(struct sized_stack *s); /*@ spec free__sized_stack(pointer s); - requires take R = Block(s); + requires take R = W(s); ensures true; @*/ diff --git a/src/examples/swap.c b/src/examples/swap.c index 435ef1b0..8191331b 100644 --- a/src/examples/swap.c +++ b/src/examples/swap.c @@ -1,9 +1,9 @@ void swap (unsigned int *p, unsigned int *q) /* --BEGIN-- */ -/*@ requires take P = Owned(p); - take Q = Owned(q); - ensures take P_post = Owned(p); - take Q_post = Owned(q); +/*@ requires take P = RW(p); + take Q = RW(q); + ensures take P_post = RW(p); + take Q_post = RW(q); P_post == Q && Q_post == P; @*/ /* --END-- */ diff --git a/src/examples/swap_array.c b/src/examples/swap_array.c index 8cb18d67..41d5fa6c 100644 --- a/src/examples/swap_array.c +++ b/src/examples/swap_array.c @@ -1,20 +1,20 @@ void swap_array (int *p, int n, int i, int j) /* --BEGIN-- */ -/*@ requires take a1 = each(i32 k; 0i32 <= k && k < n) { Owned(array_shift(p,k)) }; +/*@ requires take a1 = each(i32 k; 0i32 <= k && k < n) { RW(array_shift(p,k)) }; 0i32 <= i && i < n; 0i32 <= j && j < n; j != i; - ensures take a2 = each(i32 k; 0i32 <= k && k < n) { Owned(array_shift(p,k)) }; + ensures take a2 = each(i32 k; 0i32 <= k && k < n) { RW(array_shift(p,k)) }; a2 == a1[i: a1[j], j: a1[i]]; @*/ /* --END-- */ { /* --BEGIN-- */ - /*@ extract Owned, i; @*/ + /*@ focus RW, i; @*/ /* --END-- */ int tmp = p[i]; /* --BEGIN-- */ - /*@ extract Owned, j; @*/ + /*@ focus RW, j; @*/ /* --END-- */ p[i] = p[j]; p[j] = tmp; diff --git a/src/examples/transpose.broken.c b/src/examples/transpose.broken.c index 47ef9479..7549408a 100644 --- a/src/examples/transpose.broken.c +++ b/src/examples/transpose.broken.c @@ -1,8 +1,8 @@ struct point { int x; int y; }; void transpose (struct point *p) -/*@ requires take P = Owned(p); - ensures take P_post = Owned(p); +/*@ requires take P = RW(p); + ensures take P_post = RW(p); P_post.x == P.y; P_post.y == P.x; @*/ diff --git a/src/examples/transpose.c b/src/examples/transpose.c index 03b1d9d8..bfad9b6d 100644 --- a/src/examples/transpose.c +++ b/src/examples/transpose.c @@ -1,8 +1,8 @@ struct point { int x; int y; }; void transpose (struct point *p) -/*@ requires take P = Owned(p); - ensures take P_post = Owned(p); +/*@ requires take P = RW(p); + ensures take P_post = RW(p); P_post.x == P.y; P_post.y == P.x; @*/ diff --git a/src/examples/transpose2.c b/src/examples/transpose2.c index 31b390fd..63bde377 100644 --- a/src/examples/transpose2.c +++ b/src/examples/transpose2.c @@ -1,8 +1,8 @@ void swap (unsigned int *p, unsigned int *q) -/*@ requires take P = Owned(p); - take Q = Owned(q); - ensures take P_post = Owned(p); - take Q_post = Owned(q); +/*@ requires take P = RW(p); + take Q = RW(q); + ensures take P_post = RW(p); + take Q_post = RW(q); P_post == Q && Q_post == P; @*/ { @@ -16,8 +16,8 @@ struct upoint { unsigned int x; unsigned int y; }; void transpose2 (struct upoint *p) /* --BEGIN-- */ -/*@ requires take P = Owned(p); - ensures take P_post = Owned(p); +/*@ requires take P = RW(p); + ensures take P_post = RW(p); P_post.x == P.y; P_post.y == P.x; @*/ diff --git a/src/examples/zero.c b/src/examples/zero.c index c7fbf8c7..56062d43 100644 --- a/src/examples/zero.c +++ b/src/examples/zero.c @@ -1,7 +1,7 @@ void zero (int *p) /* --BEGIN-- */ -/*@ requires take P = Block(p); - ensures take P_post = Owned(p); +/*@ requires take P = W(p); + ensures take P_post = RW(p); P_post == 0i32; @*/ /* --END-- */ diff --git a/src/underconstruction/bst/getter.c b/src/underconstruction/bst/getter.c index f3983af8..a05c50fd 100644 --- a/src/underconstruction/bst/getter.c +++ b/src/underconstruction/bst/getter.c @@ -23,10 +23,10 @@ int get_Tree_Data (struct node *t) struct node* get_Tree_Left (struct node *t) /* FILL IN HERE */ /* --BEGIN-- */ -/*@ requires take v1 = Owned(t); - take v1_left = Owned(v1.left); - ensures take v2 = Owned(t); - take v2_left = Owned(v2.left); +/*@ requires take v1 = RW(t); + take v1_left = RW(v1.left); + ensures take v2 = RW(t); + take v2_left = RW(v2.left); v1 == v2 && v1_left == v2_left; ptr_eq(return, ((is_null(t)) ? (t) : (v1.left))); @*/ /* --END-- */ @@ -44,10 +44,10 @@ struct node* get_Tree_Left (struct node *t) struct node* get_Tree_Right (struct node *t) /* FILL IN HERE */ /* --BEGIN-- */ -/*@ requires take v1 = Owned(t); - take v1_right = Owned(v1.right); - ensures take v2 = Owned(t); - take v2_right = Owned(v2.right); +/*@ requires take v1 = RW(t); + take v1_right = RW(v1.right); + ensures take v2 = RW(t); + take v2_right = RW(v2.right); v1 == v2 && v1_right == v2_right; ptr_eq(return, ((is_null(t)) ? (t) : (v1.right))); @*/ /* --END-- */ From 22375b43d2f52f8d35e9c51d8185ef0b51cd79d6 Mon Sep 17 00:00:00 2001 From: Dhruv Makwana Date: Wed, 12 Mar 2025 19:05:14 +0000 Subject: [PATCH 2/2] Update deprecated keywords in tutorial --- src/tutorial.md | 200 ++++++++++++++++++++++-------------------------- 1 file changed, 93 insertions(+), 107 deletions(-) diff --git a/src/tutorial.md b/src/tutorial.md index 6c62e1ea..8dcb0142 100644 --- a/src/tutorial.md +++ b/src/tutorial.md @@ -186,7 +186,7 @@ statement, CN lists the typechecked sub-expressions, and the memory accesses and function calls within these. In our example, there is only one possible control-flow path: entering -the function body (section "`function body`") and executing the block +the function body (section "`function body`") and executing the W from lines 2 to 4, followed by the return statement at line 3. The entry for the latter contains the sequence of sub-expressions in the return statement, including reads of the variables `x` and `y`. @@ -325,31 +325,17 @@ cn verify exercises/read.c exercises/read.c:3:10: error: Missing resource for reading return \*p; ^~ -Resource needed: Owned(p) +Resource needed: RW(p) Consider the state in /var/folders/\_v/ndl32wpj4bb3y9dg11rvc8ph0000gn/T/state_403624.html ``` -For the read `*p` to be safe, ownership of a resource is missing: a resource `Owned(p)`. +For the read `*p` to be safe, ownership of a resource is missing: a resource `RW(p)`. -### Owned resources +### RW resources - +Given a C-type `T` and pointer `p`, the resource `RW(p)` asserts the ability to read and write that memory cell at location `p` of the size of C-type `T`. It is CN’s equivalent of a points-to assertion in separation logic (indexed by C-types `T`). - - -Given a C-type `T` and pointer `p`, the resource `Owned(p)` asserts ownership of a memory cell at location `p` of the size of C-type `T`. It is CN’s equivalent of a points-to assertion in separation logic (indexed by C-types `T`). - -In this example we can ensure the safe execution of `read` by adding a precondition that requires ownership of `Owned(p)`, as shown below. For now ignore the notation `take ... = Owned(p)`. Since reading the pointer does not disturb its value, we also add a corresponding postcondition, whereby `read` returns ownership of `p` after it is finished executing, in the form of another `Owned(p)` resource. +In this example we can ensure the safe execution of `read` by adding a precondition that requires ownership of `RW(p)`, as shown below. For now ignore the notation `take ... = RW(p)`. Since reading the pointer does not disturb its value, we also add a corresponding postcondition, whereby `read` returns ownership of `p` after it is finished executing, in the form of another `RW(p)` resource. ```c title="solutions/read.c" --8<-- @@ -359,9 +345,9 @@ solutions/read.c This specification means that: -- any function calling `read` has to be able to provide a resource `Owned(p)` to pass into `read`, and +- any function calling `read` has to be able to provide a resource `RW(p)` to pass into `read`, and -- the caller will receive back a resource `Owned(p)` when `read` returns. +- the caller will receive back a resource `RW(p)` when `read` returns. ### Resource outputs @@ -369,12 +355,12 @@ A caller of `read` may also wish to know that `read` actually returns the correc -In CN, resources have _outputs_. Each resource outputs the information that can be derived from ownership of the resource. What information is returned is specific to the type of resource. A resource `Owned(p)` (for some C-type `T`) outputs the _pointee value_ of `p`, since that can be derived from the resource ownership: assume you have a pointer `p` and the associated ownership, then this uniquely determines the pointee value of `p`. +In CN, resources have _outputs_. Each resource outputs the information that can be derived from ownership of the resource. What information is returned is specific to the type of resource. A resource `RW(p)` (for some C-type `T`) outputs the _pointee value_ of `p`, since that can be derived from the resource ownership: assume you have a pointer `p` and the associated ownership, then this uniquely determines the pointee value of `p`. -CN uses the `take`-notation seen in the example above to bind the output of a resource to a new name. The precondition `take P = Owned(p)` does two things: (1) it assert ownership of resource `Owned(p)`, and (2) it binds the name `P` to the resource output, here the pointee value of `p` at the start of the function. Similarly, the postcondition introduces the name `P_post` for the pointee value on function return. +CN uses the `take`-notation seen in the example above to bind the output of a resource to a new name. The precondition `take P = RW(p)` does two things: (1) it assert ownership of resource `RW(p)`, and (2) it binds the name `P` to the resource output, here the pointee value of `p` at the start of the function. Similarly, the postcondition introduces the name `P_post` for the pointee value on function return. @@ -424,14 +410,14 @@ CN rejects this program with the following message: ``` cn verify exercises/read.broken.c [1/1]: read -build/exercises/read.broken.c:4:3: error: Left_Sublist-over unused resource 'Owned(p)(v1)' +build/exercises/read.broken.c:4:3: error: Left_Sublist-over unused resource 'RW(p)(v1)' return \*p; ^~~~~~~~~~ Consider the state in /var/folders/\_v/ndl32wpj4bb3y9dg11rvc8ph0000gn/T/state_17eb4a.html ``` CN has typechecked the function and verified (1) that it is safe to -execute under the precondition (given ownership `Owned(p)`) +execute under the precondition (given ownership `RW(p)`) and (2) that the function (vacuously) satisfies its postcondition. But following the check of the postcondition it finds that not all resources have been "`used up`". @@ -465,40 +451,40 @@ exercises/abs_mem.c --8<-- ``` -### Block resources +### W resources -Aside from the `Owned` resources seen so far, CN has another -built-in type of resource called `Block`. Given a C-type `T` and -pointer `p`, `Block(p)` asserts the same ownership as -`Owned(p)` — ownership of a memory cell at `p` the size of type -`T` — but, in contrast to `Owned`, `Block` memory is not assumed -to be initialised. +Aside from the `RW` resources seen so far, CN has another +built-in type of resource called `W`. Given a C-type `T` and +pointer `p`, `W(p)` is similar to +`RW(p)` — referring to a memory cell at `p` the size of type +`T` — but, in contrast to `RW`, `W` memory is not assumed +to be initialised, and thus is write-only. CN uses this distinction to prevent reads from uninitialised memory: - A read at C-type `T` and pointer `p` requires a resource - `Owned(p)`, i.e., ownership of _initialised_ memory at the - right C-type. The load returns the `Owned` resource unchanged. + `RW(p)`, i.e., ownership of _initialised_ memory at the + right C-type. The load returns the `RW` resource unchanged. - A write at C-type `T` and pointer `p` needs only a -`Block(p)` (so, unlike reads, writes to uninitialised memory -are fine). The write consumes ownership of the `Block` resource -(it destroys it) and returns a new resource `Owned(p)` with the -value written as the output. This means the resource returned from a +`W(p)` (so, unlike reads, writes to uninitialised memory +are fine). The write consumes ownership of the `W` resource +(it destroys it) and returns a new resource `RW(p)` with the +value written as its output. This means the resource returned from a write records the fact that this memory cell is now initialised and can be read from. - + -Since `Owned` carries the same ownership as `Block`, just with the -additional information that the `Owned` memory is initalised, a -resource `Owned(p)` is "`at least as good`" as `Block(p)` — -an `Owned(p)` resource can be used whenever `Block(p)` is +Since `RW` carries the same ownership as `W`, just with the +additional information that the `RW` memory is initalised, a +resource `RW(p)` is "`at least as good`" as `W(p)` — +an `RW(p)` resource can be used whenever `W(p)` is needed. For instance CN’s type checking of a write to `p` requires a -`Block(p)`, but if an `Owned(p)` resource is what is +`W(p)`, but if an `RW(p)` resource is what is available, this can be used just the same. This allows an already-initialised memory cell to be over-written again. -Unlike `Owned`, whose output is the pointee value, `Block` has no meaningful output. +Unlike `RW`, whose output is the pointee value, `W` has no meaningful output. ### Writing through pointers @@ -510,7 +496,7 @@ exercises/slf0_basic_incr.signed.c --8<-- ``` -In the precondition we assert ownership of resource `Owned(p)`, +In the precondition we assert ownership of resource `RW(p)`, binding its output/pointee value to `P`, and use `P` to specify that `p` must point to a sufficiently small value at the start of the function so as not to overflow when incremented. The postcondition @@ -518,7 +504,7 @@ asserts ownership of `p` with output `P_post`, as before, and uses this to express that the value `p` points to is incremented by `incr`: `P_post == P + 1i32`. -If we incorrectly tweaked this specification and used `Block(p)` instead of `Owned(p)` in the precondition, as below, then CN would reject the program. +If we incorrectly tweaked this specification and used `W(p)` instead of `RW(p)` in the precondition, as below, then CN would reject the program. ```c title="exercises/slf0_basic_incr.signed.broken.c" --8<-- @@ -532,17 +518,17 @@ CN reports: build/solutions/slf0_basic_incr.signed.broken.c:6:11: error: Missing resource for reading int n = \*p; ^~ -Resource needed: Owned(p) +Resource needed: RW(p) Consider the state in /var/folders/\_v/ndl32wpj4bb3y9dg11rvc8ph0000gn/T/state_5da0f3.html ``` -The `Owned(p)` resource required for reading is missing, since, per the precondition, only `Block(p)` is available. Checking the linked HTML file confirms this. Here the section "`Available resources`" lists all resource ownership at the point of the failure: +The `RW(p)` resource required for reading is missing, since, per the precondition, only `W(p)` is available. Checking the linked HTML file confirms this. Here the section "`Available resources`" lists all resource ownership at the point of the failure: -- `Block(p)(u)`, i.e., ownership of uninitialised memory +- `W(p)(u)`, i.e., ownership of uninitialised memory at location `p`; the output is a `void`/`unit` value `u` (specified in the second pair of parentheses) -- `Owned(&ARG0)(p)`, the ownership of (initialised) +- `RW(&ARG0)(p)`, the ownership of (initialised) memory at location `&ARG0`, i.e., the memory location where the first function argument is stored; its output is the pointer `p` (not to be confused with the pointee of `p`); and finally @@ -577,10 +563,10 @@ exercises/slf3_basic_inplace_double.c When functions manipulate multiple pointers, we can assert their ownership just like before. However pointer ownership in CN is unique -- that is, simultaneously owning -`Owned` or `Block` resources for two pointers implies that these +`RW` or `W` resources for two pointers implies that these pointers are disjoint. -The following example shows the use of two `Owned` resources for +The following example shows the use of two `RW` resources for accessing two different pointers by a function `add`, which reads two `int` values in memory, at locations `p` and `q`, and returns their sum. @@ -646,24 +632,24 @@ the members of `P` and `P_post` individually. -### Compound Owned and Block resources +### Compound RW and W resources While one might like to think of a struct as a single (compound) object that is manipulated as a whole, C permits more flexible struct manipulation: given a struct pointer, programmers can construct pointers to _individual struct members_ and manipulate these as values, including even passing them to other functions. -CN therefore cannot treat resources for compound C types like structs as primitive, indivisible units. Instead, `Owned` and `Block` are defined inductively on the structure of the C-type `T`. +CN therefore cannot treat resources for compound C types like structs as primitive, indivisible units. Instead, `RW` and `W` are defined inductively on the structure of the C-type `T`. -For struct types `T`, the `Owned` resource is defined as the collection of `Owned` resources for its members (as well as `Block` resources for any padding bytes in-between them). The resource `Block`, similarly, is made up of `Block` resources for all members (and padding bytes). +For struct types `T`, the `RW` resource is defined as the collection of `RW` resources for its members (as well as `W` resources for any padding bytes in-between them). The resource `W`, similarly, is made up of `W` resources for all members (and padding bytes). To handle code that manipulates pointers into parts of a struct object, CN can automatically decompose a struct resource into the member resources, and it can recompose the struct later, as needed. The following example illustrates this. -Recall the function `zero` from our earlier exercise. It takes an `int` pointer to uninitialised memory, with `Block` ownership, and initialises the value to zero, returning an `Owned` resource with output `0`. +Recall the function `zero` from our earlier exercise. It takes an `int` pointer to uninitialised memory, with `W` ownership, and initialises the value to zero, returning an `RW` resource with output `0`. Now consider the function `init_point`, shown below, which takes a pointer `p` to a `struct point` and zero-initialises its members by calling `zero` twice, once with a pointer to struct member `x`, and once with a pointer to `y`. @@ -673,9 +659,9 @@ exercises/init_point.c --8<-- ``` -As stated in its precondition, `init_point` receives ownership `Block(p)`. The `zero` function, however, works on `int` pointers and requires `Block` ownership. +As stated in its precondition, `init_point` receives ownership `W(p)`. The `zero` function, however, works on `int` pointers and requires `W` ownership. -CN can prove the calls to `zero` with `&p->x` and `&p->y` are safe because it decomposes the `Block(p)` into a `Block` for member `x` and a `Block` for member `y`. Later, the reverse happens: following the two calls to `zero`, as per `zero`’s precondition, `init_point` has ownership of two adjacent `Owned` resources – ownership for the two struct member pointers, with the member now initialised. Since the postcondition of `init_point` requires ownership `Owned(p)`, CN combines these back into a compound resource. The resulting `Owned` resource has for an output the struct value `P_post` that is composed of the zeroed member values for `x` and `y`. +CN can prove the calls to `zero` with `&p->x` and `&p->y` are safe because it decomposes the `W(p)` into a `W` for member `x` and a `W` for member `y`. Later, the reverse happens: following the two calls to `zero`, as per `zero`’s precondition, `init_point` has ownership of two adjacent `RW` resources – ownership for the two struct member pointers, with the member now initialised. Since the postcondition of `init_point` requires ownership `RW(p)`, CN combines these back into a compound resource. The resulting `RW` resource has for an output the struct value `P_post` that is composed of the zeroed member values for `x` and `y`. ### Resource inference @@ -691,17 +677,17 @@ exercises/transpose.broken.c --8<-- ``` -The precondition of `transpose` asserts ownership of an `Owned(p)` resource. The error report now instead lists under "`Available resources`" two resources: +The precondition of `transpose` asserts ownership of an `RW(p)` resource. The error report now instead lists under "`Available resources`" two resources: -- `Owned(member_shift(p, x))` with output `P.x` and +- `RW(member_shift(p, x))` with output `P.x` and -- `Owned(member_shift(p, y))` with output `P.y` +- `RW(member_shift(p, y))` with output `P.y` Here `member_shift(p,m)` is the CN expression that constructs, from a `struct s` pointer `p`, the "`shifted`" pointer for its member `m`. -When the function returns, the two member resources are recombined "`on demand`" to satisfy the postcondition `Owned(p)`. +When the function returns, the two member resources are recombined "`on demand`" to satisfy the postcondition `RW(p)`. ### Exercises @@ -733,7 +719,7 @@ To support reasoning about code manipulating arrays and computed pointers, CN ha ```c each (i32 i; 0i32 <= i && i < 10i32) -{ Owned(array_shift(p,i)) } +{ RW(array_shift(p,i)) } ``` In detail, this can be read as follows: @@ -742,7 +728,7 @@ In detail, this can be read as follows: - if `i` is between `0` and `10`, … -- assert ownership of a resource `Owned` … +- assert ownership of a resource `RW` … - for cell `i` of the array with base-address `p`. @@ -774,7 +760,7 @@ exercises/array_load.broken.c The CN precondition requires -- ownership of the array on entry — one `Owned` resource for each array index between `0` and `n` — and +- ownership of the array on entry — one `RW` resource for each array index between `0` and `n` — and - that `i` lies within the range of owned indices. On exit the array ownership is returned again. @@ -787,12 +773,12 @@ cn verify solutions/array_load.broken.c build/solutions/array_load.broken.c:5:10: error: Missing resource for reading return p[i]; ^~~~ -Resource needed: Owned(array_shift(p, (u64)i)) +Resource needed: RW(array_shift(p, (u64)i)) ``` -The reason is that, when searching for a required resource, such as the `Owned` resource for `p[i]` here, CN’s resource inference does not consider iterated resources. Quantifiers, as used by iterated resources, can make verification undecidable, so, in order to maintain predictable type checking, CN delegates this aspect of the reasoning to the user. +The reason is that, when searching for a required resource, such as the `RW` resource for `p[i]` here, CN’s resource inference does not consider iterated resources. Quantifiers, as used by iterated resources, can make verification undecidable, so, in order to maintain predictable type checking, CN delegates this aspect of the reasoning to the user. -To make the `Owned` resource required for accessing `p[i]` available to CN’s resource inference we have to explicitly "`extract`" ownership for index `i` out of the iterated resource. +To make the `RW` resource required for accessing `p[i]` available to CN’s resource inference we have to explicitly "`focus`" ownership for index `i` out of the iterated resource. ```c title="exercises/array_load.c" --8<-- @@ -800,10 +786,10 @@ exercises/array_load.c --8<-- ``` -Here the CN comment `/*@ extract Owned, i; @*/` is a proof hint in the form of a "`ghost statement`" that instructs CN to instantiate any available iterated `Owned` resource for index `i`. In our example this operation splits the iterated resource into two: +Here the CN comment `/*@ focus RW, i; @*/` is a proof hint in the form of a "`ghost statement`" that instructs CN to instantiate any available iterated `RW` resource for index `i`. In our example this operation splits the iterated resource into two: ```c -each(i32 j; 0i32 <= j && j < n) { Owned(array_shift(p,j)) } +each(i32 j; 0i32 <= j && j < n) { RW(array_shift(p,j)) } ``` is split into @@ -811,19 +797,19 @@ is split into 1. the instantiation of the iterated resource at `i` ```c -Owned(array_shift(p,i)) +RW(array_shift(p,i)) ``` 2. the remainder of the iterated resource, the ownership for all indices except `i` ```c each(i32 j; 0i32 <= j && j < n && j != i) - { Owned(array_shift(p,j)) } + { RW(array_shift(p,j)) } ``` -After this extraction step, CN can use the (former) extracted resource to justify the access `p[i]`. Note that an `extract` statement's second argument can be any arithmetic expression, not just a single identifier like in this example. +After this focusion step, CN can use the (former) focused resource to justify the access `p[i]`. Note that an `focus` statement's second argument can be any arithmetic expression, not just a single identifier like in this example. -Following an `extract` statement, CN remembers the extracted index and can automatically "`reverse`" the extraction when needed: after type checking the access `p[i]` CN must ensure the function’s postcondition holds, which needs the full array ownership again (including the extracted index `i`); remembering the index `i`, CN then automatically merges resources (1) and (2) again to obtain the required full array ownership, and completes the verification of the function. +Following an `focus` statement, CN remembers the focused index and can automatically "`reverse`" the focusion when needed: after type checking the access `p[i]` CN must ensure the function’s postcondition holds, which needs the full array ownership again (including the focused index `i`); remembering the index `i`, CN then automatically merges resources (1) and (2) again to obtain the required full array ownership, and completes the verification of the function. So far the specification only guarantees safe execution but does not specify the behaviour of `read`. To address this, let’s return to @@ -831,9 +817,9 @@ the iterated resources in the function specification. When we specify `take A = each ...` here, what is `A`? In CN, the output of an iterated resource is a _map_ from indices to resource outputs. In this example, where index `j` has CN type `i32` and the iterated -resource is `Owned`, the output `A` is a map from `i32` +resource is `RW`, the output `A` is a map from `i32` indices to `i32` values — CN type `map`. If the type of -`j` was `i64` and the resource `Owned`, `A` would have +`j` was `i64` and the resource `RW`, `A` would have type `map`. We can use this to refine our specification with information about the functional behaviour of `read`. @@ -844,7 +830,7 @@ exercises/array_load2.c --8<-- ``` -We specify that `read` does not change the array — the outputs of `Owned`, +We specify that `read` does not change the array — the outputs of `RW`, `A` and `A_post`, taken before and after running the function, are the same — and that the value returned is `A[i]`. @@ -861,7 +847,7 @@ exercises/add_two_array.c ``` @@ -878,18 +864,18 @@ exercises/swap_array.c TODO: BCP: I wrote this, which seemed natural but did not work -- I still don't fully understand why. I think this section will need some more examples / exercises to be fully digestible, or perhaps this is just yet another symptom of my imperfecdt understanding of how the numeric stuff works. void swap_array (int *p, int n, int i, int j) - /*@ requires take a1 = each(i32 k; 0i32 <= k && k < n) { Owned(array_shift(p,k)) }; + /*@ requires take a1 = each(i32 k; 0i32 <= k && k < n) { RW(array_shift(p,k)) }; 0i32 <= i && i < n; 0i32 <= j && j < n; j != i; - take xi = Owned(array_shift(p,i)); - take xj = Owned(array_shift(p,j)) - ensures take a2 = each(i32 k; 0i32 <= k && k < n) { Owned(array_shift(p,k)) }; + take xi = RW(array_shift(p,i)); + take xj = RW(array_shift(p,j)) + ensures take a2 = each(i32 k; 0i32 <= k && k < n) { RW(array_shift(p,k)) }; a1[i:xj][j:xi] == a2 @*/ { - extract Owned, i; - extract Owned, j; + focus RW, i; + focus RW, j; int tmp = p[i]; p[i] = p[j]; p[j] = tmp; @@ -913,7 +899,7 @@ exercises/init_array.c --8<-- ``` -If, for the moment, we focus just on proving safe execution of `init_array`, ignoring its functional behaviour, a specification might look as above: on entry, `init_array` takes ownership of an iterated `Owned` resource -- one `Owned` resource for each index `i` of type `u32` (so necessarily greater or equal to `0`) up to `n`; on exit `init_array` returns the ownership. +If, for the moment, we focus just on proving safe execution of `init_array`, ignoring its functional behaviour, a specification might look as above: on entry, `init_array` takes ownership of an iterated `RW` resource -- one `RW` resource for each index `i` of type `u32` (so necessarily greater or equal to `0`) up to `n`; on exit `init_array` returns the ownership. To verify this, we have to supply a loop invariant that specifies all resource ownership and the necessary constraints that hold before and after each iteration of the loop. Loop invariants are specified using the keyword `inv`, followed by CN specifications using the same syntax as in function pre- and postconditions. The variables in scope for loop invariants are all in-scope C variables, as well as CN variables introduced in the function precondition. _In loop invariants, the name of a C variable refers to its current value_ (more on this shortly). @@ -937,13 +923,13 @@ The second thing we need to do, however, is less straightforward. Recall that, a TODO: BCP: This seems like a good idea! --> -The final piece needed in the verification is an `extract` statement, as used in the previous examples: to separate the individual `Owned` resource for index `j` out of the iterated `Owned` resource and make it available to the resource inference, we specify `extract Owned, j;`. +The final piece needed in the verification is an `focus` statement, as used in the previous examples: to separate the individual `RW` resource for index `j` out of the iterated `RW` resource and make it available to the resource inference, we specify `focus RW, j;`. -With the `inv` and `extract` statements in place, CN accepts the function. +With the `inv` and `focus` statements in place, CN accepts the function. ### Second loop example -The specification of `init_array` is overly strong: it requires an iterated `Owned` resource for the array on entry. If, as the name suggests, the purpose of `init_array` is to initialise the array, then a precondition asserting only an iterated `Block` resource for the array should also be sufficient. The modified specification is then as follows. +The specification of `init_array` is overly strong: it requires an iterated `RW` resource for the array on entry. If, as the name suggests, the purpose of `init_array` is to initialise the array, then a precondition asserting only an iterated `W` resource for the array should also be sufficient. The modified specification is then as follows. ```c title="exercises/init_array2.c" --8<-- @@ -951,7 +937,7 @@ exercises/init_array2.c --8<-- ``` -This specification _should_ hold: assuming ownership of an uninitialised array on entry, each iteration of the loop initialises one cell of the array, moving it from `Block` to `Owned` "`state`", so that on function return the full array is initialised. (Recall that stores only require `Block` ownership of the written memory location, i.e., ownership of not-necessarily-initialised memory.) +This specification _should_ hold: assuming ownership of an uninitialised array on entry, each iteration of the loop initialises one cell of the array, moving it from `W` to `RW` "`state`", so that on function return the full array is initialised. (Recall that stores only require `W` ownership of the written memory location, i.e., ownership of not-necessarily-initialised memory.) To verify this modified example we again need a loop Invariant. But this time the loop invariant is more involved: since each iteration of @@ -959,7 +945,7 @@ the loop initialises one more array cell, the loop invariant has to do precise book-keeping of the initialisation status of the different sections of the array. -To do this, we partition the array ownership into two parts: for each index of the array the loop has already visited, we have an `Owned` resource, for all other array indices we have the (unchanged) `Block` ownership. +To do this, we partition the array ownership into two parts: for each index of the array the loop has already visited, we have an `RW` resource, for all other array indices we have the (unchanged) `W` ownership. ```c title="solutions/init_array2.c" --8<-- @@ -969,21 +955,21 @@ solutions/init_array2.c Let's go through this line-by-line: -- We assert ownership of an iterated `Owned` resource, one for each index `i` strictly smaller than loop variable `j`. +- We assert ownership of an iterated `RW` resource, one for each index `i` strictly smaller than loop variable `j`. -- All remaining indices `i`, between `j` and `n` are still uninitialised, so part of the iterated `Block` resource. +- All remaining indices `i`, between `j` and `n` are still uninitialised, so part of the iterated `W` resource. - As in the previous example, we assert `p` and `n` are unchanged. -- Finally, unlike in the previous example, this loop invariant involves `j`. We therefore also need to know that `j` does not exceed the array length `n`. Otherwise CN would not be able to prove that, on completing the last loop iteration, `j=n` holds. This, in turn, is needed to show that, when the function returns, ownership of the iterated `Owned` resource --- as specified in the loop invariant --- is fully consumed by the function's post-condition and there is no left-over unused resource. +- Finally, unlike in the previous example, this loop invariant involves `j`. We therefore also need to know that `j` does not exceed the array length `n`. Otherwise CN would not be able to prove that, on completing the last loop iteration, `j=n` holds. This, in turn, is needed to show that, when the function returns, ownership of the iterated `RW` resource --- as specified in the loop invariant --- is fully consumed by the function's post-condition and there is no left-over unused resource. -As before, we also have to instruct CN to `extract` ownership of individual array cells out of the iterated resources: +As before, we also have to instruct CN to `focus` ownership of individual array cells out of the iterated resources: -- to allow CN to extract the individual `Block` to be written, we use `extract Block, j;`; +- to allow CN to focus the individual `W` to be written, we use `focus W, j;`; -- the store returns a matching `Owned` resource for index `j`; +- the store returns a matching `RW` resource for index `j`; -- finally, we add `extract Owned, j;` to allow CN to "`attach`" this resource to the iterated `Owned` resource. CN issues a warning, because nothing is, in fact, extracted: we are using `extract` only for the "`reverse`" direction. +- finally, we add `focus RW, j;` to allow CN to "`attach`" this resource to the iterated `RW` resource. CN issues a warning, because nothing is, in fact, focused: we are using `focus` only for the "`reverse`" direction. @@ -1049,7 +1035,7 @@ exercises/slf_incr2_alias.c This version does correctly state that the final values of `p` and `q` are,m respectively, `3` and `1` more than their original values. But the way we got there -- by duplicating the whole function `incr2`, is horrible. - + A better way is to define a _predicate_ that captures both the aliased @@ -1057,7 +1043,7 @@ and the non-aliased cases together and use it in the pre- and postconditions: - + ```c title="exercises/slf_incr2.c" @@ -1066,7 +1052,7 @@ exercises/slf_incr2.c --8<-- ``` - + @@ -1180,7 +1166,7 @@ exercises/list/c_types.h - + To write specifications for C functions that manipulate lists, we need to define a CN "predicate" that describes specification-level list @@ -1188,7 +1174,7 @@ structures, as one would do in ML, Haskell, or Coq. We use the datatype `List` for CN-level lists. Intuitively, the `SLList_At` predicate walks over a singly-linked -pointer structure in the C heap and extracts an `Owned` version of +pointer structure in the C heap and focuss an `RW` version of the CN-level list that it represents. ```c title="exercises/list/cn_types.h" @@ -2263,5 +2249,5 @@ alternative: [](https://www.sphinx-doc.org/en/master/index.html) Misc notes: -- Nb: take V = Owned(p) === p |-t-> V +- Nb: take V = RW(p) === p |-t-> V -->