Fix #49. (Race condition on the addition of entrypoint attribute)

boogie-org · Aug 18, 2017 · 53eae67 · 53eae67
1 parent 82b603c
commit 53eae67
Showing 1 changed file with 8 additions and 2 deletions.
diff --git a/AddOns/FastAVN/FastAVN/Program.cs b/AddOns/FastAVN/FastAVN/Program.cs
@@ -681,8 +681,6 @@ public void RunSplitAndAvhAndAv()
 
                     var topLevelProcs = new HashSet<string> { impl.Name };
                     if(initProc != null) topLevelProcs.Add(initProc.Name);    
-                    //Add {:entrypoint} add attribute to impl
-                    impl.Proc.AddAttribute("entrypoint");
 
                     BoogieUtil.pruneProcs(newprogram, topLevelProcs);
 
@@ -715,6 +713,14 @@ public void RunSplitAndAvhAndAv()
                         continue;
                     }
 
+                    // make a copy of impl.Proc
+                    var dup = new FixedDuplicator(true);
+                    var implProcCopy = dup.VisitProcedure(impl.Proc);
+                    // Mark entrypoint
+                    implProcCopy.AddAttribute("entrypoint");
+
+                    newprogram.RemoveTopLevelDeclaration(impl.Proc);
+                    newprogram.AddTopLevelDeclaration(implProcCopy);
 
                     BoogieUtil.PrintProgram(newprogram, pruneFile); // dump sliced program