Crash report: Missing: Quantified resource aloc(optGet1(boxes), i).ref.value might not be injective.

[sakehl]

This is from the current tutorial

Crash Message

Missing: Quantified resource aloc(optGet1(boxes), i).ref.value might not be injective.
  at viper.api.backend.SilverBackend.getFailure(SilverBackend.scala:398)
  at viper.api.backend.SilverBackend.getFailure$(SilverBackend.scala:385)
  at viper.api.backend.silicon.Silicon.getFailure(Silicon.scala:34)
  at viper.api.backend.SilverBackend.processError(SilverBackend.scala:200)
  at viper.api.backend.SilverBackend.processError$(SilverBackend.scala:173)
  at viper.api.backend.silicon.Silicon.processError(Silicon.scala:34)
  at viper.api.backend.SilverBackend.$anonfun$submit$1(SilverBackend.scala:165)
  at viper.api.backend.SilverBackend.$anonfun$submit$1$adapted(SilverBackend.scala:165)
  at scala.collection.immutable.List.foreach(List.scala:333)
  at viper.api.backend.SilverBackend.submit(SilverBackend.scala:165)
  at viper.api.backend.SilverBackend.submit$(SilverBackend.scala:144)
  at viper.api.backend.silicon.Silicon.submit(Silicon.scala:34)
  ...
  at vct.main.Main$.main(Main.scala:51)
  at vct.main.Main.main(Main.scala)

Version Information

• VerCors version 9999.9.9-SNAPSHOT
• At commit 54d8cfd from branch AddSMTSolver (changes=true)

Arguments

arrays-and-pointers-injectivity-object-arrays-and-efficient-verification-2.pvl

File Inputs

arrays-and-pointers-injectivity-object-arrays-and-efficient-verification-2.pvl

//:: cases arrays-and-pointers-injectivity-object-arrays-and-efficient-verification-2
//:: verdict Fail
//:: tools silicon
class Box {
    int value;

    requires a != null ** (\forall* int i; 0 <= i && i < a.length; Perm(a[i], read));
    requires (\forall* int i; 0 <= i && i < a.length; a[i] != null ** Perm(a[i].value, write));
    void test(Box[] a) {
        
    }

    void foo() {
        Box box = new Box();
        Box[] boxes = new Box[2];

[sakehl]

(Same error on commit: 4d4937c from branch dev)

[superaxander]

That's interesting, when you exclude the call you get the the expected error about the contract. But when calling it the contract is evaluated again, and this leads to the error appearing again but this time we are looking for errors that fit within PreconditionFailed and this is not one of them.

I guess the best solution would be to duplicate the cases from defer in getFailure (from the SilverBackend class where defer just deals with any ErrorReason and getFailure deals with errors that yield ContractFailures) and have a new "NotWellDefined" VerificationFailure class which adapts another VerificationFailure so that you can use it inside something that requires a ContractFailure.