Skip to content

Update deprecated keywords #122

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
wants to merge 2 commits into
base: main
Choose a base branch
from
Open

Update deprecated keywords #122

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
a7ad231
Update deprecated keywords
dc-mak Mar 12, 2025
22375b4
Update deprecated keywords in tutorial
dc-mak Mar 12, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
8 changes: 4 additions & 4 deletions src/example-archive/Rust/broken/error-proof/00004-simple-lifetimes.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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?
Expand All @@ -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<int>(input);
ensures take v2 = Block<int>(input);
/*@ requires take v1 = W<int>(input);
ensures take v2 = W<int>(input);
return == input;
@*/
{
Expand Down
4 changes: 2 additions & 2 deletions src/example-archive/Rust/broken/error-proof/00006-lifetimes-broken.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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<int>(input);
ensures take v2 = Owned<int>(input);
/*@ requires take v1 = RW<int>(input);
ensures take v2 = RW<int>(input);
return == input;
@*/
{
Expand Down
30 changes: 15 additions & 15 deletions src/example-archive/SAW/broken/error-cerberus/00001.swap.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -140,10 +140,10 @@ llvm_verify swapmod "wacky_sort"
#include <stdio.h>

void swap(uint32_t *x, uint32_t *y)
/*@ requires take xv0 = Owned<uint32_t>(x);
take yv0 = Owned<uint32_t>(y);
ensures take xv1 = Owned<uint32_t>(x);
take yv1 = Owned<uint32_t>(y);
/*@ requires take xv0 = RW<uint32_t>(x);
take yv0 = RW<uint32_t>(y);
ensures take xv1 = RW<uint32_t>(x);
take yv1 = RW<uint32_t>(y);
xv1 == yv0;
yv1 == xv0;
@*/
Expand All @@ -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<uint32_t>(x);
take yv0 = Owned<uint32_t>(y);
ensures take xv1 = Owned<uint32_t>(x);
take yv1 = Owned<uint32_t>(y);
/*@ requires take xv0 = RW<uint32_t>(x);
take yv0 = RW<uint32_t>(y);
ensures take xv1 = RW<uint32_t>(x);
take yv1 = RW<uint32_t>(y);
xv1 == yv0;
yv1 == xv0;
@*/
Expand All @@ -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<int>(array_shift<int>(a,j)) };
ensures take av1 = each(size_t j; 0u64 <= j && j < len) { Owned<int>(array_shift<int>(a,j)) };
/*@ requires take av0 = each(size_t j; 0u64 <= j && j < len) { RW<int>(array_shift<int>(a,j)) };
ensures take av1 = each(size_t j; 0u64 <= j && j < len) { RW<int>(array_shift<int>(a,j)) };
@*/
{
for (size_t i = 0; i < len - 1; ++i)
/*@ inv take avl = each(u64 k; 0u64 <= k && k < i) { Owned<int>(array_shift<int>(a,k)) };
take avr = each(u64 k; i <= k && k < len) { Owned<int>(array_shift<int>(a,k)) } ;
/*@ inv take avl = each(u64 k; 0u64 <= k && k < i) { RW<int>(array_shift<int>(a,k)) };
take avr = each(u64 k; i <= k && k < len) { RW<int>(array_shift<int>(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<int>(array_shift<int>(a,k)) };
take avr = each(u64 k; i <= k && k < j) { Owned<int>(array_shift<int>(a,k)) };
take avr = each(u64 k; j <= k && k < len) { Owned<int>(array_shift<int>(a,k)) };
/*@ inv take avl = each(u64 k; 0u64 <= k && k < i) { RW<int>(array_shift<int>(a,k)) };
take avr = each(u64 k; i <= k && k < j) { RW<int>(array_shift<int>(a,k)) };
take avr = each(u64 k; j <= k && k < len) { RW<int>(array_shift<int>(a,k)) };
{a} unchanged; {len} unchanged;
j <= len;
@*/
Expand Down
32 changes: 16 additions & 16 deletions src/example-archive/SAW/broken/error-proof/00003.point.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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<struct point>(p1);
take vp20 = Owned<struct point>(p2);
ensures take vp11 = Owned<struct point>(p1);
take vp21 = Owned<struct point>(p2);
/*@ requires take vp10 = RW<struct point>(p1);
take vp20 = RW<struct point>(p2);
ensures take vp11 = RW<struct point>(p1);
take vp21 = RW<struct point>(p2);
vp10 == vp11 ; vp20 == vp21;
if (vp11.x == vp21.x && vp11.y == vp21.x) {
return == 1u8
Expand All @@ -118,13 +118,13 @@ bool point_eq(const point *p1, const point *p2)

/*@ spec malloc();
requires true;
ensures take v = Block<struct point>(return);
ensures take v = W<struct point>(return);
@*/

// Allocate and return a new point
point* point_new(uint32_t x, uint32_t y)
/*@ requires true;
ensures take vp1 = Owned<struct point>(return);
ensures take vp1 = RW<struct point>(return);
vp1.x == x ; vp1.y == y;
@*/
{
Expand All @@ -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<struct point>(p);
ensures take vp1 = Owned<struct point>(p);
take vr1 = Owned<struct point>(return);
/*@ requires take vp0 = RW<struct point>(p);
ensures take vp1 = RW<struct point>(p);
take vr1 = RW<struct point>(return);
vp0.x == vp1.x ; vp0.y == vp1.y;
vr1.x == vp1.x ; vr1.y == vp1.y;
@*/
Expand All @@ -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<struct point>(p1);
take vp20 = Owned<struct point>(p2);
take vZ0 = Owned<struct point>(&ZERO);
/*@ requires take vp10 = RW<struct point>(p1);
take vp20 = RW<struct point>(p2);
take vZ0 = RW<struct point>(&ZERO);
vZ0.x == 0u32 ; vZ0.y == 0u32;
ensures take vp11 = Owned<struct point>(p1);
take vp21 = Owned<struct point>(p2);
take vZ1 = Owned<struct point>(&ZERO);
take vr1 = Owned<struct point>(return);
ensures take vp11 = RW<struct point>(p1);
take vp21 = RW<struct point>(p2);
take vZ1 = RW<struct point>(&ZERO);
take vr1 = RW<struct point>(return);
vr1.x == vp11.x + vp21.x ; vr1.y == vp11.y + vp21.y;
@*/
{
Expand Down
14 changes: 7 additions & 7 deletions src/example-archive/SAW/broken/error-proof/00004.tutorial-dotprod.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -48,25 +48,25 @@ function [rec] (u32) dotprod_spec(map<u32, u32> x,map<u32, u32> 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<uint32_t>(array_shift<uint32_t>(x,j)) };
take ay0 = each(u32 j; 0u32 <= j && j < size) { Owned<uint32_t>(array_shift<uint32_t>(y,j)) }
ensures take ax1 = each(u32 j; 0u32 <= j && j < size) { Owned<uint32_t>(array_shift<uint32_t>(x,j)) };
take ay1 = each(u32 j; 0u32 <= j && j < size) { Owned<uint32_t>(array_shift<uint32_t>(y,j)) };
/*@ requires take ax0 = each(u32 j; 0u32 <= j && j < size) { RW<uint32_t>(array_shift<uint32_t>(x,j)) };
take ay0 = each(u32 j; 0u32 <= j && j < size) { RW<uint32_t>(array_shift<uint32_t>(y,j)) }
ensures take ax1 = each(u32 j; 0u32 <= j && j < size) { RW<uint32_t>(array_shift<uint32_t>(x,j)) };
take ay1 = each(u32 j; 0u32 <= j && j < size) { RW<uint32_t>(array_shift<uint32_t>(y,j)) };
return == dotprod_spec(ax1,ay1,size)
@*/
{
uint32_t res = 0;
/*@ 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<uint32_t>(array_shift<uint32_t>(x,j)) };
take ayi = each(u32 j; 0u32 <= j && j < size) { Owned<uint32_t>(array_shift<uint32_t>(y,j)) };
/*@ inv take axi = each(u32 j; 0u32 <= j && j < size) { RW<uint32_t>(array_shift<uint32_t>(x,j)) };
take ayi = each(u32 j; 0u32 <= j && j < size) { RW<uint32_t>(array_shift<uint32_t>(y,j)) };
{x} unchanged; {y} unchanged;
0u64<=i;
res == dotprod_spec(axi,ayi,(u32)i)
@*/
{
/*@ extract Owned<uint32_t>, i; @*/
/*@ focus RW<uint32_t>, i; @*/
res += x[i] * y[i];
/*@ unfold dotprod_spec(axi,ayi,(u32)i); @*/
}
Expand Down
6 changes: 3 additions & 3 deletions src/example-archive/c-testsuite/broken/error-proof/00077.err1.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,12 +3,12 @@
int
foo(int x[100])
/*@ requires
take PreX = each (u64 j; 0u64 <= j && j < 100u64) {Owned<int>(x + j)}; @*/
take PreX = each (u64 j; 0u64 <= j && j < 100u64) {RW<int>(x + j)}; @*/
{
int y[100];
int *p;

/*@ extract Block<int>, 0u64; @*/
/*@ focus W<int>, 0u64; @*/
y[0] = 2000;

if(x[0] != 1000)
Expand Down Expand Up @@ -49,7 +49,7 @@ main()
{
int x[100];
assert(0);
/*@ extract Block<int>, 0u64; @*/
/*@ focus W<int>, 0u64; @*/
x[0] = 1000;

return foo(x);
Expand Down
2 changes: 1 addition & 1 deletion src/example-archive/c-testsuite/broken/error-timeout/00182.timeout.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 */

Expand Down
4 changes: 2 additions & 2 deletions src/example-archive/c-testsuite/working/00015.working.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,9 +4,9 @@ main()
{
int arr[2];

/*@ extract Block<int>, 0u64; @*/
/*@ focus W<int>, 0u64; @*/
arr[0] = 1;
/*@ extract Block<int>, 1u64; @*/
/*@ focus W<int>, 1u64; @*/
arr[1] = 2;

return arr[0] + arr[1] - 3;
Expand Down
2 changes: 1 addition & 1 deletion src/example-archive/c-testsuite/working/00016.working.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@ main()
int arr[2];
int *p;

/*@ extract Block<int>, 1u64; @*/
/*@ focus W<int>, 1u64; @*/
p = &arr[1];
*p = 0;
return arr[1];
Expand Down
4 changes: 2 additions & 2 deletions src/example-archive/c-testsuite/working/00032.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,9 +7,9 @@ main()
int arr[2];
int *p;

/*@ extract Block<int>, 0u64; @*/
/*@ focus W<int>, 0u64; @*/
arr[0] = 2;
/*@ extract Block<int>, 1u64; @*/
/*@ focus W<int>, 1u64; @*/
arr[1] = 3;
p = &arr[0];
if(*(p++) != 2)
Expand Down
8 changes: 4 additions & 4 deletions src/example-archive/c-testsuite/working/00033.working.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,9 +3,9 @@ int g;
int
effect()
/*@ requires
take Pre = Owned<int>(&g); @*/
take Pre = RW<int>(&g); @*/
/*@ ensures
take Post = Owned<int>(&g);
take Post = RW<int>(&g);
Post == 1i32;
return == 1i32; @*/
{
Expand All @@ -16,9 +16,9 @@ effect()
int
main()
/*@ requires
take Pre = Owned<int>(&g); @*/
take Pre = RW<int>(&g); @*/
/*@ ensures
take Post = Owned<int>(&g); @*/
take Post = RW<int>(&g); @*/
/*@ ensures return == 0i32; @*/
{
int x;
Expand Down
2 changes: 1 addition & 1 deletion src/example-archive/c-testsuite/working/00037.working.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@ main()
{
int x[2];
int *p;
/*@ extract Block<int>, 1u64; @*/
/*@ focus W<int>, 1u64; @*/
x[1] = 7;
p = &x[0];
p = p + 1;
Expand Down
2 changes: 1 addition & 1 deletion src/example-archive/c-testsuite/working/00072.working.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@ main()
{
int arr[2];
int *p;
/*@ extract Block<int>, 1u64; @*/
/*@ focus W<int>, 1u64; @*/
p = &arr[0];
p += 1;
*p = 123;
Expand Down
4 changes: 2 additions & 2 deletions src/example-archive/c-testsuite/working/00078.working.c
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,9 +1,9 @@
int
f1(char *p)
/*@ requires
take PreP = Owned<char>(p); @*/
take PreP = RW<char>(p); @*/
/*@ ensures
take PostP = Owned<char>(p);
take PostP = RW<char>(p);
return == 1i32 + (i32) PreP; @*/
{
return *p+1;
Expand Down
6 changes: 3 additions & 3 deletions src/example-archive/c-testsuite/working/00090.working.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -12,9 +12,9 @@ main()
@*/
/*@ ensures return == 0i32; @*/
{
/*@ extract Owned<int>, 0u64; @*/
/*@ extract Owned<int>, 1u64; @*/
/*@ extract Owned<int>, 2u64; @*/
/*@ focus RW<int>, 0u64; @*/
/*@ focus RW<int>, 1u64; @*/
/*@ focus RW<int>, 2u64; @*/
if (a[0] != 0)
return 1;
if (a[1] != 1)
Expand Down
8 changes: 4 additions & 4 deletions src/example-archive/dafny-tutorial/working/binary_search.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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<int>(a + j)}; @*/
{RW<int>(a + j)}; @*/
/*@ ensures
take IndexPost = each (i32 j; 0i32 <= j && j < length)
{Owned<int>(a + j)};
{RW<int>(a + j)};
IndexPost == IndexPre;
(return < 0i32) || (IndexPost[return] == value); @*/
{
Expand All @@ -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<int>(a + j)};
{RW<int>(a + j)};
IndexInv == IndexPre; @*/
{
int mid = (low + high) / 2;
/*@ extract Owned<int>, mid; @*/
/*@ focus RW<int>, mid; @*/
/*@ instantiate good<int>, mid; @*/
if (a[mid] < value)
{
Expand Down
8 changes: 4 additions & 4 deletions src/example-archive/dafny-tutorial/working/linear_search.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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<int>(a + j)}; @*/
{RW<int>(a + j)}; @*/
/*@ ensures
take IndexPost = each (i32 j; 0i32 <= j && j < length)
{Owned<int>(a + j)};
{RW<int>(a + j)};
(return < 0i32) || (IndexPost[return] == key);
each (i32 j; 0i32 <= j && j < length)
{return >= 0i32 || IndexPre[j] != key};
Expand All @@ -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<int>(a + j)};
{RW<int>(a + j)};
IndexInv == IndexPre;
each (i32 j; 0i32 <= j && j < idx) {IndexPre[j] != key}; @*/
{
/*@ extract Owned<int>, idx; @*/
/*@ focus RW<int>, idx; @*/
if (*(a + idx) == key)
{
return idx;
Expand Down
4 changes: 2 additions & 2 deletions src/example-archive/dafny-tutorial/working/multiple_returns.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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<struct int_pair>(ret);
take PairPre = RW<struct int_pair>(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<struct int_pair>(ret);
take PairPost = RW<struct int_pair>(ret);
PairPost.fst == x + y;
PairPost.snd == x - y; @*/
{
Expand Down
Loading
Loading