search

alegnani / pancake-verifier

1 stars 0 forks source link

Operator for multiple access annotations #37

Closed alegnani closed 6 days ago

alegnani commented 1 week ago

Add slice access operator s.t. an annotation as follows:

    /*@ requires acc(heap[1]) @*/
    /*@ requires acc(heap[2]) @*/
    /*@ requires acc(heap[3]) @*/
    /*@ requires acc(heap[7]) @*/
    /*@ requires acc(heap[8]) @*/
    /*@ requires acc(heap[9]) @*/
    /*@ requires acc(heap[10]) @*/

can be expressed as:

/*@ requires acc(heap[1..=3]) @*/
/*@ requires acc(heap[7..=10]) @*/

The inclusive range acc(heap[l..=h]) will be syntactic sugar for forall x: Int :: l <= x && x <= h ==> acc(heap[x]). The exlusive range acc(heap[l..h]) will be syntactic sugar for forall x: Int :: l <= x && x < h ==> acc(heap[x]).