search

alegnani / pancake-verifier

2 stars 0 forks source link

Heap access with expression #30

Closed JunmingZhao42 closed 1 month ago

JunmingZhao42 commented 1 month ago

It seems that the current notion of heap[x]) doesn't accept x as an expression. For example:

fun access_ptr(1 ptr) {
    /*@ requires acc(heap[ptr/@biw]) @*/
    /*@ ensures acc(heap[ptr/@biw]) @*/

    st @base + ptr, 1337;
    return 0;
}

has transpiled result with requires acc and ensures acc.