allow names for actions in refines clause

boogie-org · Nov 20, 2024 · 3b68356 · 3b68356
1 parent b709fa4
commit 3b68356
Show file tree

Hide file tree

Showing 5 changed files with 7 additions and 20 deletions.
diff --git a/Source/Core/BoogiePL.atg b/Source/Core/BoogiePL.atg
@@ -769,10 +769,9 @@ SpecRefinedActionForYieldProcedure<.ref ActionDeclRef refinedAction, IToken name
     Ident<out m>
     ImplBody<out locals, out stmtList>
     (.
-      if (m.val != "_") {
-        this.SemErr("expected _ for name of anoonymous action");
-      } else if (refinedAction == null) {
-        var actionDecl = new ActionDecl(tok, null, moverType, Formal.StripWhereClauses(ins), Formal.StripWhereClauses(outs),
+      if (refinedAction == null) {
+        var actionName = m.val == "_" ? null : m.val;
+        var actionDecl = new ActionDecl(tok, actionName, moverType, Formal.StripWhereClauses(ins), Formal.StripWhereClauses(outs),
                                       false, new List<ActionDeclRef>(), null, null,
                                       new List<Requires>(), new List<CallCmd>(), new List<AssertCmd>(), new List<IdentifierExpr>(), null, akv);
         Pgm.AddTopLevelDeclaration(actionDecl);

diff --git a/Source/Core/Parser.cs b/Source/Core/Parser.cs
@@ -1235,10 +1235,9 @@ void SpecRefinedActionForYieldProcedure(ref ActionDeclRef refinedAction, IToken
 			}
 			Ident(out m);
 			ImplBody(out locals, out stmtList);
-			if (m.val != "_") {
-			 this.SemErr("expected _ for name of anoonymous action");
-			} else if (refinedAction == null) {
-			 var actionDecl = new ActionDecl(tok, null, moverType, Formal.StripWhereClauses(ins), Formal.StripWhereClauses(outs),
+			if (refinedAction == null) {
+			 var actionName = m.val == "_" ? null : m.val;
+			 var actionDecl = new ActionDecl(tok, actionName, moverType, Formal.StripWhereClauses(ins), Formal.StripWhereClauses(outs),
 			                               false, new List<ActionDeclRef>(), null, null,
 			                               new List<Requires>(), new List<CallCmd>(), new List<AssertCmd>(), new List<IdentifierExpr>(), null, akv);
 			 Pgm.AddTopLevelDeclaration(actionDecl);

diff --git a/Test/civl/regression-tests/anonymous-action-fail.bpl b/Test/civl/regression-tests/anonymous-action-fail.bpl
diff --git a/Test/civl/regression-tests/anonymous-action-fail.bpl.expect b/Test/civl/regression-tests/anonymous-action-fail.bpl.expect
diff --git a/Test/civl/regression-tests/anonymous-action.bpl b/Test/civl/regression-tests/anonymous-action.bpl
@@ -17,7 +17,7 @@ refines both action {:layer 2} _ {
 }
 
 yield procedure {:layer 0} C(i: int) returns (j: int);
-refines both action {:layer 1} _ {
+refines both action {:layer 1} AC {
     call Incr();
 }