Fixes to refactoring

5 files changed, 33 insertions, 27 deletions

diff --git a/Source/Core/BitvectorAnalysis.cs b/Source/Core/BitvectorAnalysis.cs
index 0bd3123b..a555352b 100644
--- a/Source/Core/BitvectorAnalysis.cs
+++ b/Source/Core/BitvectorAnalysis.cs
@@ -528,7 +528,7 @@ namespace Microsoft.Boogie {
       DiscoverIntAndBv32Functions(program);

 

       BvType bv32Type = new BvType(32);

-      List<Variable> bv32In = new List<Variable>(new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "in", bv32Type), true));

+      List<Variable> bv32In = new List<Variable> { new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "in", bv32Type), true) };

       Formal bv32Out = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "out", bv32Type), false);

       bv32Id = new Function(Token.NoToken, "bv32Id", bv32In, bv32Out);

       bv32Id.Body = new IdentifierExpr(Token.NoToken, bv32In[0]);

diff --git a/Source/Core/LinearSets.cs b/Source/Core/LinearSets.cs
index 8d0faf2b..957718fa 100644
--- a/Source/Core/LinearSets.cs
+++ b/Source/Core/LinearSets.cs
@@ -400,7 +400,12 @@ namespace Microsoft.Boogie
                 foreach (string domainName in linearDomains.Keys)

                 {

                     var domain = linearDomains[domainName];

-                    Formal f = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, domainName + "_in", new MapType(Token.NoToken, new TypeVariableSeq(), new List<Type>(domain.elementType), Type.Bool)), true);

+                    Formal f = new Formal(

+                      Token.NoToken,

+                      new TypedIdent(Token.NoToken, 

+                        domainName + "_in",

+                        new MapType(Token.NoToken, new TypeVariableSeq(), 

+                          new List<Type> { domain.elementType }, Type.Bool)), true);

                     impl.InParams.Add(f);

                     domainNameToInputVar[domainName] = f;

                 }

@@ -518,7 +523,7 @@ namespace Microsoft.Boogie
                 {

                     proc.Requires.Add(new Requires(true, DisjointnessExpr(domainName, domainNameToInputScope[domainName])));

                     var domain = linearDomains[domainName];

-                    Formal f = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, domainName + "_in", new MapType(Token.NoToken, new TypeVariableSeq(), new List<Type>(domain.elementType), Type.Bool)), true);

+                    Formal f = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, domainName + "_in", new MapType(Token.NoToken, new TypeVariableSeq(), new List<Type> { domain.elementType }, Type.Bool)), true);

                     proc.InParams.Add(f);

                     domainNameToOutputScope[domainName].Add(f);

                     proc.Ensures.Add(new Ensures(true, DisjointnessExpr(domainName, domainNameToOutputScope[domainName])));

@@ -568,7 +573,7 @@ namespace Microsoft.Boogie
         public Expr DisjointnessExpr(string domainName, HashSet<Variable> scope)

         {

             LinearDomain domain = linearDomains[domainName];

-            BoundVariable partition = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("partition_{0}", domainName), new MapType(Token.NoToken, new TypeVariableSeq(), new List<Type>(domain.elementType), Microsoft.Boogie.Type.Int)));

+            BoundVariable partition = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("partition_{0}", domainName), new MapType(Token.NoToken, new TypeVariableSeq(), new List<Type> { domain.elementType }, Microsoft.Boogie.Type.Int)));

             Expr disjointExpr = Expr.True;

             int count = 0;

             foreach (Variable v in scope)

@@ -580,7 +585,7 @@ namespace Microsoft.Boogie
                 e = Expr.Binary(BinaryOperator.Opcode.Eq, e, new NAryExpr(Token.NoToken, new FunctionCall(domain.mapConstBool), new ExprSeq(Expr.True)));

                 disjointExpr = Expr.Binary(BinaryOperator.Opcode.And, e, disjointExpr);

             }

-            return new ExistsExpr(Token.NoToken, new List<Variable>(partition), disjointExpr);

