diff --git a/AddOns/FastAVN/FastAVN/Program.cs b/AddOns/FastAVN/FastAVN/Program.cs index c6fe9197d..f6dd46bcf 100644 --- a/AddOns/FastAVN/FastAVN/Program.cs +++ b/AddOns/FastAVN/FastAVN/Program.cs @@ -681,8 +681,6 @@ public void RunSplitAndAvhAndAv() var topLevelProcs = new HashSet { 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