Open akiarie opened 2 months ago
Fixing the pointer now, and making the array of unknown size, we get a different challenge:
zerofifth(int *arr) { arr[5] = 0; }
We could modify our understanding of the .clump to make it a permissive restriction:
.clump
zerofifth(int *arr) ~ [ setup: arr = .clump(sizeof(int)) - 5; /* arr+5 is valid address */ arr[5] = 0; /* assign to *(arr+5) */ ];
The meaning would be that an argument x of zerofifth must satisfy that x+5 points at a block of the size sizeof(int).
x
zerofifth
x+5
sizeof(int)
It also seems it would work for more advanced cases:
zerofifthseventh(int *arr) ~ [ setup: arr = .clump(sizeof(int)*3) - 5; arr[5] = 0; arr[7] = 0; ]{ arr[5] = 0; arr[7] = 0; } zeromany(int *arr) ~ [ int i; setup: arr = .clump(sizeof(int)*10) - 3; for (i = 3; i < 13; i++) { arr[i] = 0; } ]{ int i; for (i = 3; i < 13; i++) { arr[i] = 0; } }
Fixing the pointer now, and making the array of unknown size, we get a different challenge:
We could modify our understanding of the
.clump
to make it a permissive restriction:The meaning would be that an argument
x
ofzerofifth
must satisfy thatx+5
points at a block of the sizesizeof(int)
.It also seems it would work for more advanced cases: