Chalice: add pre-conditions to specification statements; semantically spec statement is just like a call statement now

1 files changed, 2 insertions, 1 deletions

diff --git a/Chalice/src/Resolver.scala b/Chalice/src/Resolver.scala
index c1740c61..360146f5 100644
--- a/Chalice/src/Resolver.scala
+++ b/Chalice/src/Resolver.scala
@@ -277,7 +277,8 @@ object Resolver {
            if (v.v != null && !s.locals.contains(v.v) && v.v.IsImmutable)

              context.Error(s.pos, "Immutable variable cannot be updated by a spec statement: " + v.id);           

          }

-         ResolveExpr(s.expr, ctx, true, true)(false)

+         ResolveExpr(s.pre, ctx, false, true)(false)

+         ResolveExpr(s.post, ctx, true, true)(false)

        case s =>

          ResolveStmt(s, ctx)

      }