Fix issue #1005

Source/Concurrency/YieldingProcDuplicator.cs

@@ -297,15 +297,7 @@ private void ProcessCallCmd(CallCmd newCall)
           }
           else if (IsRefinementLayer)
           {
-            if (newCall.HasAttribute(CivlAttributes.SKIP))
-            {
-              var calleeRefinedAction = PrepareNewCall(newCall, yieldingProc);
-              InjectGate(calleeRefinedAction, newCall);
-            }
-            else
-            {
-              AddPendingAsync(newCall, yieldingProc);
-            }
+            AddPendingAsync(newCall, yieldingProc);
           }
         }
         else

Source/Core/AST/Commands/CallCmd.cs

@@ -301,7 +301,6 @@ void CheckModifies(IEnumerable<Variable> modifiedVars)
     if (Proc is YieldProcedureDecl calleeDecl)
     {
       var isSynchronized = this.HasAttribute(CivlAttributes.SYNC);
-      var isSkipped = this.HasAttribute(CivlAttributes.SKIP);
       if (calleeDecl.Layer > callerDecl.Layer)
       {
         tc.Error(this, "layer of callee must not be more than layer of caller");
@@ -320,12 +319,12 @@ void CheckModifies(IEnumerable<Variable> modifiedVars)
             else
             {
               CheckModifies(highestRefinedActionDecl.ModifiedVars);
+              if (callerDecl.HasMoverType && highestRefinedActionDecl.Creates.Any())
+              {
+                tc.Error(this, "caller must not be a mover procedure");
+              }
               if (!IsAsync)
               {
-                if (highestRefinedActionDecl.Creates.Any() && callerDecl.HasMoverType)
-                {
-                  tc.Error(this, "caller must not be a mover procedure");
-                }
                 // check there is no application of IS_RIGHT in the entire chain of refined actions
                 var calleeRefinedAction = calleeDecl.RefinedAction;
                 while (calleeRefinedAction != null)
@@ -363,16 +362,9 @@ void CheckModifies(IEnumerable<Variable> modifiedVars)
                   calleeRefinedAction = calleeActionDecl.RefinedAction;
                 }
               }
-              else if (isSkipped)
+              else if (callerDecl.HasMoverType)
               {
-                if (highestRefinedActionDecl.LayerRange.UpperLayer != callerDecl.Layer)
-                {
-                  tc.Error(this, $"upper layer of action {highestRefinedActionDecl.Name} must be same as layer of caller");
-                }
-                else if (!highestRefinedActionDecl.IsSkippable())
-                {
-                  tc.Error(this, $"action {highestRefinedActionDecl.Name} must be skippable");
-                }
+                tc.Error(this, "async call must be synchronized");
               }
             }
           }

Source/Core/CivlAttributes.cs

@@ -86,7 +86,6 @@ public static class CivlAttributes
     public const string HIDE = "hide";
     public const string PENDING_ASYNC = "pending_async";
     public const string SYNC = "sync";
-    public const string SKIP = "skip";
     public const string IS_RIGHT = "IS_right";
     public const string IS_LEFT = "IS_left";
 

Test/civl/regression-tests/issue-1005.bpl

@@ -0,0 +1,15 @@
+// RUN: %parallel-boogie "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+left action {:layer 1, 100} voting_action ()
+{
+}
+
+yield procedure {:layer 0} voting_procedure ();
+refines voting_action;
+
+
+yield left procedure {:layer 100} voting_loop_yield_procedure()
+{
+    async call voting_procedure();
+}

Test/civl/regression-tests/issue-1005.bpl.expect

@@ -0,0 +1,2 @@
+issue-1005.bpl(14,10): Error: async call must be synchronized
+1 type checking errors detected in issue-1005.bpl