Function modifications are not considered for caching

[ArquintL]

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
}

[mschwerhoff]

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]

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