test.pvl

class test {

    ensures \result == 0;
    int test1() {
        return 0;
    }

}