The following program generates a meaningless verification error, but as a workaround it is possible to wrap the mutable reference modification in a helper method. This is a bug. The original program should verify without raising a verification errors related to an inexistent loop invariant.
Debugging details: It's because at the end of client we want to exhale the permission for the initial target of i, but the *i += 1 overwrites the field in our encoding with a new target. The _preserve variables in the encoding try to encode that the target remains constant, but it actually changes. By removing the _preserve hack Viper then complains that it doesn't have permission to exhale stuff at the end of client.
The following program generates a meaningless verification error, but as a workaround it is possible to wrap the mutable reference modification in a helper method. This is a bug. The original program should verify without raising a verification errors related to an inexistent loop invariant.
Unsupported:
Error message:
Workaround:
Workaround with contracts:
Debugging details: It's because at the end of
client
we want to exhale the permission for the initial target ofi
, but the*i += 1
overwrites the field in our encoding with a new target. The_preserve
variables in the encoding try to encode that the target remains constant, but it actually changes. By removing the_preserve
hack Viper then complains that it doesn't have permission to exhale stuff at the end ofclient
.