search

viperproject / sample

Other
0 stars 0 forks source link

[SIL Specification Inference] Inferred postcondition of list/prepend.sil does not contain permissions #39

Open viper-admin opened 10 years ago

viper-admin commented 10 years ago

Created by bitbucket user severinh on 2014-04-06 10:13 Last updated on 2016-07-04 20:42

The field assignment newList.next := this adds the predicate instance specifying this as a nested predicate instance to the predicate specifying newList.

At the end of the method, the analysis decides (see folding heuristics) not to fold the predicate instance for newList, because then the method would lose the nested predicate instance for list (even though it does not contain any permissions at all).

Thus, because folding did not happen, the analysis conservatively does not extract any permissions for newList.

viper-admin commented 10 years ago

@mueller55 on 2014-10-13 15:22:

  • changed the assignee from (none) to bitbucket user mnovacek
viper-admin commented 8 years ago

Bitbucket user caterinaurban on 2016-07-04 20:42:

  • changed state from new to on hold