add error message when trying to use pverifier syntax for other backends

p-org · Nov 28, 2024 · c26fc9b · c26fc9b
1 parent c12d6a7
commit c26fc9b
Showing 1 changed file with 34 additions and 0 deletions.
diff --git a/Src/PCompiler/CompilerCore/Compiler.cs b/Src/PCompiler/CompilerCore/Compiler.cs
@@ -121,6 +121,40 @@ private static PParser.ProgramContext Parse(ICompilerConfiguration job, FileInfo
             var fileStream = new AntlrInputStream(fileText);
             var lexer = new PLexer(fileStream);
             var tokens = new CommonTokenStream(lexer);
+
+            if (!job.OutputLanguages.Contains(CompilerOutput.Uclid5))
+            {
+                // disallow any pverifier tokens
+                tokens.Fill();
+                foreach (var token in tokens.GetTokens())
+                {
+                    switch (token.Type)
+                    {
+                        case PParser.INVARIANT:
+                        case PParser.AXIOM:
+                        case PParser.IS:
+                        case PParser.FLYING:
+                        case PParser.TARGETS:
+                        case PParser.SENT:
+                        case PParser.PROOF:
+                        case PParser.PROVE:
+                        case PParser.USING:
+                        case PParser.LEMMA:
+                        case PParser.THEOREM:
+                        case PParser.EXCEPT:
+                        case PParser.REQUIRES:
+                        case PParser.ENSURES:
+                        case PParser.FORALL:
+                        case PParser.EXISTS:
+                        case PParser.INIT:
+                            throw new NotSupportedException(
+                                $"line {token.Line}:{token.Column} \"{token.Text}\" only supported by PVerifier backend.");
+                    }
+                }
+
+                tokens.Reset();
+            }
+
             var parser = new PParser(tokens);
             parser.RemoveErrorListeners();