Finding predicates with arguments in the heap

[viper-admin]

Created by @mschwerhoff on 2013-07-25 10:23 Last updated on 2017-09-23 13:47

As illustrated by the test file Sil:all/predicates/arguments.sil, Silicon isn't able to verify snippets such as

inhale acc(this.valid(b), write)
inhale acc(this.valid(!b), write)
exhale acc(this.valid(true), write)

It is obvious that the prover needs to be invoked when looking for a matching heap chunk. It is not obvious, however, how to proceed. Since b and !b are both may- but not must-matches, one could i) just pick the first may-match and ignore other possibilities or ii) branch and try all possibilities.

[viper-admin]

@alexanderjsummers on 2013-09-10 22:36:

• edited the description

[viper-admin]

@alexanderjsummers commented on 2013-09-10 22:38

This seems conceptually related to the incompleteness we discussed recently:

inhale acc(y.f)&&acc(z.f)&& (x==y || x==z); exhale acc(x.f)

will not succeed.

[viper-admin]

@mueller55 on 2014-09-22 13:54:

• changed the assignee from (none) to @mschwerhoff

[viper-admin]

@mueller55 on 2015-02-19 15:57:

• changed priority from major to minor
• changed the assignee from @mschwerhoff to (none)

[viper-admin]

@mschwerhoff commented on 2017-09-23 13:44

The non-greedy consume algorithm implemented as part of robinsierra's bachelor's thesis solves this problem. For now, this algorithm is not used by default, it must be chosen explicitly by running Silicon with the command-line option --enableMoreCompleteExhale.

[viper-admin]

@mschwerhoff commented on 2017-09-23 13:47

See also https://github.com/viperproject/silicon/issues/72, https://github.com/viperproject/silicon/issues/232