rename uclid5 backend to pverifier

p-org · Dec 5, 2024 · d01c547 · d01c547
1 parent 446859b
commit d01c547
Show file tree

Hide file tree

Showing 6 changed files with 13 additions and 13 deletions.
diff --git a/...Core/Backend/Uclid5/CompilationContext.cs → ...e/Backend/PVerifier/CompilationContext.cs b/...Core/Backend/Uclid5/CompilationContext.cs → ...e/Backend/PVerifier/CompilationContext.cs
@@ -1,4 +1,4 @@
-namespace Plang.Compiler.Backend.Uclid5;
+namespace Plang.Compiler.Backend.PVerifier;
 
 internal class CompilationContext : CompilationContextBase
 {

diff --git a/...ore/Backend/Uclid5/Uclid5CodeGenerator.cs → .../Backend/PVerifier/Uclid5CodeGenerator.cs b/...ore/Backend/Uclid5/Uclid5CodeGenerator.cs → .../Backend/PVerifier/Uclid5CodeGenerator.cs
@@ -15,15 +15,15 @@
 using Plang.Compiler.TypeChecker.AST.States;
 using Plang.Compiler.TypeChecker.Types;
 
-namespace Plang.Compiler.Backend.Uclid5;
+namespace Plang.Compiler.Backend.PVerifier;
 
-public class UclidCache
+public class PVerifierCache
 {
     public string Reply { get; set; }
     public byte[] Checksum { get; set; }
 }
 
-public class Uclid5CodeGenerator : ICodeGenerator
+public class PVerifierCodeGenerator : ICodeGenerator
 {
     private CompilationContext _ctx;
     private CompiledFile _src;
@@ -53,7 +53,7 @@ public void Compile(ICompilerConfiguration job)
         var db = new LiteDatabase(Path.Join(job.OutputDirectory.FullName, ".verifier-cache.db"));
         var md5 = MD5.Create();
         // Get a collection (or create, if doesn't exist)
-        var qCollection = db.GetCollection<UclidCache>("qCollection");
+        var qCollection = db.GetCollection<PVerifierCache>("qCollection");
 
         int parallelism = job.Parallelism;
         if (parallelism == 0)
@@ -124,7 +124,7 @@ public void Compile(ICompilerConfiguration job)
                     // add stdout to the database along with the corresponding checksum of the uclid query
                     using (var stream = File.OpenRead(Path.Join(job.OutputDirectory.FullName, r.Key)))
                     {
-                        var newResult = new UclidCache
+                        var newResult = new PVerifierCache
                         {
                             Reply = stdout,
                             Checksum = md5.ComputeHash(stream)

diff --git a/Src/PCompiler/CompilerCore/Backend/TargetLanguage.cs b/Src/PCompiler/CompilerCore/Backend/TargetLanguage.cs
@@ -3,7 +3,7 @@
 using Plang.Compiler.Backend.Java;
 using Plang.Compiler.Backend.Stately;
 using Plang.Compiler.Backend.Symbolic;
-using Plang.Compiler.Backend.Uclid5;
+using Plang.Compiler.Backend.PVerifier;
 
 namespace Plang.Compiler.Backend
 {
@@ -18,7 +18,7 @@ static TargetLanguage()
             RegisterCodeGenerator(CompilerOutput.Java, new JavaCompiler());
             RegisterCodeGenerator(CompilerOutput.Symbolic, new SymbolicCodeGenerator());
             RegisterCodeGenerator(CompilerOutput.Stately, new StatelyCodeGenerator());
-            RegisterCodeGenerator(CompilerOutput.Uclid5, new Uclid5CodeGenerator());
+            RegisterCodeGenerator(CompilerOutput.PVerifier, new PVerifierCodeGenerator());
         }
 
         private static void RegisterCodeGenerator(CompilerOutput name, ICodeGenerator generator)

diff --git a/Src/PCompiler/CompilerCore/Compiler.cs b/Src/PCompiler/CompilerCore/Compiler.cs
@@ -47,7 +47,7 @@ public int Compile(ICompilerConfiguration job)
                 return Environment.ExitCode;
             }
 
-            if (job.OutputLanguages.Contains(CompilerOutput.Uclid5))
+            if (job.OutputLanguages.Contains(CompilerOutput.PVerifier))
             {
                 // If using the PVerifier, don't output anything else
                 if (job.OutputLanguages.Count > 1)
@@ -78,7 +78,7 @@ public int Compile(ICompilerConfiguration job)
                 var compiledFiles = job.Backend.GenerateCode(job, scope);
                 foreach (var file in compiledFiles)
                 {
-                    if (entry != CompilerOutput.Uclid5)
+                    if (entry != CompilerOutput.PVerifier)
                     {
                         job.Output.WriteInfo($"Generated {file.FileName}.");
                     }
@@ -122,7 +122,7 @@ private static PParser.ProgramContext Parse(ICompilerConfiguration job, FileInfo
             var lexer = new PLexer(fileStream);
             var tokens = new CommonTokenStream(lexer);
 
-            if (!job.OutputLanguages.Contains(CompilerOutput.Uclid5))
+            if (!job.OutputLanguages.Contains(CompilerOutput.PVerifier))
             {
                 // disallow any pverifier tokens
                 tokens.Fill();

diff --git a/Src/PCompiler/CompilerCore/CompilerOutput.cs b/Src/PCompiler/CompilerCore/CompilerOutput.cs
@@ -7,6 +7,6 @@ public enum CompilerOutput
         CSharp,
         Java,
         Stately,
-        Uclid5,
+        PVerifier,
     }
 }
diff --git a/Src/PCompiler/PCommandLine/Parser/ParsePProjectFile.cs b/Src/PCompiler/PCommandLine/Parser/ParsePProjectFile.cs
@@ -243,7 +243,7 @@ private IList<CompilerOutput> GetTargetLanguages(FileInfo fullPathName)
                             outputLanguages.Add(CompilerOutput.Stately);
                             break;
                         case "pverifier":
-                            outputLanguages.Add(CompilerOutput.Uclid5);
+                            outputLanguages.Add(CompilerOutput.PVerifier);
                             break;
                         default:
                             throw new CommandlineParsingError(
-Original file line number
+Diff line change
@@ Expand Up / @@ -7,6 +7,6 @@ public enum CompilerOutput @@
             CSharp,
             Java,
             Stately,
-            Uclid5,
+            PVerifier,
         }
     }