[Silver Permission Inference] no inference for accesses in tests

[viper-admin]

Created by bitbucket user caterinaurban on 2016-07-04 21:20 Last updated on 2016-07-06 20:10

The inference does not seem to track accesses that appear in boolean conditions. See for instance the following program:

#!Scala
field f: Int

method Foo(r: Ref)
{
    var i: Int := 2
    while (i < r.f)
    {
        i := i + 1
    }
}

[viper-admin]

@dohrau on 2016-07-04 21:28:

• changed the assignee from (none) to @dohrau

[viper-admin]

@dohrau commented on 2016-07-05 08:27

Bug does not seem to be in the permission analysis state. The assume method is called with a UnitExpression as an argument. Maybe the bug is in the backward interpreter.

[viper-admin]

@dohrau on 2016-07-05 08:27:

• changed the assignee from @dohrau to bitbucket user caterinaurban

[viper-admin]

Bitbucket user caterinaurban commented on 2016-07-06 20:10

fixed https://github.com/viperproject/sample/issues/58

→ <<cset https://github.com/viperproject/sample/commit/f9c7406baf0201c635f29332bee830221df70649>>

[viper-admin]

Bitbucket user caterinaurban on 2016-07-06 20:10:

• changed state from new to resolved