+            return new ExistsExpr(Token.NoToken, new List<Variable> { partition }, disjointExpr);

         }

     }

 

@@ -599,11 +604,11 @@ namespace Microsoft.Boogie
             this.elementType = elementType;

             this.axioms = new List<Axiom>();

 

-            MapType mapTypeBool = new MapType(Token.NoToken, new TypeVariableSeq(), new List<Type>(this.elementType), Type.Bool);

-            MapType mapTypeInt = new MapType(Token.NoToken, new TypeVariableSeq(), new List<Type>(this.elementType), Type.Int);

+            MapType mapTypeBool = new MapType(Token.NoToken, new TypeVariableSeq(), new List<Type> { this.elementType }, Type.Bool);

+            MapType mapTypeInt = new MapType(Token.NoToken, new TypeVariableSeq(), new List<Type> { this.elementType }, Type.Int);

             this.mapOrBool = new Function(Token.NoToken, domainName + "_linear_MapOr",

-                                          new List<Variable>(new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "a", mapTypeBool), true),

-                                                          new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "b", mapTypeBool), true)),

+                                          new List<Variable> { new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "a", mapTypeBool), true),

+                                                          new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "b", mapTypeBool), true) },

                                           new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "c", mapTypeBool), false));

             if (CommandLineOptions.Clo.UseArrayTheory)

             {

@@ -622,16 +627,16 @@ namespace Microsoft.Boogie
                 var rhsTerm = Expr.Binary(BinaryOperator.Opcode.Or,

                                           new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1), new ExprSeq(aie, xie)),

                                           new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1), new ExprSeq(bie, xie)));

-                var axiomExpr = new ForallExpr(Token.NoToken, new TypeVariableSeq(), new List<Variable>(a, b), null, 

+                var axiomExpr = new ForallExpr(Token.NoToken, new TypeVariableSeq(), new List<Variable> { a, b }, null, 

                                                new Trigger(Token.NoToken, true, new ExprSeq(mapApplTerm)), 

-                                               new ForallExpr(Token.NoToken, new List<Variable>(x), Expr.Binary(BinaryOperator.Opcode.Eq, lhsTerm, rhsTerm)));

+                                               new ForallExpr(Token.NoToken, new List<Variable> { x }, Expr.Binary(BinaryOperator.Opcode.Eq, lhsTerm, rhsTerm)));

                 axiomExpr.Typecheck(new TypecheckingContext(null));

                 axioms.Add(new Axiom(Token.NoToken, axiomExpr));

             }

 

             this.mapImpBool = new Function(Token.NoToken, domainName + "_linear_MapImp",

-                                              new List<Variable>(new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "a", mapTypeBool), true),

-                                                              new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "b", mapTypeBool), true)),

+                                              new List<Variable> { new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "a", mapTypeBool), true),

+                                                              new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "b", mapTypeBool), true) },

                                               new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "c", mapTypeBool), false));

             if (CommandLineOptions.Clo.UseArrayTheory)

             {

@@ -650,15 +655,15 @@ namespace Microsoft.Boogie
                 var rhsTerm = Expr.Binary(BinaryOperator.Opcode.Imp,

                                           new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1), new ExprSeq(aie, xie)),

                                           new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1), new ExprSeq(bie, xie)));

-                var axiomExpr = new ForallExpr(Token.NoToken, new TypeVariableSeq(), new List<Variable>(a, b), null,

+                var axiomExpr = new ForallExpr(Token.NoToken, new TypeVariableSeq(), new List<Variable> { a, b }, null,

                                                new Trigger(Token.NoToken, true, new ExprSeq(mapApplTerm)), 

-                                               new ForallExpr(Token.NoToken, new List<Variable>(x), Expr.Binary(BinaryOperator.Opcode.Eq, lhsTerm, rhsTerm)));

+                                               new ForallExpr(Token.NoToken, new List<Variable> { x }, Expr.Binary(BinaryOperator.Opcode.Eq, lhsTerm, rhsTerm)));

                 axiomExpr.Typecheck(new TypecheckingContext(null));

                 axioms.Add(new Axiom(Token.NoToken, axiomExpr));

             }

 

             this.mapConstBool = new Function(Token.NoToken, domainName + "_linear_MapConstBool",

-                                              new List<Variable>(new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "b", Type.Bool), true)),

