fixed bug in OG

added another OG sample illustrating rely-guarantee encoding

3 files changed, 16 insertions, 11 deletions

diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs
index 69fb547c..c4db46f4 100644
--- a/Source/BoogieDriver/BoogieDriver.cs
+++ b/Source/BoogieDriver/BoogieDriver.cs
@@ -197,7 +197,7 @@ namespace Microsoft.Boogie {
         }

         LinearSetTransform linearTransform = new LinearSetTransform(program);

         linearTransform.Transform();

-          

+

         EliminateDeadVariablesAndInline(program);

 

         int errorCount, verified, inconclusives, timeOuts, outOfMemories;

diff --git a/Source/Core/LinearSets.cs b/Source/Core/LinearSets.cs
index 4edbfeed..d2904d59 100644
--- a/Source/Core/LinearSets.cs
+++ b/Source/Core/LinearSets.cs
@@ -285,11 +285,6 @@ namespace Microsoft.Boogie
                     b.Cmds = newCmds;

                 }

 

-                foreach (var v in copies.Values)

-                {

-                    impl.LocVars.Add(v);

-                }

-

                 {

                     // Loops

                     impl.PruneUnreachableBlocks();

@@ -332,6 +327,11 @@ namespace Microsoft.Boogie
                     newCmds.AddRange(impl.Blocks[0].Cmds);

                     impl.Blocks[0].Cmds = newCmds;

                 }

+

+                foreach (var v in copies.Values)

+                {

+                    impl.LocVars.Add(v);

+                }

             }

 

             foreach (var decl in program.TopLevelDeclarations)

@@ -437,7 +437,10 @@ namespace Microsoft.Boogie
                 lhss.Add(new SimpleAssignLhs(Token.NoToken, new IdentifierExpr(Token.NoToken, copies[allocator])));

                 rhss.Add(new IdentifierExpr(Token.NoToken, allocator));

             }

-            newCmds.Add(new AssignCmd(Token.NoToken, lhss, rhss));

+            if (lhss.Count > 0)

+            {

+                newCmds.Add(new AssignCmd(Token.NoToken, lhss, rhss));

+            }

             foreach (string domainName in domainNameToHavocVars.Keys)

             {

                 var allocator = linearDomains[domainName].allocator;

diff --git a/Source/Core/OwickiGries.cs b/Source/Core/OwickiGries.cs
index 6eaf9650..55565375 100644
--- a/Source/Core/OwickiGries.cs
+++ b/Source/Core/OwickiGries.cs
@@ -232,17 +232,19 @@ namespace Microsoft.Boogie
                 // Create substitution maps

                 Hashtable map = new Hashtable();

                 VariableSeq locals = new VariableSeq();

-                foreach (Variable inParam in impl.Proc.InParams)

+                for (int i = 0; i < impl.Proc.InParams.Length; i++)

                 {

+                    Variable inParam = impl.Proc.InParams[i];

                     var copy = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, inParam.Name, inParam.TypedIdent.Type));

                     locals.Add(copy);

-                    map[inParam] = new IdentifierExpr(Token.NoToken, copy);

+                    map[impl.InParams[i]] = new IdentifierExpr(Token.NoToken, copy);

                 }

-                foreach (Variable outParam in impl.Proc.OutParams)

+                for (int i = 0; i < impl.Proc.OutParams.Length; i++)

                 {

+                    Variable outParam = impl.Proc.OutParams[i];

                     var copy = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, outParam.Name, outParam.TypedIdent.Type), outParam.Attributes);

                     locals.Add(copy);

-                    map[outParam] = new IdentifierExpr(Token.NoToken, copy);

+                    map[impl.OutParams[i]] = new IdentifierExpr(Token.NoToken, copy);

                 }

                 foreach (Variable local in impl.LocVars)

                 {