diff options
| author |  stefanheule <unknown> | 2012-02-25 03:21:56 -0800 |
|---|---|---|
| committer | stefanheule <unknown> | 2012-02-25 03:21:56 -0800 |
| commit | b782048b795635c9461c3b442ff336a33f6a9eb3 (patch) | |
| tree | 3cb0427a075493d3575e21b563d9d047bf6a72e2 /Chalice/src | |
| parent | dc8a86355f0d00e20ab13a5e2dcef0966b91d63f (diff) | |
Chalice: use canread instead of canreadforsure in function axiom
Diffstat (limited to 'Chalice/src')
| -rw-r--r-- | Chalice/src/main/scala/Translator.scala | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/Chalice/src/main/scala/Translator.scala b/Chalice/src/main/scala/Translator.scala index be641169..bfc85662 100644 --- a/Chalice/src/main/scala/Translator.scala +++ b/Chalice/src/main/scala/Translator.scala @@ -1827,12 +1827,12 @@ class ExpressionTranslator(val globals: Globals, preGlobals: Globals, val fpi: F TrAll(tmp)
case acc@Access(e,perm) =>
val memberName = if(e.isPredicate) e.predicate.FullName else e.f.FullName;
- CanReadForSure(Tr(e.e), memberName)
+ CanRead(Tr(e.e), memberName)
case acc @ AccessSeq(s, Some(member), perm) =>
if (member.isPredicate) throw new NotSupportedException("not yet implemented");
val memberName = member.f.FullName;
val (refV, ref) = Boogie.NewBVar("ref", tref, true);
- (SeqContains(Tr(s), ref) ==> CanReadForSure(ref, memberName)).forall(refV)
+ (SeqContains(Tr(s), ref) ==> CanRead(ref, memberName)).forall(refV)
case _ => etran.Tr(e, TrAllHelper)
}
TrAllHelper(e, this)
|