From c26fc9b9e8328623fe54c9d61566d0b50661f6cd Mon Sep 17 00:00:00 2001 From: FedericoAureliano Date: Thu, 28 Nov 2024 11:05:25 -0800 Subject: [PATCH] add error message when trying to use pverifier syntax for other backends --- Src/PCompiler/CompilerCore/Compiler.cs | 34 ++++++++++++++++++++++++++ 1 file changed, 34 insertions(+) diff --git a/Src/PCompiler/CompilerCore/Compiler.cs b/Src/PCompiler/CompilerCore/Compiler.cs index dd30a3041..1e73305b9 100644 --- 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();