diff options
| author |  mueller <unknown> | 2010-12-16 16:25:08 +0000 |
|---|---|---|
| committer | mueller <unknown> | 2010-12-16 16:25:08 +0000 |
| commit | 063f42fc32048568db11fc24cbbe5a81f03f429f (patch) | |
| tree | 80b6059d49b12c72e9e6a802144592589445a11e /Chalice | |
| parent | 8c68d648346f8aa1719f0f12161a36fbd7993454 (diff) | |
Chalice: this fixes a bug (an unsoundness) that arose in when a program combined predicates, read permissions to predicates, and forks.
Diffstat (limited to 'Chalice')
| -rw-r--r-- | Chalice/src/Translator.scala | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/Chalice/src/Translator.scala b/Chalice/src/Translator.scala index 3b6955b1..69f82b1f 100644 --- a/Chalice/src/Translator.scala +++ b/Chalice/src/Translator.scala @@ -682,7 +682,10 @@ class Translator { // create a new token
BLocal(tokenV) :: Havoc(tokenId) :: bassume(nonNull(tokenId)) ::
// the following assumes help in proving that the token is fresh
- bassume(etran.Heap.select(tokenId, "joinable") ==@ 0) ::
+ // the first statement used to be an assume, but this caused an unsoundness in combination with the storing of a heap snapshot
+ // in the location of a predicate. The assume constrained both the current heap and the snapshot, whereas the assignment
+ // changes only the current heap (which is then different from a previously stored snapshot.
+ etran.Heap.store(tokenId, "joinable", 0) ::
bassume(new Boogie.MapSelect(etran.Mask, tokenId, "joinable", "perm$N")==@ 0) ::
bassume(new Boogie.MapSelect(etran.Mask, tokenId, "joinable", "perm$R")==@ 0) ::
etran.IncPermission(tokenId, "joinable", 100) ::
|