Roughly implement opaque (rest of files)

viperproject · Jan 30, 2024 · f790863 · f790863
1 parent 3c5177c
commit f790863
Show file tree

Hide file tree

Showing 11 changed files with 3,246 additions and 3,130 deletions.
diff --git a/src/main/antlr4/GobraLexer.g4 b/src/main/antlr4/GobraLexer.g4
@@ -89,3 +89,5 @@ PROOF       : 'proof';
 GHOST_EQUALS     : '===';
 GHOST_NOT_EQUALS : '!==';
 WITH        : 'with';
+OPAQUE      : 'opaque';
+REVEAL      : 'reveal';
diff --git a/src/main/antlr4/GobraParser.g4 b/src/main/antlr4/GobraParser.g4
@@ -161,8 +161,8 @@ sqType: (kind=(SEQ | SET | MSET | OPT) L_BRACKET type_ R_BRACKET)
 
 // Specifications
 
-specification returns[boolean trusted = false, boolean pure = false;]:
-  ((specStatement | PURE {$pure = true;} | TRUSTED {$trusted = true;}) eos)*? (PURE {$pure = true;})? // Non-greedily match PURE to avoid missing eos errors.
+specification returns[boolean trusted = false, boolean pure = false, boolean opaque = false;]:
+  ((specStatement | OPAQUE {$opaque = true;} | PURE {$pure = true;} | TRUSTED {$trusted = true;}) eos)*? (PURE {$pure = true;})? // Non-greedily match PURE to avoid missing eos errors.
   ;
 
 specStatement
@@ -226,11 +226,11 @@ new_: NEW L_PAREN type_ R_PAREN;
 
 // Added specifications and parameter info
 
-specMember: specification (functionDecl[$specification.trusted, $specification.pure] | methodDecl[$specification.trusted, $specification.pure]);
+specMember: specification (functionDecl[$specification.trusted, $specification.pure, $specification.opaque] | methodDecl[$specification.trusted, $specification.pure, $specification.opaque]);
 
-functionDecl[boolean trusted, boolean pure]:  FUNC IDENTIFIER (signature blockWithBodyParameterInfo?);
+functionDecl[boolean trusted, boolean pure, boolean opaque]:  FUNC IDENTIFIER (signature blockWithBodyParameterInfo?);
 
-methodDecl[boolean trusted, boolean pure]: FUNC receiver IDENTIFIER (signature blockWithBodyParameterInfo?);
+methodDecl[boolean trusted, boolean pure, boolean opaque]: FUNC receiver IDENTIFIER (signature blockWithBodyParameterInfo?);
 
 
 
@@ -376,7 +376,9 @@ primaryExpr:
   | primaryExpr slice_ #slicePrimaryExpr
   | primaryExpr seqUpdExp #seqUpdPrimaryExpr
   | primaryExpr typeAssertion #typeAssertionPrimaryExpr
+  // REVEAL? primaryExpr arguments doesn't work due to mutual left recursion
   | primaryExpr arguments #invokePrimaryExpr
+  | REVEAL primaryExpr arguments #revealInvokePrimaryExpr
   | primaryExpr arguments AS closureSpecInstance #invokePrimaryExprWithSpec
   | primaryExpr predConstructArgs #predConstrPrimaryExpr
   | call_op=(

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