diff options
| author |  stefanheule <unknown> | 2012-02-25 03:20:13 -0800 |
|---|---|---|
| committer | stefanheule <unknown> | 2012-02-25 03:20:13 -0800 |
| commit | 285d324e05f2252cab216747a732038020d947ef (patch) | |
| tree | 9479ed26730a060370bdbfb098d9d1f9096713fd /Chalice/src | |
| parent | ef49594d0d30ef46e75a02b5a11e29315ab04db9 (diff) | |
Chalice: the secondary mask was not saved using CallSecMask at a fork
Diffstat (limited to 'Chalice/src')
| -rw-r--r-- | Chalice/src/main/scala/Translator.scala | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/Chalice/src/main/scala/Translator.scala b/Chalice/src/main/scala/Translator.scala index aaf091d8..fd7d90ac 100644 --- a/Chalice/src/main/scala/Translator.scala +++ b/Chalice/src/main/scala/Translator.scala @@ -705,6 +705,7 @@ class Translator { val (asyncStateV,asyncState) = NewBVar("asyncstate", tint, true)
val (preCallHeapV, preCallHeap) = NewBVar("preCallHeap", theap, true)
val (preCallMaskV, preCallMask) = NewBVar("preCallMask", tmask, true)
+ val (preCallSecMaskV, preCallSecMask) = NewBVar("preCallSecMask", tmask, true)
val (preCallCreditsV, preCallCredits) = NewBVar("preCallCredits", tcredits, true)
val (argsSeqV, argsSeq) = NewBVar("argsSeq", tArgSeq, true)
val argsSeqLength = 1 + args.length;
@@ -722,6 +723,7 @@ class Translator { // remember the value of the heap/mask/credits
BLocal(preCallHeapV) :: (preCallHeap := etran.Heap) ::
BLocal(preCallMaskV) :: (preCallMask := etran.Mask) ::
+ BLocal(preCallSecMaskV) :: (preCallSecMask := etran.SecMask) ::
BLocal(preCallCreditsV) :: (preCallCredits := etran.Credits) ::
BLocal(argsSeqV) ::
// introduce formal parameters and pre-state globals
@@ -756,6 +758,7 @@ class Translator { // assume the pre call state for the token is the state before inhaling the precondition
bassume(CallHeap(asyncState) ==@ preCallHeap) ::
bassume(CallMask(asyncState) ==@ preCallMask) ::
+ bassume(CallSecMask(asyncState) ==@ preCallSecMask) ::
bassume(CallCredits(asyncState) ==@ preCallCredits) ::
bassume(CallArgs(asyncState) ==@ argsSeq) :::
// assign the returned token to the variable
|