+                                              new List<Variable> { new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "b", Type.Bool), true) },

                                               new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "c", mapTypeBool), false));

             if (CommandLineOptions.Clo.UseArrayTheory)

             {

@@ -670,19 +675,19 @@ namespace Microsoft.Boogie
                 IdentifierExpr xie = new IdentifierExpr(Token.NoToken, x);

                 var trueTerm = new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1), 

                                            new ExprSeq(new NAryExpr(Token.NoToken, new FunctionCall(mapConstBool), new ExprSeq(Expr.True)), xie));

-                var trueAxiomExpr = new ForallExpr(Token.NoToken, new List<Variable>(x), trueTerm);

+                var trueAxiomExpr = new ForallExpr(Token.NoToken, new List<Variable> { x }, trueTerm);

                 trueAxiomExpr.Typecheck(new TypecheckingContext(null));

                 axioms.Add(new Axiom(Token.NoToken, trueAxiomExpr));

                 var falseTerm = new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1),

                                            new ExprSeq(new NAryExpr(Token.NoToken, new FunctionCall(mapConstBool), new ExprSeq(Expr.False)), xie)); 

-                var falseAxiomExpr = new ForallExpr(Token.NoToken, new List<Variable>(x), Expr.Unary(Token.NoToken, UnaryOperator.Opcode.Not, falseTerm));

+                var falseAxiomExpr = new ForallExpr(Token.NoToken, new List<Variable> { x }, Expr.Unary(Token.NoToken, UnaryOperator.Opcode.Not, falseTerm));

                 falseAxiomExpr.Typecheck(new TypecheckingContext(null));

                 axioms.Add(new Axiom(Token.NoToken, falseAxiomExpr));

             }

 

             this.mapEqInt = new Function(Token.NoToken, domainName + "_linear_MapEq",

-                                              new List<Variable>(new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "a", mapTypeInt), true),

-                                                              new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "b", mapTypeInt), true)),

+                                              new List<Variable> { new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "a", mapTypeInt), true),

+                                                              new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "b", mapTypeInt), true) },

                                               new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "c", mapTypeBool), false));

             if (CommandLineOptions.Clo.UseArrayTheory)

             {

@@ -701,15 +706,15 @@ namespace Microsoft.Boogie
                 var rhsTerm = Expr.Binary(BinaryOperator.Opcode.Eq,

                                           new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1), new ExprSeq(aie, xie)),

                                           new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1), new ExprSeq(bie, xie)));

-                var axiomExpr = new ForallExpr(Token.NoToken, new TypeVariableSeq(), new List<Variable>(a, b), null, 

+                var axiomExpr = new ForallExpr(Token.NoToken, new TypeVariableSeq(), new List<Variable> { a, b }, null, 

                                                new Trigger(Token.NoToken, true, new ExprSeq(mapApplTerm)), 

-                                               new ForallExpr(Token.NoToken, new List<Variable>(x), Expr.Binary(BinaryOperator.Opcode.Eq, lhsTerm, rhsTerm)));

+                                               new ForallExpr(Token.NoToken, new List<Variable> { x }, Expr.Binary(BinaryOperator.Opcode.Eq, lhsTerm, rhsTerm)));

                 axiomExpr.Typecheck(new TypecheckingContext(null));

                 axioms.Add(new Axiom(Token.NoToken, axiomExpr));

             }

 

             this.mapConstInt = new Function(Token.NoToken, domainName + "_linear_MapConstInt",

-                                          new List<Variable>(new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "b", Type.Int), true)),

