Unsoundness with field-access trigger

Issue #326 resolved
Tierry Hörmann created an issue

The following simple program verifies

field val: Int

function foo(): Bool
    ensures forall n:Ref :: { n.val } true

method test(x: Ref)
    assert false

However when using a different trigger in foo() as follows, everything is fine again:

field val: Int

function foo(): Int
    ensures forall n:Ref :: { dummy(n) } true

function dummy(n:Ref): Bool

method test(x: Ref)
    assert false

Comments (7)

  1. Malte Schwerhoff

    Thanks for filing this issue! Silicon can currently only handle field deferences as triggers if the field is used in combination with quantified permissions, see also issue #294. This isn't the case here and the function should therefore be rejected by Silicon's consistency checker.

  2. Malte Schwerhoff

    Could it be that you're using a (very) old version of Silicon? I just tried your example that uses n.val as a trigger and I get the following Silicon error message:

    Silicon finished in 1.875 seconds.
    The following errors were found:
      An internal error occurred. n.val is not supported. Silicon only supports field accesses as triggers if (1) permissions to the field come from quantified permissions, and if (2) the field access also occurs in the body of the quantification. n.val is not such a field access.

    Please update your version of Silicon and try again.

  3. Tierry Hörmann reporter

    Indeed, when running the example with building the current version myself, it outputs the same error. However using VSCode with updated dependencies, it still verifies. So maybe the VSCode plugin downloads old binaries?

  4. Alexander J. Summers

    Could you double-check that you have the "Viper Experimental" and not the "Viper" plugin installed please, Tierry?

  5. Malte Schwerhoff

    I just reinstalled the VSCode plugin and the bundled Viper tools and I also don't get the expected error message. @arshavir Any idea why the VSCode plugin might not show the error?

  6. Log in to comment