Disjointness cannot be proven between existing set of references and newly created objects

[viper-admin]

Created by @aterga on 2018-03-01 16:08

The problem seems to be related to triggering. The QP body doesn't get triggered when new an object is created via new expressions:

field next:Ref
method test_new_node(g:Set[Ref])
    requires forall n:Ref :: {n.next} n in g ==> acc(n.next)
{
    var new_node:Ref 
    new_node := new(next)
    new_node.next := null
    assert !( new_node in g ) // fails in Carbon, verifies in Silicon
}

However:

field next:Ref
method test_new_node(g:Set[Ref])
    requires forall n:Ref :: {n.next} n in g ==> acc(n.next)
{
    var new_node:Ref 
    inhale acc(new_node.next)
    new_node.next := null
    assert !( new_node in g ) // verifies
}

Related:

• https://github.com/viperproject/carbon/issues/126
• https://github.com/viperproject/carbon/issues/132
• https://github.com/viperproject/carbon/issues/174
• https://github.com/viperproject/carbon/issues/220