remove Spec# leftovers

Author: shazqadeer

Source/AbstractInterpretation/Traverse.cs

@@ -118,8 +118,8 @@ public static List<Block> ComputeLoopBodyFrom(Block block)
       Contract.Assert(rootBlock == null);
       rootBlock = block;
 
-      List<Block /*!*/> blocksInLoop = new List<Block /*!*/>(); // We use a list just because .net does not define a set
-      List<Block /*!*/> visitingPath = new List<Block /*!*/>(); // The order is important, as we want paths
+      List<Block> blocksInLoop = new List<Block>(); // We use a list just because .net does not define a set
+      List<Block> visitingPath = new List<Block>(); // The order is important, as we want paths
 
       blocksInLoop.Add(block);
 

Source/BaseTypes/BigDec.cs

@@ -153,7 +153,7 @@ public override int GetHashCode()
     }
 
     [Pure]
-    public override string /*!*/ ToString()
+    public override string ToString()
     {
       Contract.Ensures(Contract.Result<string>() != null);
       return String.Format("{0}e{1}", this.mantissa.ToString(), this.exponent.ToString());

Source/BaseTypes/BigFloat.cs

@@ -213,7 +213,7 @@ public override int GetHashCode()
     }
 
     [Pure]
-    public override string /*!*/ ToString()
+    public override string ToString()
     {
       Contract.Ensures(Contract.Result<string>() != null);
       if (value == "")

Source/BaseTypes/BigNum.cs

@@ -145,7 +145,7 @@ public override int GetHashCode()
     }
 
     [Pure]
