diff --git a/Source/Core/AST/Absy.cs b/Source/Core/AST/Absy.cs index 8747597ab..f169ace39 100644 --- a/Source/Core/AST/Absy.cs +++ b/Source/Core/AST/Absy.cs @@ -2974,9 +2974,13 @@ public override void Resolve(ResolutionContext rc) if (RefinedAction != null) { RefinedAction.Resolve(rc); + if (!HasMoverType) + { + MoverType = MoverType.Atomic; + } if (RefinedAction.ActionDecl is { HasMoverType: false }) { - rc.Error(this, $"refined action {RefinedAction.ActionDecl.Name} must have a mover type"); + RefinedAction.ActionDecl.MoverType = MoverType.Atomic; } } if (InvariantAction != null) @@ -3298,7 +3302,7 @@ public override void Resolve(ResolutionContext rc) RefinedAction.Resolve(rc); if (RefinedAction.ActionDecl is { HasMoverType: false }) { - rc.Error(this, $"refined action {RefinedAction.ActionDecl.Name} must have a mover type"); + RefinedAction.ActionDecl.MoverType = MoverType.Atomic; } } diff --git a/Source/Core/BoogiePL.atg b/Source/Core/BoogiePL.atg index 6f1f0c676..6d336e458 100644 --- a/Source/Core/BoogiePL.atg +++ b/Source/Core/BoogiePL.atg @@ -705,16 +705,16 @@ ActionDecl 0) + if (outs.Count > 0) { this.SemErr("async action must not have output parameters"); } else { + if (moverType == MoverType.None) + { + moverType = MoverType.Atomic; + } datatypeTypeCtorDecl = new DatatypeTypeCtorDecl(name, name.val, new List(), null); var fields = ins.Select(v => new Formal(v.tok, new TypedIdent(v.TypedIdent.tok, v.Name, v.TypedIdent.Type), true, v.Attributes)).ToList(); datatypeTypeCtorDecl.AddConstructor(name, name.val, fields); diff --git a/Source/Core/Parser.cs b/Source/Core/Parser.cs index 871576e28..09a9b05ba 100644 --- a/Source/Core/Parser.cs +++ b/Source/Core/Parser.cs @@ -725,16 +725,16 @@ void ActionDecl(bool isPure, out ActionDecl actionDecl, out Implementation impl, } } if (isAsync) { - if (moverType == MoverType.None) - { - this.SemErr("async action must have a mover type"); - } - else if (outs.Count > 0) + if (outs.Count > 0) { this.SemErr("async action must not have output parameters"); } else { + if (moverType == MoverType.None) + { + moverType = MoverType.Atomic; + } datatypeTypeCtorDecl = new DatatypeTypeCtorDecl(name, name.val, new List(), null); var fields = ins.Select(v => new Formal(v.tok, new TypedIdent(v.TypedIdent.tok, v.Name, v.TypedIdent.Type), true, v.Attributes)).ToList(); datatypeTypeCtorDecl.AddConstructor(name, name.val, fields);