Created by bitbucket user ykass on 2014-06-12 15:02
Last updated on 2014-06-16 07:35
Note the assertions marked by //lemma in the attached files linkedlist.chalice and lseg.chalice. It seems that these lemmas are needed by Silicon to verify these files (translated by Chalice2Silver).
The problem seems to be that after folding a predicate instance for the first time, the functions that depend on it will get computed only if there is an assertion about their value that triggers this computation. If one of these lemmas is omitted, then the corresponding postcondition is not verified.
Note that lseg does not fully verify: the loop invariant in line 62 fails to verify. I conjecture that the same bug is behind this, but I could not find appropriate lemmas to make the verification go through.
Attachments:
Note the assertions marked by //lemma in the attached files linkedlist.chalice and lseg.chalice. It seems that these lemmas are needed by Silicon to verify these files (translated by Chalice2Silver).
The problem seems to be that after folding a predicate instance for the first time, the functions that depend on it will get computed only if there is an assertion about their value that triggers this computation. If one of these lemmas is omitted, then the corresponding postcondition is not verified.
Note that lseg does not fully verify: the loop invariant in line 62 fails to verify. I conjecture that the same bug is behind this, but I could not find appropriate lemmas to make the verification go through.
Attachments:
lseg.chalicelinkedlist.chalice