-    public override string /*!*/ ToString()
+    public override string ToString()
     {
       Contract.Ensures(Contract.Result<string>() != null);
       return Cce.NonNull(val.ToString());
@@ -158,7 +158,7 @@ public override int GetHashCode()
     // int32.ToString(format) does) 
 
     [Pure]
-    public string /*!*/ ToString(string /*!*/ format)
+    public string ToString(string format)
     {
       Contract.Requires(format != null);
       Contract.Ensures(Contract.Result<string>() != null);
@@ -185,7 +185,7 @@ public override int GetHashCode()
     private static readonly System.Numerics.BigInteger BI_2_TO_24 = new BIM(0x1000000);
 
     [Pure]
-    private string /*!*/ toHex(string /*!*/ format)
+    private string toHex(string format)
     {
       Contract.Requires(format != null);
       Contract.Ensures(Contract.Result<string>() != null);
@@ -202,7 +202,7 @@ public override int GetHashCode()
     }
 
     [Pure]
-    private int extractPrecision(string /*!*/ format)
+    private int extractPrecision(string format)
     {
       Contract.Requires(format != null);
       if (format.Length > 1)
@@ -216,7 +216,7 @@ private int extractPrecision(string /*!*/ format)
     }
 
     [Pure]
-    private string /*!*/ addMinus(int signum, string /*!*/ suffix)
+    private string addMinus(int signum, string suffix)
     {
       Contract.Requires(suffix != null);
       Contract.Ensures(Contract.Result<string>() != null);
@@ -229,7 +229,7 @@ private int extractPrecision(string /*!*/ format)
     }
 
     [Pure]
-    private string /*!*/ prefixWithZeros(int minLength, string /*!*/ suffix)
+    private string prefixWithZeros(int minLength, string suffix)
     {
       Contract.Requires(suffix != null);
       Contract.Ensures(Contract.Result<string>() != null);

Source/BaseTypes/Rational.cs

@@ -129,7 +129,7 @@ public BigNum Denominator
       get { return denominator == BigNum.ZERO ? BigNum.ONE : denominator; }
     }
 
-    public override string /*!*/ ToString()
+    public override string ToString()
     {
       Contract.Ensures(Contract.Result<string>() != null);
       return String.Format("{0}/{1}", Numerator, Denominator);

Source/BaseTypes/RoundingMode.cs

@@ -67,7 +67,7 @@ public override int GetHashCode()
     }
 
     [Pure]
-    public override string /*!*/ ToString()
+    public override string ToString()
     {
       Contract.Ensures(Contract.Result<string>() != null);
       return val;

Source/BaseTypes/Set.cs

@@ -30,7 +30,7 @@ public GSet()
       //:base();
     }
 
-    private GSet(Dictionary<T, int> /*!*/ ht, List<T> arr)
+    private GSet(Dictionary<T, int> ht, List<T> arr)
     {
       Contract.Requires(ht != null);
       Contract.Requires(arr != null);
@@ -47,7 +47,7 @@ public GSet(int capacity)
     }
 
 
-    public readonly static GSet<T> /*!*/
+    public readonly static GSet<T>
       Empty = new GSet<T>();
 
     public void Clear()
@@ -146,7 +146,7 @@ public T Take()
       return r;
     }
 
-    public void Intersect(GSet<T> /*!*/ s)
+    public void Intersect(GSet<T> s)
     {
       Contract.Requires(s != null);
       if (s == this)
@@ -222,7 +222,7 @@ public bool ContainsRange(IEnumerable<T> s)
       return true;
     }
 
-    public object /*!*/ Clone()
+    public object Clone()
     {
       Contract.Ensures(Contract.Result<object>() != null);
       return new GSet<T>(new Dictionary<T, int>(ht), new List<T>(arr));
@@ -234,11 +234,11 @@ public virtual int Count
     }
 
     [Pure]
-    public override string /*!*/ ToString()
+    public override string ToString()
     {
       Contract.Ensures(Contract.Result<string>() != null);
       string s = null;
-      foreach (object /*!*/ key in ht.Keys)
+      foreach (object key in ht.Keys)
       {
         Contract.Assert(key != null);
         if (s == null)
@@ -266,34 +266,33 @@ public virtual int Count
     //----------------------------- Static Methods ---------------------------------
 
     // Functional Intersect
-    public static GSet<T> /*!*/ Intersect(GSet<T> /*!*/ a, GSet<T> /*!*/ b)
+    public static GSet<T> Intersect(GSet<T> a, GSet<T> b)
     {
       Contract.Requires(b != null);
       Contract.Requires(a != null);
       Contract.Ensures(Contract.Result<GSet<T>>() != null);
-      //Contract.Ensures(Contract.ForAll(result, x => a[x] && b[x] ));
-      GSet<T> /*!*/
-        res = (GSet<T> /*!*/) Cce.NonNull(a.Clone());
+      GSet<T>
+        res = (GSet<T>) Cce.NonNull(a.Clone());
       res.Intersect(b);
       return res;
     }
 
     // Functional Union
-    public static GSet<T> /*!*/ Union(GSet<T> /*!*/ a, GSet<T> /*!*/ b)
+    public static GSet<T> Union(GSet<T> a, GSet<T> b)
     {
       Contract.Requires(a != null);
       Contract.Requires(b != null);
       Contract.Ensures(Contract.Result<GSet<T>>() != null);
       //  Contract.Ensures(Contract.ForAll(result, x => a[x] || b[x] ));
-      GSet<T> /*!*/
-        res = (GSet<T> /*!*/) Cce.NonNull(a.Clone());
+      GSet<T>
+        res = (GSet<T>) Cce.NonNull(a.Clone());
       res.AddRange(b);
       return res;
     }
 
-    public delegate bool SetFilter(object /*!*/ obj);
+    public delegate bool SetFilter(object obj);
 
-    public static GSet<T> /*!*/ Filter(GSet<T> /*!*/ a, Func<T, bool> filter)
+    public static GSet<T> Filter(GSet<T> a, Func<T, bool> filter)
     {
       Contract.Requires(filter != null);
       Contract.Requires(a != null);

Source/Concurrency/CivlUtil.cs

@@ -306,7 +306,7 @@ public static HavocCmd HavocCmd(params IdentifierExpr[] vars)
 
   public static class BlockHelper
   {
-    public static readonly IToken /*!*/ ReportedNoToken = new Token();
+    public static readonly IToken ReportedNoToken = new Token();
 
     public static Block Block(string label, List<Cmd> cmds)
     {