fixed a couple of issues:

1. eliminated special case for alloc
2. added iteration over out parameters in VisitCallCmd

1 files changed, 7 insertions, 3 deletions

diff --git a/Source/Core/DeadVarElim.cs b/Source/Core/DeadVarElim.cs
index 711770c2..ff097ce8 100644
--- a/Source/Core/DeadVarElim.cs
+++ b/Source/Core/DeadVarElim.cs
@@ -163,11 +163,17 @@ namespace Microsoft.Boogie {
       Contract.Ensures(Contract.Result<Cmd>() != null);

       Cmd ret = base.VisitCallCmd(callCmd);

       Procedure callee = callCmd.Proc;

-      if (callee != null && modSets.ContainsKey(callee)) {

+      if (callee == null)

+          return ret;

+      if (modSets.ContainsKey(callee)) {

         foreach (Variable var in modSets[callee]) {

           ProcessVariable(var);

         }

       }

+      foreach (IdentifierExpr ie in callCmd.Outs)

+      {

+        ProcessVariable(ie.Decl);

+      }

       return ret;

     }

     private static void ProcessVariable(Variable var) {

@@ -176,8 +182,6 @@ namespace Microsoft.Boogie {
         return;

       if (!(var is GlobalVariable))

         return;

-      if (var.Name == "alloc")

-        return;

       if (!modSets.ContainsKey(localProc)) {

         modSets[localProc] = new HashSet<Variable/*!*/>();

       }