diff options
| author |  stefanheule <unknown> | 2012-02-25 03:22:02 -0800 |
|---|---|---|
| committer | stefanheule <unknown> | 2012-02-25 03:22:02 -0800 |
| commit | e663d52194a17a63fa1e97a727e2aad1dd0acf0d (patch) | |
| tree | 939b1c7d462bc77d79f1eac4c8ae33fdb37df388 /Chalice/src/main | |
| parent | b782048b795635c9461c3b442ff336a33f6a9eb3 (diff) | |
Chalice: Add trigger to 'limited axiom' instead of the definining axiom.
Diffstat (limited to 'Chalice/src/main')
| -rw-r--r-- | Chalice/src/main/scala/Translator.scala | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/Chalice/src/main/scala/Translator.scala b/Chalice/src/main/scala/Translator.scala index bfc85662..84a2efe8 100644 --- a/Chalice/src/main/scala/Translator.scala +++ b/Chalice/src/main/scala/Translator.scala @@ -238,16 +238,16 @@ class Translator { wf(h, m, sm) && CurrentModule == module#C ==> #C.f(h, m, this, x_1, ..., x_n) == tr(body))
*/
Axiom(new Boogie.Forall(Nil,
- formals, List(new Trigger(applyF),new Trigger(trigger)),
- (trigger) && (wf(VarExpr(HeapName), VarExpr(MaskName), VarExpr(SecMaskName)) && (CurrentModule ==@ ModuleName(currentClass)) && etran.TrAll(pre))
+ formals, List(new Trigger(applyF)),
+ (wf(VarExpr(HeapName), VarExpr(MaskName), VarExpr(SecMaskName)) && (CurrentModule ==@ ModuleName(currentClass)) && etran.TrAll(pre))
==>
(applyF ==@ body))) ::
(if (f.isRecursive)
// define the limited function (even for unlimited function since its SCC might have limited functions)
Boogie.Function(functionName(f) + "#limited", formals, BVar("$myresult", f.out.typ)) ::
- Axiom(new Boogie.Forall(
- formals, new Trigger(applyF),
- applyF ==@ FunctionApp(functionName(f) + "#limited", List(etran.Heap, etran.Mask, etran.SecMask) ::: args))) ::
+ Axiom(new Boogie.Forall(Nil,
+ formals, List(new Trigger(applyF), new Trigger(trigger)),
+ (trigger) && (applyF ==@ FunctionApp(functionName(f) + "#limited", List(etran.Heap, etran.Mask, etran.SecMask) ::: args)))) ::
Nil
else
Nil) :::
|