Decreases leads to error with nested quantified permission
sakehl opened this issue · 1 comments
sakehl commented
The dummy program below, based on how VerCors encodes pointers, does not verify with the latest silicon version. It also does not give a proper line failure:
Silicon 1.1-SNAPSHOT (c891a153)
Silicon found 1 error in 2.88s:
[0] Conditional statement might fail. There might be insufficient permission to access ptr_deref(ptr_add(inp, i)).ref (<no position>)
However, when commenting out the decreases
, it does verify, so there seems to be an error there.
domain block {
function block_length(b: block): Int
function loc(b: block, i: Int): Ref
function loc_inv_1(r: Ref): block
function loc_inv_2(r: Ref): Int
axiom {
(forall b: block ::block_length(b) >= 0)
}
axiom {
(forall b: block, i: Int ::
{ loc(b, i) }
loc_inv_1(loc(b, i)) == b && loc_inv_2(loc(b, i)) == i)
}
}
domain pointer {
function pointer_of(b: block, offset: Int): pointer
function pointer_block(p: pointer): block
function pointer_offset(p: pointer): Int
axiom {
(forall p: pointer ::pointer_offset(p) >= 0 &&
pointer_offset(p) < block_length(pointer_block(p)))
}
axiom {
(forall b: block, offset: Int ::
{ pointer_block(pointer_of(b, offset)), pointer_offset(pointer_of(b, offset)) }
pointer_block(pointer_of(b, offset)) == b &&
pointer_offset(pointer_of(b, offset)) == offset)
}
}
function ptr_deref(p: pointer): Ref
decreases
{
loc(pointer_block(p), pointer_offset(p))
}
function ptr_add(p: pointer, offset: Int): pointer
requires 0 <= pointer_offset(p) + offset
requires pointer_offset(p) + offset < block_length(pointer_block(p))
decreases
{
pointer_of(pointer_block(p), pointer_offset(p) + offset)
}
field ref: Ref
field x: Int
function inp_to_seq_2(inp: pointer, n: Int): Seq[Int]
requires n <=
block_length(pointer_block(inp)) -
pointer_offset(inp)
requires (forall i: Int ::
{ ptr_deref(ptr_add(inp, i)).ref }
0 <= i && i < n ==>
acc(ptr_deref(ptr_add(inp, i)).ref, 1 *
write /
10))
requires (forall i: Int, j: Int ::0 <= i &&
i < n &&
0 <= j &&
j < n ==>
i != j ==>
ptr_deref(ptr_add((inp), i)).ref !=
ptr_deref(ptr_add((inp), j)).ref)
requires (forall i: Int ::
{ ptr_deref(ptr_add(inp, i)).ref.x }
0 <= i && i < n ==>
acc(ptr_deref(ptr_add(inp, i)).ref.x, 1 *
write /
10))
decreases
{
Seq[Int]()
}
marcoeilers commented
Fixed in viperproject/silver#754.