the allocator corresponding to every linear variable

in the modset of a procedure is now put into the modset itself
(in addition to the allocators for the output parameters)

1 files changed, 15 insertions, 3 deletions

diff --git a/Source/Core/LinearSets.cs b/Source/Core/LinearSets.cs
index d4c12ee0..75ea7b69 100644
--- a/Source/Core/LinearSets.cs
+++ b/Source/Core/LinearSets.cs
@@ -423,7 +423,7 @@ namespace Microsoft.Boogie
             {

                 Procedure proc = decl as Procedure;

                 if (proc == null) continue;

-                HashSet<string> domainNamesForOutParams = new HashSet<string>();

+                HashSet<string> domainNames = new HashSet<string>();

                 foreach (Variable v in proc.OutParams)

                 {

                     var domainName = QKeyValue.FindStringAttribute(v.Attributes, "linear");

@@ -432,8 +432,20 @@ namespace Microsoft.Boogie
                     {

                         linearDomains[domainName] = new LinearDomain(program, v, domainName);

                     }

-                    if (domainNamesForOutParams.Contains(domainName)) continue;

-                    domainNamesForOutParams.Add(domainName);

+                    domainNames.Add(domainName);

+                }

+                foreach (IdentifierExpr ie in proc.Modifies)

+                {

+                    var domainName = QKeyValue.FindStringAttribute(ie.Decl.Attributes, "linear");

+                    if (domainName == null) continue;

+                    if (!linearDomains.ContainsKey(domainName))

+                    {

+                        linearDomains[domainName] = new LinearDomain(program, ie.Decl, domainName);

+                    }

+                    domainNames.Add(domainName);

+                }

+                foreach (string domainName in domainNames)

+                {

                     proc.Modifies.Add(new IdentifierExpr(Token.NoToken, linearDomains[domainName].allocator));

                 }

             }