1 files changed, 260 insertions, 260 deletions
diff --git a/Source/AIFramework/VariableMap/Nullness.cs b/Source/AIFramework/VariableMap/Nullness.cs
index 613f55e0..474792e0 100644
--- a/Source/AIFramework/VariableMap/Nullness.cs
+++ b/Source/AIFramework/VariableMap/Nullness.cs
@@ -1,260 +1,260 @@
-//-----------------------------------------------------------------------------
-//
-// Copyright (C) Microsoft Corporation.  All Rights Reserved.
-//
-//-----------------------------------------------------------------------------
-using System.Diagnostics.Contracts;
-namespace Microsoft.AbstractInterpretationFramework {
-  using System.Collections;
-  using System.Diagnostics;
-  //using System.Compiler.Analysis;
-
-  public class NullnessLattice : MicroLattice {
-    readonly INullnessFactory/*!*/ factory;
-    [ContractInvariantMethod]
-    void ObjectInvariant() {
-      Contract.Invariant(factory != null);
-    }
-
-
-    public NullnessLattice(INullnessFactory/*!*/ factory) {
-      Contract.Requires(factory != null);
-      this.factory = factory;
-      // base();
-    }
-
-    enum Value {
-      Bottom,
-      NotNull,
-      Null,
-      MayBeNull
-    }
-
-    private class Elt : Element {
-      public Value value;
-
-      public Elt(Value v) {
-        this.value = v;
-      }
-
-      [Pure]
-      public override System.Collections.Generic.ICollection<IVariable/*!*/>/*!*/ FreeVariables() {
-        Contract.Ensures(cce.NonNullElements(Contract.Result<System.Collections.Generic.ICollection<IVariable>>()));
-        return cce.NonNull(new System.Collections.Generic.List<IVariable/*!*/>()).AsReadOnly();
-      }
-
-      public override Element/*!*/ Clone() {
-        Contract.Ensures(Contract.Result<Element>() != null);
-        return new Elt(this.value);
-      }
-    }
-
-
-    public override Element/*!*/ Top {
-      get {
-        Contract.Ensures(Contract.Result<Element>() != null);
-        return new Elt(Value.MayBeNull);
-      }
-    }
-
-    public override Element/*!*/ Bottom {
-      get {
-        Contract.Ensures(Contract.Result<Element>() != null);
-        return new Elt(Value.Bottom);
-      }
-    }
-
-    public static Element/*!*/ Null {
-      get {
-        Contract.Ensures(Contract.Result<Element>() != null);
-        return new Elt(Value.Null);
-      }
-    }
-
-    public static Element/*!*/ NotNull {
-      get {
-        Contract.Ensures(Contract.Result<Element>() != null);
-        return new Elt(Value.NotNull);
-      }
-    }
-
-    public override bool IsTop(Element/*!*/ element) {
-      //Contract.Requires(element != null);
-      Elt e = (Elt)element;
-      return e.value == Value.MayBeNull;
-    }
-
-    public override bool IsBottom(Element/*!*/ element) {
-      //Contract.Requires(element != null);
-      Elt e = (Elt)element;
-      return e.value == Value.Bottom;
-    }
-
-    public override Lattice.Element/*!*/ NontrivialJoin(Element/*!*/ first, Element/*!*/ second) {
-      //Contract.Requires(second != null);
-      //Contract.Requires(first != null);
-      Contract.Ensures(Contract.Result<Lattice.Element>() != null);
-      Elt a = (Elt)first;
-      Elt b = (Elt)second;
-      return (a.value == b.value) ? a : (Elt)Top;
-    }
-
-    public override Lattice.Element/*!*/ NontrivialMeet(Element/*!*/ first, Element/*!*/ second) {
-      //Contract.Requires(second != null);
-      //Contract.Requires(first != null);
-      Contract.Ensures(Contract.Result<Lattice.Element>() != null);
-      Elt a = (Elt)first;
-      Elt b = (Elt)second;
-      return (a.value == b.value) ? a : (Elt)Bottom;
-    }
-
-    public override Element/*!*/ Widen(Element/*!*/ first, Element/*!*/ second) {
-      //Contract.Requires(second != null);
-      //Contract.Requires(first != null);
-      Contract.Ensures(Contract.Result<Element>() != null);
-      return Join(first, second);
-    }
-
-    protected override bool AtMost(Element/*!*/ first, Element/*!*/ second) // this <= that
-    {
-      //Contract.Requires(first != null);
-      //Contract.Requires(second != null);
-      Elt a = (Elt)first;
-      Elt b = (Elt)second;
-      return a.value == b.value;
-    }
-
-    public override IExpr/*!*/ ToPredicate(IVariable/*!*/ var, Element/*!*/ element) {
-      //Contract.Requires(element != null);
-      //Contract.Requires(var != null);
-      Contract.Ensures(Contract.Result<IExpr>() != null);
-      Elt e = (Elt)element;
-
-      if (e.value == Value.NotNull) {
-        return factory.Neq(var, factory.Null);
-      }
-      if (e.value == Value.Null) {
-        return factory.Eq(var, factory.Null);
-      }
-      {
-        Contract.Assert(false);
-        throw new cce.UnreachableException();
-      }
-      throw new System.Exception();
-    }
-
-    public override IExpr GetFoldExpr(Element/*!*/ e) {
-      //Contract.Requires(e != null);
-      Elt elt = (Elt)e;
-      if (elt.value == Value.Null) {
-        return factory.Null;
-      } else {
-        // can't fold into an expression
-        return null;
-      }
-    }
-
-    public override bool Understands(IFunctionSymbol/*!*/ f, IList/*<IExpr!>*//*!*/ args) {
-      //Contract.Requires(args != null);
-      //Contract.Requires(f != null);
-      if (f.Equals(Microsoft.AbstractInterpretationFramework.Value.Eq) ||
-          f.Equals(Microsoft.AbstractInterpretationFramework.Value.Neq)) {
-
-        Contract.Assert(args.Count == 2);
-        IExpr/*!*/ arg0 = (IExpr/*!*/)cce.NonNull(args[0]);
-        IExpr/*!*/ arg1 = (IExpr/*!*/)cce.NonNull(args[1]);
-
-        // Look for "x OP null" or "null OP x" where OP is "==" or "!=".
-        if (arg0 is IVariable && arg1 is IFunApp && ((IFunApp)arg1).FunctionSymbol == Ref.Null) {
-          return true;
-        } else if (arg1 is IVariable && arg0 is IFunApp && ((IFunApp)arg0).FunctionSymbol == Ref.Null) {
-          return true;
-        }
-      }
-      return false;
-    }
-
-    public override Element/*!*/ EvaluatePredicate(IExpr/*!*/ e) {
-      //Contract.Requires(e != null);
-      Contract.Ensures(Contract.Result<Element>() != null);
-      IFunApp nary = e as IFunApp;
-      if (nary != null) {
-        bool isEq = nary.FunctionSymbol.Equals(Microsoft.AbstractInterpretationFramework.Value.Eq);
-        if (isEq || nary.FunctionSymbol.Equals(Microsoft.AbstractInterpretationFramework.Value.Neq)) {
-          IList/*<IExpr!>*//*!*/ args = nary.Arguments;
-          Contract.Assert(args != null);
-          Contract.Assert(args.Count == 2);
-          IExpr/*!*/ arg0 = (IExpr/*!*/)cce.NonNull(args[0]);
-          IExpr/*!*/ arg1 = (IExpr/*!*/)cce.NonNull(args[1]);
-
-          // Look for "x OP null" or "null OP x" where OP is "==" or "!=".
-          IVariable var = null;
-          if (arg0 is IVariable && arg1 is IFunApp && ((IFunApp)arg1).FunctionSymbol == Ref.Null) {
-            var = (IVariable)arg0;
-          } else if (arg1 is IVariable && arg0 is IFunApp && ((IFunApp)arg0).FunctionSymbol == Ref.Null) {
-            var = (IVariable)arg1;
-          }
-
-          if (var != null) // found the pattern
-                    {
-            return isEq ? Null : NotNull;
-          }
-        }
-      }
-      return Top;
-    }
-  }
-
-#if false
-
-    public class NullnessMicroLattice : MicroLattice 
-    {
-        public override MicroLatticeElement Top { get { return NullnessLatticeElement.Top; } }
-        public override MicroLatticeElement Bottom { get { return NullnessLatticeElement.Bottom; } }
-
-
-        public override MicroLatticeElement EvaluateExpression (Expr e, LookupValue lookup)
-        {
-            if (e is LiteralExpr && ((LiteralExpr)e).Val == null)
-            {
-                return NullnessLatticeElement.Null;
-            }
-            return Top;
-        }
-
-
-        public override MicroLatticeElement EvaluatePredicate (Expr e, LookupValue lookup)
-        {
-            NAryExpr nary = e as NAryExpr;
-            if (nary != null && 
-                    (nary.Fun.FunctionName.Equals("==") || nary.Fun.FunctionName.Equals("!=")))
-            {
-                Debug.Assert(nary.Args.Length == 2);
-
-                Expr arg0 = nary.Args[0], arg1 = nary.Args[1];
-                Variable var = null;
-
-                // Look for "x OP null" or "null OP x" where OP is "==" or "!=".
-                if (arg0 is IdentifierExpr && arg1 is LiteralExpr && ((LiteralExpr)arg1).Val == null)
-                {
-                    var = ((IdentifierExpr)arg0).Decl;
-                }
-                else if (arg1 is IdentifierExpr && arg0 is LiteralExpr && ((LiteralExpr)arg0).Val == null)
-                {
-                    var = ((IdentifierExpr)arg1).Decl;
-                }
-
-                if (var != null) // found the pattern
-                {
-                    return nary.Fun.FunctionName.Equals("==") ? 
-                        NullnessLatticeElement.Null : 
-                        NullnessLatticeElement.NotNull;
-                }
-            }
-            return Top;
-        }
-    }
-
-#endif
-
-}
+//-----------------------------------------------------------------------------
+//
+// Copyright (C) Microsoft Corporation.  All Rights Reserved.
+//
+//-----------------------------------------------------------------------------
+using System.Diagnostics.Contracts;
+namespace Microsoft.AbstractInterpretationFramework {
+  using System.Collections;
+  using System.Diagnostics;
+  //using System.Compiler.Analysis;
+
+  public class NullnessLattice : MicroLattice {
+    readonly INullnessFactory/*!*/ factory;
+    [ContractInvariantMethod]
+    void ObjectInvariant() {
+      Contract.Invariant(factory != null);
+    }
+
+
+    public NullnessLattice(INullnessFactory/*!*/ factory) {
+      Contract.Requires(factory != null);
+      this.factory = factory;
+      // base();
+    }
+
+    enum Value {
+      Bottom,
+      NotNull,
+      Null,
+      MayBeNull
+    }
+
+    private class Elt : Element {
+      public Value value;
+
+      public Elt(Value v) {
+        this.value = v;
+      }
+
+      [Pure]
+      public override System.Collections.Generic.ICollection<IVariable/*!*/>/*!*/ FreeVariables() {
+        Contract.Ensures(cce.NonNullElements(Contract.Result<System.Collections.Generic.ICollection<IVariable>>()));
+        return cce.NonNull(new System.Collections.Generic.List<IVariable/*!*/>()).AsReadOnly();
+      }
+
+      public override Element/*!*/ Clone() {
+        Contract.Ensures(Contract.Result<Element>() != null);
+        return new Elt(this.value);
+      }
+    }
+
+
+    public override Element/*!*/ Top {
+      get {
+        Contract.Ensures(Contract.Result<Element>() != null);
+        return new Elt(Value.MayBeNull);
+      }
+    }
+
+    public override Element/*!*/ Bottom {
+      get {
+        Contract.Ensures(Contract.Result<Element>() != null);
+        return new Elt(Value.Bottom);
+      }
+    }
+
+    public static Element/*!*/ Null {
+      get {
+        Contract.Ensures(Contract.Result<Element>() != null);
+        return new Elt(Value.Null);
+      }
+    }
+
+    public static Element/*!*/ NotNull {
+      get {
+        Contract.Ensures(Contract.Result<Element>() != null);
+        return new Elt(Value.NotNull);
+      }
+    }
+
+    public override bool IsTop(Element/*!*/ element) {
+      //Contract.Requires(element != null);
+      Elt e = (Elt)element;
+      return e.value == Value.MayBeNull;
+    }
+
+    public override bool IsBottom(Element/*!*/ element) {
+      //Contract.Requires(element != null);
+      Elt e = (Elt)element;
+      return e.value == Value.Bottom;
+    }
+
+    public override Lattice.Element/*!*/ NontrivialJoin(Element/*!*/ first, Element/*!*/ second) {
+      //Contract.Requires(second != null);
+      //Contract.Requires(first != null);
+      Contract.Ensures(Contract.Result<Lattice.Element>() != null);
+      Elt a = (Elt)first;
+      Elt b = (Elt)second;
+      return (a.value == b.value) ? a : (Elt)Top;
+    }
+
+    public override Lattice.Element/*!*/ NontrivialMeet(Element/*!*/ first, Element/*!*/ second) {
+      //Contract.Requires(second != null);
+      //Contract.Requires(first != null);
+      Contract.Ensures(Contract.Result<Lattice.Element>() != null);
+      Elt a = (Elt)first;
+      Elt b = (Elt)second;
+      return (a.value == b.value) ? a : (Elt)Bottom;
+    }
+
+    public override Element/*!*/ Widen(Element/*!*/ first, Element/*!*/ second) {
+      //Contract.Requires(second != null);
+      //Contract.Requires(first != null);
+      Contract.Ensures(Contract.Result<Element>() != null);
+      return Join(first, second);
+    }
+
+    protected override bool AtMost(Element/*!*/ first, Element/*!*/ second) // this <= that
+    {
+      //Contract.Requires(first != null);
+      //Contract.Requires(second != null);
+      Elt a = (Elt)first;
+      Elt b = (Elt)second;
+      return a.value == b.value;
+    }
+
+    public override IExpr/*!*/ ToPredicate(IVariable/*!*/ var, Element/*!*/ element) {
+      //Contract.Requires(element != null);
+      //Contract.Requires(var != null);
+      Contract.Ensures(Contract.Result<IExpr>() != null);
+      Elt e = (Elt)element;
+
+      if (e.value == Value.NotNull) {
+        return factory.Neq(var, factory.Null);
+      }
+      if (e.value == Value.Null) {
+        return factory.Eq(var, factory.Null);
+      }
+      {
+        Contract.Assert(false);
+        throw new cce.UnreachableException();
+      }
+      throw new System.Exception();
+    }
+
+    public override IExpr GetFoldExpr(Element/*!*/ e) {
+      //Contract.Requires(e != null);
+      Elt elt = (Elt)e;
+      if (elt.value == Value.Null) {
+        return factory.Null;
+      } else {
+        // can't fold into an expression
+        return null;
+      }
+    }
+
+    public override bool Understands(IFunctionSymbol/*!*/ f, IList/*<IExpr!>*//*!*/ args) {
+      //Contract.Requires(args != null);
+      //Contract.Requires(f != null);
+      if (f.Equals(Microsoft.AbstractInterpretationFramework.Value.Eq) ||
+          f.Equals(Microsoft.AbstractInterpretationFramework.Value.Neq)) {
+
+        Contract.Assert(args.Count == 2);
+        IExpr/*!*/ arg0 = (IExpr/*!*/)cce.NonNull(args[0]);
+        IExpr/*!*/ arg1 = (IExpr/*!*/)cce.NonNull(args[1]);
+
+        // Look for "x OP null" or "null OP x" where OP is "==" or "!=".
+        if (arg0 is IVariable && arg1 is IFunApp && ((IFunApp)arg1).FunctionSymbol == Ref.Null) {
+          return true;
+        } else if (arg1 is IVariable && arg0 is IFunApp && ((IFunApp)arg0).FunctionSymbol == Ref.Null) {
+          return true;
+        }
+      }
+      return false;
+    }
+
+    public override Element/*!*/ EvaluatePredicate(IExpr/*!*/ e) {
+      //Contract.Requires(e != null);
+      Contract.Ensures(Contract.Result<Element>() != null);
+      IFunApp nary = e as IFunApp;
+      if (nary != null) {
+        bool isEq = nary.FunctionSymbol.Equals(Microsoft.AbstractInterpretationFramework.Value.Eq);
+        if (isEq || nary.FunctionSymbol.Equals(Microsoft.AbstractInterpretationFramework.Value.Neq)) {
+          IList/*<IExpr!>*//*!*/ args = nary.Arguments;
+          Contract.Assert(args != null);
+          Contract.Assert(args.Count == 2);
+          IExpr/*!*/ arg0 = (IExpr/*!*/)cce.NonNull(args[0]);
+          IExpr/*!*/ arg1 = (IExpr/*!*/)cce.NonNull(args[1]);
+
+          // Look for "x OP null" or "null OP x" where OP is "==" or "!=".
+          IVariable var = null;
+          if (arg0 is IVariable && arg1 is IFunApp && ((IFunApp)arg1).FunctionSymbol == Ref.Null) {
+            var = (IVariable)arg0;
+          } else if (arg1 is IVariable && arg0 is IFunApp && ((IFunApp)arg0).FunctionSymbol == Ref.Null) {
+            var = (IVariable)arg1;
+          }
+
+          if (var != null) // found the pattern
+                    {
+            return isEq ? Null : NotNull;
+          }
+        }
+      }
+      return Top;
+    }
+  }
+
+#if false
+
+    public class NullnessMicroLattice : MicroLattice 
+    {
+        public override MicroLatticeElement Top { get { return NullnessLatticeElement.Top; } }
+        public override MicroLatticeElement Bottom { get { return NullnessLatticeElement.Bottom; } }
+
+
+        public override MicroLatticeElement EvaluateExpression (Expr e, LookupValue lookup)
+        {
+            if (e is LiteralExpr && ((LiteralExpr)e).Val == null)
+            {
+                return NullnessLatticeElement.Null;
+            }
+            return Top;
+        }
+
+
+        public override MicroLatticeElement EvaluatePredicate (Expr e, LookupValue lookup)
+        {
+            NAryExpr nary = e as NAryExpr;
+            if (nary != null && 
+                    (nary.Fun.FunctionName.Equals("==") || nary.Fun.FunctionName.Equals("!=")))
+            {
+                Debug.Assert(nary.Args.Length == 2);
+
+                Expr arg0 = nary.Args[0], arg1 = nary.Args[1];
+                Variable var = null;
+
+                // Look for "x OP null" or "null OP x" where OP is "==" or "!=".
+                if (arg0 is IdentifierExpr && arg1 is LiteralExpr && ((LiteralExpr)arg1).Val == null)
+                {
+                    var = ((IdentifierExpr)arg0).Decl;
+                }
+                else if (arg1 is IdentifierExpr && arg0 is LiteralExpr && ((LiteralExpr)arg0).Val == null)
+                {
+                    var = ((IdentifierExpr)arg1).Decl;
+                }
+
+                if (var != null) // found the pattern
+                {
+                    return nary.Fun.FunctionName.Equals("==") ? 
+                        NullnessLatticeElement.Null : 
+                        NullnessLatticeElement.NotNull;
+                }
+            }
+            return Top;
+        }
+    }
+
+#endif
+
+}