+                                          new List<Variable> { new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "b", Type.Int), true) },

                                           new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "c", mapTypeInt), false));

             if (CommandLineOptions.Clo.UseArrayTheory)

             {

@@ -722,7 +727,7 @@ namespace Microsoft.Boogie
                 BoundVariable x = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "x", elementType));

                 IdentifierExpr xie = new IdentifierExpr(Token.NoToken, x);

                 var lhsTerm = new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1), new ExprSeq(new NAryExpr(Token.NoToken, new FunctionCall(mapConstInt), new ExprSeq(aie)), xie));

-                var axiomExpr = new ForallExpr(Token.NoToken, new List<Variable>(a, x), Expr.Binary(BinaryOperator.Opcode.Eq, lhsTerm, aie));

+                var axiomExpr = new ForallExpr(Token.NoToken, new List<Variable> { a, x }, Expr.Binary(BinaryOperator.Opcode.Eq, lhsTerm, aie));

                 axiomExpr.Typecheck(new TypecheckingContext(null));

                 axioms.Add(new Axiom(Token.NoToken, axiomExpr));

             }

diff --git a/Source/Core/OwickiGries.cs b/Source/Core/OwickiGries.cs
index 2df7b3ba..cbaff3ef 100644
--- a/Source/Core/OwickiGries.cs
+++ b/Source/Core/OwickiGries.cs
@@ -168,7 +168,7 @@ namespace Microsoft.Boogie
             foreach (string domainName in linearTypechecker.linearDomains.Keys)

             {

                 var domain = linearTypechecker.linearDomains[domainName];

-                Formal f = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, domainName + "_in", new MapType(Token.NoToken, new TypeVariableSeq(), new List<Type>(domain.elementType), Type.Bool)), true);

+                Formal f = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, domainName + "_in", new MapType(Token.NoToken, new TypeVariableSeq(), new List<Type> { domain.elementType }, Type.Bool)), true);

                 inputs.Add(f);

             }

             foreach (IdentifierExpr ie in globalMods)

@@ -727,7 +727,7 @@ namespace Microsoft.Boogie
             foreach (string domainName in linearTypechecker.linearDomains.Keys)

             {

                 var domain = linearTypechecker.linearDomains[domainName];

-                Formal f = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, domainName + "_in", new MapType(Token.NoToken, new TypeVariableSeq(), new List<Type>(domain.elementType), Type.Bool)), true);

+                Formal f = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, domainName + "_in", new MapType(Token.NoToken, new TypeVariableSeq(), new List<Type> { domain.elementType }, Type.Bool)), true);

                 inputs.Add(f);

             }

             foreach (IdentifierExpr ie in globalMods)

diff --git a/Source/Core/TypeAmbiguitySeeker.cs b/Source/Core/TypeAmbiguitySeeker.cs
index 1293dd1b..ecb1e418 100644
--- a/Source/Core/TypeAmbiguitySeeker.cs
+++ b/Source/Core/TypeAmbiguitySeeker.cs
@@ -5,6 +5,7 @@
 //-----------------------------------------------------------------------------

 using System;

 using System.Diagnostics.Contracts;

+using System.Collections.Generic;

 

 // Visitor to search for types proxies that could not completely be

 // determined by type inference. If this happens, a warning is

diff --git a/Source/Predication/SmartBlockPredicator.cs b/Source/Predication/SmartBlockPredicator.cs
index 484a866d..28005186 100644
--- a/Source/Predication/SmartBlockPredicator.cs
+++ b/Source/Predication/SmartBlockPredicator.cs
@@ -115,7 +115,7 @@ public class SmartBlockPredicator {
             new IdentifierExpr(Token.NoToken, havocVar);

         }

         cmdSeq.Add(new HavocCmd(Token.NoToken,

-                                new List<IdentifierExpr>(havocTempExpr)));

+                                new List<IdentifierExpr> { havocTempExpr }));

         cmdSeq.Add(Cmd.SimpleAssign(Token.NoToken, v,

                                     new NAryExpr(Token.NoToken,

                                       new IfThenElse(Token.NoToken),