summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Chalice/examples/Answer16
-rw-r--r--Chalice/src/Resolver.scala2
-rw-r--r--Chalice/src/Translator.scala11
-rw-r--r--Util/Emacs/dafny-mode.el2
4 files changed, 11 insertions, 20 deletions
diff --git a/Chalice/examples/Answer b/Chalice/examples/Answer
index d9856d2d..e8ca406d 100644
--- a/Chalice/examples/Answer
+++ b/Chalice/examples/Answer
@@ -6,10 +6,10 @@ Boogie program verifier finished with 31 verified, 1 error
------ Running regression test counter.chalice
69.5: Monitor invariant might hot hold. The expression at 4.27 might not evaluate to true.
80.5: Assertion might not hold. The expression at 80.12 might not evaluate to true.
- 119.5: The held field of the target of the release statement might not be writable.
+ 119.5: The target of the release statement might be not be locked by the current thread.
128.7: The mu field of the target of the acquire statement might not be above waitlevel.
136.7: The mu field of the target of the acquire statement might not be above waitlevel.
- 145.5: The held field of the target of the release statement might not be writable.
+ 145.5: The target of the release statement might be not be locked by the current thread.
Boogie program verifier finished with 24 verified, 6 errors
------ Running regression test dining-philosophers.chalice
@@ -181,8 +181,8 @@ The program did not typecheck.
33.14: Location might not be readable.
42.5: Monitor invariant might hot hold. The expression at 5.23 might not evaluate to true.
60.5: Location might not be writable
- 76.5: The held field of the target of the unshare statement might not be writable.
- 84.5: The held field of the target of the unshare statement might not be writable.
+ 76.5: The target of the unshare statement might not be shared.
+ 84.5: The target of the unshare statement might not be shared.
Boogie program verifier finished with 16 verified, 7 errors
------ Running regression test prog2.chalice
@@ -201,10 +201,12 @@ Boogie program verifier finished with 24 verified, 4 errors
Boogie program verifier finished with 51 verified, 4 errors
------ Running regression test prog4.chalice
5.5: Assertion might not hold. The expression at 5.12 might not evaluate to true.
- 15.7: The held field of the target of the release statement might not be writable.
- 27.7: The held field of the target of the release statement might not be writable.
+ 15.7: The target of the release statement might be not be locked by the current thread.
+ 15.7: Release might fail because the current thread might hold the read lock.
+ 27.7: The target of the release statement might be not be locked by the current thread.
+ 27.7: Release might fail because the current thread might hold the read lock.
-Boogie program verifier finished with 6 verified, 3 errors
+Boogie program verifier finished with 6 verified, 5 errors
------ Running regression test ImplicitLocals.chalice
Boogie program verifier finished with 8 verified, 0 errors
diff --git a/Chalice/src/Resolver.scala b/Chalice/src/Resolver.scala
index 4ce95b3e..14bd7d1c 100644
--- a/Chalice/src/Resolver.scala
+++ b/Chalice/src/Resolver.scala
@@ -671,7 +671,7 @@ object Resolver {
if(inPredicate) context.Error(expr.pos, "holds cannot be mentioned in monitor invariants or predicates")
if(! specContext)
context.Error(expr.pos, "holds is allowed only in positive predicate contexts");
- //todo: check that we are not in an invariant
+ //todo: check that we are not in a monitor invariant
ResolveExpr(e, context, twoStateContext, false)
expr.typ = BoolClass
case expr@ RdHolds(e) =>
diff --git a/Chalice/src/Translator.scala b/Chalice/src/Translator.scala
index 644d203c..10eafb6a 100644
--- a/Chalice/src/Translator.scala
+++ b/Chalice/src/Translator.scala
@@ -392,8 +392,6 @@ class Translator {
bassert(nonNull(obj), s.pos, "The target of the share statement might be null.") ::
UpdateMu(obj, true, false, lowerBounds, upperBounds, ErrorMessage(s.pos, "Share might fail.")) :::
bassume(!isHeld(obj) && ! isRdHeld(obj)) :: // follows from o.mu==lockbottom
- // no permission to o.held
- etran.SetNoPermission(etran.Tr(obj), "held", etran.Mask) ::
// exhale the monitor invariant (using the current state as the old state)
ExhaleInvariants(obj, false, ErrorMessage(s.pos, "Monitor invariant might not hold."), etran.UseCurrentAsOld()) :::
// assume a seen state is the one right before the share
@@ -407,15 +405,12 @@ class Translator {
isDefined(obj) :::
bassert(nonNull(o), s.pos, "The target of the unshare statement might be null.") ::
bassert(CanWrite(o, "mu"), s.pos, "The mu field of the target of the unshare statement might not be writable.") ::
- bassert(CanWrite(o, "held"), s.pos, "The held field of the target of the unshare statement might not be writable.") ::
bassert(isShared(o), s.pos, "The target of the unshare statement might not be shared.") ::
bassert(isHeld(o), s.pos, "The target of the unshare statement might not be locked by the current thread.") :: // locked or read-locked
etran.Heap.store(o, "mu", bLockBottom) ::
// havoc o.held where 0<=o.held
BLocal(heldV) :: Boogie.Havoc(held) :: bassume(held <= 0) ::
etran.Heap.store(o, "held", held) ::
- // set the permission of o.held to 0
- etran.SetNoPermission(o, "held", etran.Mask) ::
// set o.rdheld to false
etran.Heap.store(o, "rdheld", false)
case Acquire(obj) =>
@@ -729,7 +724,6 @@ class Translator {
bassume(! isHeld(o) && ! isRdHeld(o)) :: // this assume follows from the previous assert
// update the thread's locking state
BLocal(lastAcquireVar) :: Havoc(lastAcquire) :: bassume(0 < lastAcquire) ::
- etran.SetFullPermission(o, "held") ::
etran.Heap.store(o, "held", lastAcquire) ::
InhaleInvariants(nonNullObj, false, etran.WhereOldIs(
LastSeenHeap(lastSeenMu, lastSeenHeld),
@@ -750,7 +744,6 @@ class Translator {
BLocal(preReleaseHeapV) :: (preReleaseHeap := etran.Heap) ::
BLocal(preReleaseMaskV) :: (preReleaseMask := etran.Mask) ::
BLocal(preReleaseCreditsV) :: (preReleaseCredits := etran.Credits) ::
- bassert(CanWrite(o, "held"), s.pos, "The held field of the target of the release statement might not be writable.") ::
bassert(isHeld(o), s.pos, "The target of the release statement might be not be locked by the current thread.") ::
bassert(!isRdHeld(o), s.pos, "Release might fail because the current thread might hold the read lock.") ::
ExhaleInvariants(nonNullObj, false, ErrorMessage(s.pos, "Monitor invariant might hot hold."), etran.WhereOldIs(
@@ -760,7 +753,6 @@ class Translator {
// havoc o.held where 0<=o.held
BLocal(heldV) :: Havoc(held) :: bassume(held <= 0) ::
etran.Heap.store(o, "held", held) ::
- etran.SetNoPermission(o, "held", etran.Mask) ::
// assume a seen state is the one right before the share
bassume(LastSeenHeap(etran.Heap.select(o, "mu"), held) ==@ preReleaseHeap) ::
bassume(LastSeenMask(etran.Heap.select(o, "mu"), held) ==@ preReleaseMask) ::
@@ -1563,7 +1555,6 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E
isDefined(e)(true) :::
bassert(nonNull(trE), holds.pos, "The target of the holds predicate might be null.")
else Nil) :::
- IncPermission(trE, "held", 100) :::
bassume(IsGoodMask(Mask)) ::
bassume(IsGoodState(Boogie.MapSelect(ih, trE, "held"))) ::
bassume(wf(Heap, Mask)) ::
@@ -1709,10 +1700,8 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E
case holds@Holds(e) =>
(if(check) isDefined(e)(true) :::
bassert(nonNull(Tr(e)), error.pos, error.message + " The target of the holds predicate at " + holds.pos + " might be null.") :: Nil else Nil) :::
- bassert(HasFullPermission(Tr(e), "held", em), error.pos, error.message + " The current thread might not have full permission to the held field at " + holds.pos + ".") ::
bassert(0 < Boogie.MapSelect(Heap, Tr(e), "held"), error.pos, error.message + " The current thread might not hold lock at " + holds.pos + ".") ::
bassert(! Boogie.MapSelect(Heap, Tr(e), "rdheld"), error.pos, error.message + " The current thread might hold the read lock at " + holds.pos + ".") ::
- SetNoPermission(Tr(e), "held", em) ::
bassume(IsGoodMask(Mask)) ::
bassume(wf(Heap, Mask)) ::
bassume(wf(Heap, em))
diff --git a/Util/Emacs/dafny-mode.el b/Util/Emacs/dafny-mode.el
index 75561d65..2f5fc467 100644
--- a/Util/Emacs/dafny-mode.el
+++ b/Util/Emacs/dafny-mode.el
@@ -30,7 +30,7 @@
]\\)*" . font-lock-comment-face)
`(,(dafny-regexp-opt '(
- "class" "datatype" "function" "frame" "ghost" "var" "method" "unlimited"
+ "class" "datatype" "function" "ghost" "var" "method" "unlimited"
"module" "imports" "static" "refines" "replaces" "by"
"returns" "requires" "ensures" "modifies" "reads" "free"
"invariant" "decreases"
generated by cgit v1.2.3 (git 2.39.1) at 2025-01-02 00:41:51 +0000