fixed old issue

Author: shazqadeer

Source/Core/AST/Absy.cs

@@ -2721,8 +2721,7 @@ void TypecheckSpec(List<int> layers, Action<TypecheckingContext> f)
       {
         var oldGlobalAccessOnlyInOld = tc.GlobalAccessOnlyInOld;
         if (this is YieldProcedureDecl yieldProcedureDecl &&
-            yieldProcedureDecl.HasMoverType &&
-            layers.Any(layer => layer < yieldProcedureDecl.Layer))
+            (!yieldProcedureDecl.HasMoverType || layers.Any(layer => layer < yieldProcedureDecl.Layer)))
         {
           tc.GlobalAccessOnlyInOld = true;
         }
@@ -3317,12 +3316,13 @@ public override void Typecheck(TypecheckingContext tc)
 
       var oldProc = tc.Proc;
       tc.Proc = this;
-      tc.GlobalAccessOnlyInOld = !HasMoverType;
       base.Typecheck(tc);
-      tc.GlobalAccessOnlyInOld = false;
+      Debug.Assert(!tc.GlobalAccessOnlyInOld);
       YieldRequires.ForEach(callCmd => callCmd.Typecheck(tc));
-      YieldEnsures.ForEach(callCmd => callCmd.Typecheck(tc));
+      tc.GlobalAccessOnlyInOld = true;
       YieldPreserves.ForEach(callCmd => callCmd.Typecheck(tc));
+      YieldEnsures.ForEach(callCmd => callCmd.Typecheck(tc));
+      tc.GlobalAccessOnlyInOld = false;
       Contract.Assert(tc.Proc == this);
       tc.Proc = oldProc;
     }

Source/Core/AST/Commands/CallCmd.cs

@@ -590,19 +590,21 @@ public override void Typecheck(TypecheckingContext tc)
     }
 
     // typecheck in-parameters
+    var oldGlobalAccessOnlyInOld = tc.GlobalAccessOnlyInOld;
+    tc.GlobalAccessOnlyInOld = oldGlobalAccessOnlyInOld || tc.Proc is YieldProcedureDecl && Proc is YieldProcedureDecl;
     for (int i = 0; i < Ins.Count; i++)
     {
       var e = Ins[i];
       if (e != null)
       {
-        tc.GlobalAccessOnlyInOld = tc.Proc is YieldProcedureDecl && Proc is YieldProcedureDecl;
         tc.ExpectedLayerRange = expectedLayerRanges?[i];
         e.Typecheck(tc);
-        tc.GlobalAccessOnlyInOld = false;
         tc.ExpectedLayerRange = null;
       }
     }
+    tc.GlobalAccessOnlyInOld = oldGlobalAccessOnlyInOld;
 
+    // typecheck out-parameters
     for (int i = 0; i < Outs.Count; i++)
     {
       var e = Outs[i];

Test/civl/regression-tests/yield-pre-post-mover.bpl.expect

@@ -5,6 +5,6 @@ yield-pre-post-mover.bpl(15,23): Error: global variable must be accessed inside
 yield-pre-post-mover.bpl(13,19): Error: global variable must be accessed inside old expression: g
 yield-pre-post-mover.bpl(16,21): Error: global variable must be accessed inside old expression: g
 yield-pre-post-mover.bpl(23,9): Error: layer of callee must be less than layer of caller
-yield-pre-post-mover.bpl(24,8): Error: layer of callee must be less than layer of caller
 yield-pre-post-mover.bpl(25,10): Error: layer of callee must be less than layer of caller
+yield-pre-post-mover.bpl(24,8): Error: layer of callee must be less than layer of caller
 9 type checking errors detected in yield-pre-post-mover.bpl

Test/civl/regression-tests/yield-requires-ensures-errors-2.bpl

@@ -8,7 +8,7 @@ preserves x >= n;
 
 yield procedure {:layer 1} p0(n: int)
 requires call yield_x(n == 4);
-ensures call yield_x(n == 8);
 preserves call yield_x(n == 2);
+ensures call yield_x(n == 8);
 {
 }

Test/civl/regression-tests/yield-requires-ensures-errors-2.bpl.expect

@@ -1,4 +1,4 @@
 yield-requires-ensures-errors-2.bpl(10,24): Error: invalid type for argument 0 in call to yield_x: bool (expected: int)
-yield-requires-ensures-errors-2.bpl(11,23): Error: invalid type for argument 0 in call to yield_x: bool (expected: int)
-yield-requires-ensures-errors-2.bpl(12,25): Error: invalid type for argument 0 in call to yield_x: bool (expected: int)
+yield-requires-ensures-errors-2.bpl(11,25): Error: invalid type for argument 0 in call to yield_x: bool (expected: int)
+yield-requires-ensures-errors-2.bpl(12,23): Error: invalid type for argument 0 in call to yield_x: bool (expected: int)
 3 type checking errors detected in yield-requires-ensures-errors-2.bpl

Test/civl/regression-tests/yield-requires-ensures-errors-5.bpl.expect

@@ -1,4 +1,4 @@
 yield-requires-ensures-errors-5.bpl(10,9): Error: layer of callee must be less than layer of caller
-yield-requires-ensures-errors-5.bpl(12,8): Error: layer of callee must be less than layer of caller
 yield-requires-ensures-errors-5.bpl(11,10): Error: layer of callee must be less than layer of caller
+yield-requires-ensures-errors-5.bpl(12,8): Error: layer of callee must be less than layer of caller
 3 type checking errors detected in yield-requires-ensures-errors-5.bpl