diff options
| author |  kyessenov <unknown> | 2010-08-06 02:31:12 +0000 |
|---|---|---|
| committer | kyessenov <unknown> | 2010-08-06 02:31:12 +0000 |
| commit | 019634609db25a4c56abd0eae49da20a1957e258 (patch) | |
| tree | 9fd2c8d940bd7ac648efdb390fd68a40fe79f2e4 /Chalice/src | |
| parent | e1e7e6d9556256217d123f5ecc4904a1abebf958 (diff) | |
Chalice: still cannot verify refinement of List.get (Z3 goes out of memory); added classic sqrt refinement; assertions on acc(s[*].f) have now positions attached
Diffstat (limited to 'Chalice/src')
| -rw-r--r-- | Chalice/src/Translator.scala | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Chalice/src/Translator.scala b/Chalice/src/Translator.scala index d627e44d..1bb8849c 100644 --- a/Chalice/src/Translator.scala +++ b/Chalice/src/Translator.scala @@ -1745,7 +1745,7 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E (perm match {
case _: Read => mr ==@ 0 ==> n <= mn
case _: Write => r <= mr && (r ==@ mr ==> 0 <= mn)
- })).forall(refV), error.pos, error.message + " Insufficient permissions") ::
+ })).forall(refV), error.pos, error.message + " Insufficient permissions at " + acc.pos + " for " + member.f.FullName) ::
(em := Lambda(List(aV), List(refV, fV),
(SeqContains(e, ref) && f ==@ memberName).thenElse(
Lambda(List(), List(pcV), (pc ==@ "perm$R").thenElse(mr - r, mn - n)),
|