Merge

5 files changed, 49 insertions, 27 deletions

diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs
index d6ac8754..d961eb3e 100644
--- a/Source/Core/Absy.cs
+++ b/Source/Core/Absy.cs
@@ -2434,6 +2434,10 @@ namespace Microsoft.Boogie {
         tc.Error(this, "preconditions must be of type bool");

       }

     }

+

+    public override Absy StdDispatch(StandardVisitor visitor) {

+      return visitor.VisitRequires(this);

+    }

   }

 

   public class Ensures : Absy, IPotentialErrorNode {

@@ -2528,6 +2532,10 @@ namespace Microsoft.Boogie {
         tc.Error(this, "postconditions must be of type bool");

       }

     }

+

+    public override Absy StdDispatch(StandardVisitor visitor) {

+      return visitor.VisitEnsures(this);

+    }

   }

 

   public class Procedure : DeclWithFormals {

diff --git a/Source/Core/AbsyExpr.cs b/Source/Core/AbsyExpr.cs
index 7e71453b..33b3a818 100644
--- a/Source/Core/AbsyExpr.cs
+++ b/Source/Core/AbsyExpr.cs
@@ -2122,12 +2122,16 @@ namespace Microsoft.Boogie {
         return false;

 

       NAryExpr other = (NAryExpr)obj;

-      return this.Args.ListEquals(other.Args) && object.Equals(this.Fun, other.Fun); 

+      return object.Equals(this.Fun, other.Fun) && this.Args.SequenceEqual(other.Args);

     }

     [Pure]

     public override int GetHashCode() {

       int h = this.Fun.GetHashCode();

-      h ^= this.Args.GetHashCode();

+      // DO NOT USE Args.GetHashCode() because that uses Object.GetHashCode() which uses references

+      // We want structural equality

+      foreach (var arg in Args) {

+        h = (97*h) + arg.GetHashCode();

+      }

       return h;

     }

     public override void Emit(TokenTextWriter stream, int contextBindingStrength, bool fragileContext) {

diff --git a/Source/Core/AbsyQuant.cs b/Source/Core/AbsyQuant.cs
index 9425f698..32985053 100644
--- a/Source/Core/AbsyQuant.cs
+++ b/Source/Core/AbsyQuant.cs
@@ -103,20 +103,35 @@ namespace Microsoft.Boogie {
 

       var other = (BinderExpr) obj;

 

-      var a = this.TypeParameters.ListEquals(other.TypeParameters);

-      var b = this.Dummies.ListEquals(other.Dummies);

-      var c = !CompareAttributesAndTriggers || object.Equals(this.Attributes, other.Attributes);

-      var d = object.Equals(this.Body, other.Body);

-

-      return a && b && c && d;

+      return this.TypeParameters.SequenceEqual(other.TypeParameters)

+             && this.Dummies.SequenceEqual(other.Dummies)

+             && (!CompareAttributesAndTriggers || object.Equals(this.Attributes, other.Attributes))

+             && object.Equals(this.Body, other.Body);

     }

 

     [Pure]

     public override int GetHashCode() {

-      int h = this.Dummies.GetHashCode();

       // Note, we don't hash triggers and attributes

+   

+      // DO NOT USE Dummies.GetHashCode() because we want structurally

+      // identical Expr to have the same hash code **not** identical references

+      // to have the same hash code.

+      int h = 0;

+      foreach (var dummyVar in this.Dummies) {

+        h = ( 53 * h ) + dummyVar.GetHashCode();

+      }

+

       h ^= this.Body.GetHashCode();

-      h = h * 5 + this.TypeParameters.GetHashCode();

+

+      // DO NOT USE TypeParameters.GetHashCode() because we want structural

+      // identical Expr to have the same hash code **not** identical references

+      // to have the same hash code.

+      int h2 = 0;

+      foreach (var typeParam in this.TypeParameters) {

+        h2 = ( 97 * h2 ) + typeParam.GetHashCode();

+      }

+

+      h = h * 5 + h2;

       h *= ((int)Kind + 1);

       return h;

     }

@@ -472,7 +487,7 @@ namespace Microsoft.Boogie {
       if (other == null) {

         return false;

       } else {

-        return this.Tr.ListEquals(other.Tr) && 

+        return this.Tr.SequenceEqual(other.Tr) && 

           (Next == null ? other.Next == null : object.Equals(Next, other.Next));

       }

     }

@@ -853,4 +868,4 @@ namespace Microsoft.Boogie {
     }

 

   }

-}
\ No newline at end of file
+}

diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs
index 65554a1e..d61c9941 100644
--- a/Source/Core/CommandLineOptions.cs
+++ b/Source/Core/CommandLineOptions.cs
@@ -496,8 +496,6 @@ namespace Microsoft.Boogie {
     public int TrustPhasesUpto = -1;

     public int TrustPhasesDownto = int.MaxValue;

 

-    public bool UseParallelism = true;

-

     public enum VCVariety {

       Structured,

       Block,

@@ -1431,7 +1429,6 @@ namespace Microsoft.Boogie {
               ps.CheckBooleanFlag("verifySeparately", ref VerifySeparately) ||

               ps.CheckBooleanFlag("trustAtomicityTypes", ref TrustAtomicityTypes) ||

               ps.CheckBooleanFlag("trustNonInterference", ref TrustNonInterference) ||

-              ps.CheckBooleanFlag("doNotUseParallelism", ref UseParallelism, false) ||

               ps.CheckBooleanFlag("useBaseNameForFileName", ref UseBaseNameForFileName)

               ) {

             // one of the boolean flags matched

diff --git a/Source/Core/Util.cs b/Source/Core/Util.cs
index 1b8353e1..0a2e5a22 100644
--- a/Source/Core/Util.cs
+++ b/Source/Core/Util.cs
@@ -66,18 +66,6 @@ namespace Microsoft.Boogie {
     {

       return source1.Zip(source2, (e1, e2) => new Tuple<TSource1, TSource2>(e1, e2));

     }

-

-    public static bool ListEquals<A>(this List<A> xs, List<A> ys) {

-      var equal = xs.Count == ys.Count;

-      for (int i = 0; equal && i < xs.Count; i++) {

-        equal = object.Equals(xs[i], ys[i]);

-      }

-      return equal;

-    }

-

-    public static int ListHash<A>(this List<A> xs) {

-      return xs.Aggregate(xs.Count, (current, x) => current ^ xs.GetHashCode());

-    }

   }

 

   public class TokenTextWriter : IDisposable {

@@ -264,6 +252,11 @@ namespace Microsoft.Boogie {
       }

     }

 

+    public TokenTextWriter(string filename)

+        : this(filename, false)

+    {

+    }

+

     public TokenTextWriter(string filename, bool pretty)

       : base() {

       Contract.Requires(filename != null);

@@ -300,6 +293,11 @@ namespace Microsoft.Boogie {
       this.writer = writer;

     }

 

+    public TokenTextWriter(TextWriter writer)

+        : this(writer, false)

+    {

+    }

+

     public TokenTextWriter(TextWriter writer, bool pretty)

       : base() {

       Contract.Requires(writer != null);