diff options
| author |  stefanheule <unknown> | 2012-02-25 03:12:59 -0800 |
|---|---|---|
| committer | stefanheule <unknown> | 2012-02-25 03:12:59 -0800 |
| commit | 95a0a2ad4c055bbb91497a3128c8f86c86cf26c0 (patch) | |
| tree | b60bc4d32315c2deca6fba808b1bcff7f47589f9 | |
| parent | f26031a93283ae0842de09eef853364233ff0407 (diff) | |
Chalice: correct axiom for limited functions (use 2nd mask)
| -rw-r--r-- | Chalice/src/main/scala/Translator.scala | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Chalice/src/main/scala/Translator.scala b/Chalice/src/main/scala/Translator.scala index 5cb6e469..be672a2f 100644 --- a/Chalice/src/main/scala/Translator.scala +++ b/Chalice/src/main/scala/Translator.scala @@ -244,7 +244,7 @@ class Translator { 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) ::: args))) ::
+ applyF ==@ FunctionApp(functionName(f) + "#limited", List(etran.Heap, etran.Mask, etran.SecMask) ::: args))) ::
Nil
else
Nil)
|