Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Function modifications are not considered for caching #548

Open
ArquintL opened this issue Dec 17, 2021 · 2 comments · May be fixed by #549
Open

Function modifications are not considered for caching #548

ArquintL opened this issue Dec 17, 2021 · 2 comments · May be fixed by #549
Assignees
@ArquintL
Labels
critical

Comments

@ArquintL
Copy link
Member

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
}
@ArquintL ArquintL self-assigned this Dec 17, 2021
@mschwerhoff
Copy link
Contributor

Do we have a separate issue tracker for IDE/ViperServer issues? People who stumble across this issue and don't know the architecture of Viper well might assume that the unsoundness affects the heart of Viper.

@ArquintL
Copy link
Member Author

I've created the issue here as the dependency analysis is part of the silver codebase. You are however totally right that the dependency analysis is not used when simply verifying a Viper file e.g. via command line

@ArquintL ArquintL linked a pull request Dec 17, 2021 that will close this issue
Open
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@ArquintL ArquintL

Labels
critical
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Adds functions as a dependency to methods viperproject/silver
2 participants
@mschwerhoff @ArquintL