Re-enable parts of the WholeProgram class

atomb · Jul 3, 2024 · df3c917 · df3c917
1 parent a757f0d
commit df3c917
Showing 1 changed file with 8 additions and 16 deletions.
diff --git a/Sources/SymDiff/source/WholeProgram.cs b/Sources/SymDiff/source/WholeProgram.cs
@@ -658,8 +658,6 @@ private static void AddOKEnsures(string p1Prefix, string p2Prefix, bool mergeGlo
         }
         private static void InsertConstantsOK(string filenamePrefix, Program Prog, int n)
         {
-            /*
-            CodeCopier codeCopier = new CodeCopier();
             String OKstr = filenamePrefix + ".OK";// +n;
             AddIteAxiom(filenamePrefix, Prog.TopLevelDeclarations.ToList());
 
@@ -684,13 +682,11 @@ private static void InsertConstantsOK(string filenamePrefix, Program Prog, int n
                     {
                         AssertCmd assertCmd = cmd as AssertCmd;
                         AssumeCmd assumeCmd = cmd as AssumeCmd;
-                        if (assertCmd == null || assertCmd.Attributes == null)
-                        {
-                            newCmds.Add(codeCopier.CopyCmd(cmd));
+                        if (assertCmd == null || assertCmd.Attributes == null) {
+                            newCmds.Add((Cmd) cmd.Clone());
                         }
-                        else
-                        {
-                            newCmds.Add(codeCopier.CopyCmd(cmd));
+                        else {
+                            newCmds.Add((Cmd) cmd.Clone());
                             if (!assertCmd.Attributes.Key.Contains("sourcefile"))
                                 continue;
                             if (!assertCmd.Attributes.Next.Key.Contains("sourceline"))
@@ -720,15 +716,14 @@ private static void InsertConstantsOK(string filenamePrefix, Program Prog, int n
 
                     }
                     if (newAssumeCmd != null)
-                        newCmds.Add(codeCopier.CopyCmd(newAssumeCmd));
+                        newCmds.Add(newAssumeCmd);
 
                     newBlock = new Block(block.tok, block.Label, newCmds, block.TransferCmd);
                     newBlocks.Add(newBlock);
                 }
                 impl.Blocks = newBlocks;
             }
             Prog.AddTopLevelDeclarations(decls); //Prog.TopLevelDeclarations.InsertRange(1, decls);
-            */
         }
         private static string FindOK1var(List<Cmd> cmdSeq, string p1prefix)
         {
@@ -775,9 +770,7 @@ private static void InsertOK(int n, Program p, string[] args)
         }
         private static void InsertOKProcs(string OKstr, Program p, string filename)
         {
-            /*
             OKstr = filename.Replace(".bpl", "") + "." + OKstr;
-            CodeCopier codeCopier = new CodeCopier();
             IEnumerable<Declaration> impls = p.TopLevelDeclarations.Where(x => x is Implementation);
             foreach (Implementation impl in impls)
             {
@@ -793,7 +786,7 @@ private static void InsertOKProcs(string OKstr, Program p, string filename)
                         AssertCmd assertCmd = cmd as AssertCmd;
                         if (assertCmd == null)
                         {
-                            newCmds.Add(codeCopier.CopyCmd(cmd));
+                            newCmds.Add((Cmd)cmd.Clone());
                         }
                         else
                         {
@@ -805,16 +798,15 @@ private static void InsertOKProcs(string OKstr, Program p, string filename)
                             token.filename = filename;
                             Expr pred = Expr.And(Expr.Ident(OKstr, new BasicType(SimpleType.Bool)), assertCmd.Expr);
                             AssignCmd assignToOK = Cmd.SimpleAssign(token, new IdentifierExpr(new Token(), OKstr, new BasicType(SimpleType.Bool)), pred);
-                            newCmds.Add(codeCopier.CopyCmd(assignToOK));
-                            newCmds.Add(codeCopier.CopyCmd(cmd));
+                            newCmds.Add(assignToOK);
+                            newCmds.Add((Cmd)cmd.Clone());
                         }
                     }
                     newBlock = new Block(block.tok, block.Label, newCmds, block.TransferCmd);
                     newBlocks.Add(newBlock);
                 }
                 impl.Blocks = newBlocks;
             }
-            */
         }
 
         //Differential inlining