improve syntax for 'openDupPkgInv'

viperproject · Sep 23, 2024 · ee1f467 · ee1f467
1 parent e92a034
commit ee1f467
Show file tree

Hide file tree

Showing 8 changed files with 3,212 additions and 3,224 deletions.
diff --git a/src/main/antlr4/GobraLexer.g4 b/src/main/antlr4/GobraLexer.g4
@@ -87,7 +87,7 @@ TRUSTED     : 'trusted' -> mode(NLSEMI);
 OUTLINE     : 'outline';
 DUPLICABLE  : 'dup';
 PKG_INV     : 'pkgInvariant';
-OPEN_DUP_SINV : 'openDupPkgInv';
+OPEN_DUP_SINV : 'openDupPkgInv' -> mode(NLSEMI);
 INIT_POST   : 'initEnsures';
 IMPORT_PRE  : 'importRequires';
 PROOF       : 'proof';

diff --git a/src/main/antlr4/GobraParser.g4 b/src/main/antlr4/GobraParser.g4
@@ -63,7 +63,7 @@ ghostStatement:
   | fold_stmt=(FOLD | UNFOLD) predicateAccess #foldStatement
   | kind=(ASSUME | ASSERT | REFUTE | INHALE | EXHALE) expression #proofStatement
   | matchStmt #matchStmt_
-  | OPEN_DUP_SINV (IDENTIFIER) #pkgInvStatement
+  | OPEN_DUP_SINV #pkgInvStatement
   ;
 
 // Auxiliary statements

diff --git a/src/main/java/viper/gobra/frontend/GobraLexer.java b/src/main/java/viper/gobra/frontend/GobraLexer.java