viperproject / viperproject/silver
Function modifications are not considered for caching
Open
@ArquintL is already working on this.
Since Dec 17, 2021.
critical
- Dominant language
- Scala
- Stars
- 100
- Forks
- 53
- Avg merge
- 8h 10m
- Merged PRs (30d)
- 2
Description
Verifying the following 2 versions of a file with ViperServer results both times in a successful verification even though the second one should fail (discovered by @tdardinier):
field f: Int
function g(x: Ref): Bool
ensures false
method main(x: Ref)
{
assert false
}
field f: Int
function g(x: Ref): Bool
// ensures false
method main(x: Ref)
{
assert false
}
Contributor guide
No contributing guide indexed for this repository
First steps
- Read the whole issue, then the project's contributing guide.
- Comment on the issue to say you are picking it up — it saves two people doing the same work.
- Fork the repository and make your change on a branch.
- Open a pull request that references the issue number.
Assessment
This issue has not been assessed yet.