diff options
| author |  stefanheule <unknown> | 2012-10-01 15:56:09 +0200 |
|---|---|---|
| committer | stefanheule <unknown> | 2012-10-01 15:56:09 +0200 |
| commit | 1834b06f39ee460a36831bf5047fe77d9edff3db (patch) | |
| tree | abc03423a7cdeebc86ba4c8cb341b83829955c63 | |
| parent | 247a9f10e453d7ab84fd77422ccce1a021d4fc54 (diff) | |
Chalice: Let the trigger for the function postcondition axiom be more permissive.
| -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 e57c861e..60163a1a 100644 --- a/Chalice/src/main/scala/Translator.scala +++ b/Chalice/src/main/scala/Translator.scala @@ -389,7 +389,7 @@ class Translator { val inArgs = (f.ins map {i => Boogie.VarExpr(i.UniqueName)});
val myresult = Boogie.BVar("result", f.out.typ);
val args = VarExpr("this") :: inArgs;
- val applyF = FunctionApp(functionName(f), List(VarExpr(HeapName)) ::: args)
+ val applyFLimited = FunctionApp(functionName(f)+"#limited", List(VarExpr(HeapName)) ::: args)
val canCall = FunctionApp(functionName(f) + "#canCall", args)
val wellformed = wf(VarExpr(HeapName), VarExpr(MaskName), VarExpr(SecMaskName))
@@ -397,7 +397,7 @@ class Translator { (Postconditions(f.spec) map { post : Expression =>
Axiom(new Boogie.Forall(
BVar(HeapName, theap) :: BVar(MaskName, tmask) :: BVar(SecMaskName, tmask) :: BVar("this", tref) :: (f.ins map Variable2BVar),
- new Trigger(List(applyF, wellformed)),
+ new Trigger(List(applyFLimited, wellformed)),
(wellformed && (CanAssumeFunctionDefs || f.height < FunctionContextHeight || canCall))
==>
etran.Tr(SubstResult(post, f.apply(ExplicitThisExpr(), f.ins map { arg => new VariableExpr(arg) })))
|