Heap-dependent triggers are not as restrictive as expected

[viper-admin]

Created by @mschwerhoff on 2015-12-18 08:48
Last updated on 2019-03-08 13:56

The following example verifies in Silicon, which is sound (the assertion is actually true), but somewhat unexpected, since the heap-dependent trigger of the inhaled quantifier should prevent the quantifier from being instantiated.

#!text

function fun01(x: Ref, i: Int): Bool
  requires acc(x.f)

function bar01(i: Int): Int

method test01a(x: Ref) {
  inhale acc(x.f)

  inhale forall i: Int :: {fun01(x, i)} bar01(i) > 0

  exhale acc(x.f)
  inhale acc(x.f)

  inhale fun01(x, 5)
  assert bar01(5) > 0 // Is true, but should not be provable
}

The reason seems to be that heap snapshots are encoded as Z3 datatypes, as illustrated in this Stackoverflow post.

See also regression test all/functions/heap_dependent_triggers.sil.

[viper-admin]

@mschwerhoff on 2015-12-18 08:50:

• edited the description

[viper-admin]

@mschwerhoff commented on 2019-03-08 13:56

Potentially related: #371