Merge pull request #470 from tom-englert/SyncR#

Add missing contracts found when aligning CC with R#

Microsoft.Research/Contracts/MsCorlib/System.ActivationContext.cs

@@ -58,15 +58,17 @@ private ActivationContext ()
 
     public static System.ActivationContext CreatePartialActivationContext (ApplicationIdentity identity)
     {
+      Contract.Requires(identity != null);
       Contract.Ensures (Contract.Result<System.ActivationContext>() != null);
 
       return default(System.ActivationContext);
     }
 
     public static System.ActivationContext CreatePartialActivationContext (ApplicationIdentity identity, string[] manifestPaths)
     {
+      Contract.Requires(identity != null);
+      Contract.Requires(manifestPaths != null);
       Contract.Ensures (Contract.Result<System.ActivationContext>() != null);
-      Contract.Ensures (manifestPaths.Length >= 0);
 
       return default(System.ActivationContext);
     }

Microsoft.Research/Contracts/MsCorlib/System.Collections.ArrayList.cs

@@ -60,7 +60,7 @@ public virtual object[] ToArray()
     public static ArrayList Synchronized(ArrayList list)
     {
       Contract.Requires(list != null);
-      //Contract.Ensures(result.IsSynchronized);
+      Contract.Ensures(Contract.Result<ArrayList>() != null);
 
       return default(ArrayList);
     }
@@ -138,17 +138,16 @@ public virtual void RemoveRange(int index, int count)
     public static ArrayList ReadOnly(ArrayList list)
     {
       Contract.Requires(list != null);
+      Contract.Ensures(Contract.Result<ArrayList>() != null);
       Contract.Ensures(Contract.Result<ArrayList>().IsReadOnly);
 
-      Contract.Ensures(Contract.Result<ArrayList>() != null);
       return default(ArrayList);
     }
     public static IList ReadOnly(IList list)
     {
       Contract.Requires(list != null);
-      Contract.Ensures(Contract.Result<IList>().IsReadOnly);
-
       Contract.Ensures(Contract.Result<IList>() != null);
+      Contract.Ensures(Contract.Result<IList>().IsReadOnly);
       return default(IList);
     }
     [Pure]
@@ -222,13 +221,15 @@ public virtual IEnumerator GetEnumerator(int index, int count)
     public static ArrayList FixedSize(ArrayList list)
     {
       Contract.Requires(list != null);
+      Contract.Ensures(Contract.Result<ArrayList>() != null);
       Contract.Ensures(Contract.Result<ArrayList>().IsFixedSize);
 
       return default(ArrayList);
     }
     public static IList FixedSize(IList list)
     {
       Contract.Requires(list != null);
+      Contract.Ensures(Contract.Result<ArrayList>() != null);
       Contract.Ensures(Contract.Result<IList>().IsFixedSize);
 
       return default(IList);
@@ -293,6 +294,7 @@ public virtual void AddRange(ICollection c)
     public static ArrayList Adapter(IList list)
     {
       Contract.Requires(list != null);
+      Contract.Ensures(Contract.Result<ArrayList>() != null);
 
       return default(ArrayList);
     }

Microsoft.Research/Contracts/MsCorlib/System.Collections.BitArray.cs

@@ -57,20 +57,23 @@ extern public virtual int Count
     public BitArray Xor(BitArray value)
     {
       Contract.Requires(value != null);
+      Contract.Ensures(Contract.Result<BitArray>() != null);
 
       return default(BitArray);
     }
 
     public BitArray Or(BitArray value)
     {
       Contract.Requires(value != null);
+      Contract.Ensures(Contract.Result<BitArray>() != null);
 
       return default(BitArray);
     }
 
     public BitArray And(BitArray value)
     {
       Contract.Requires(value != null);
+      Contract.Ensures(Contract.Result<BitArray>() != null);
 
       return default(BitArray);
     }

Microsoft.Research/Contracts/MsCorlib/System.Collections.SortedList.cs

@@ -91,6 +91,7 @@ public virtual void TrimToSize()
     public static SortedList Synchronized(SortedList list)
     {
       Contract.Requires(list != null);
+      Contract.Ensures(Contract.Result<SortedList>() != null);
 
       return default(SortedList);
     }

Microsoft.Research/Contracts/MsCorlib/System.Enum.cs

@@ -23,13 +23,18 @@ public abstract class Enum
     [Pure]
     public static string Format(Type enumType, object value, string format)
     {
+      Contract.Requires(enumType != null);
+      Contract.Requires(value != null);
+      Contract.Requires(format != null);
       Contract.Ensures(Contract.Result<string>() != null);
       return default(string);   
     }
 #endif
     [Pure]
     public static string GetName(Type enumType, object value)
     {
+      Contract.Requires(enumType != null);
+      Contract.Requires(value != null);
       Contract.Ensures(Contract.Result<string>() != null);
       return default(string);
     }
@@ -38,6 +43,7 @@ public static string GetName(Type enumType, object value)
     [Pure]
     public static string[] GetNames(Type enumType)
     {
+      Contract.Requires(enumType != null);
       Contract.Ensures(Contract.Result<string[]>() != null);
       return default(string[]);
     }
@@ -92,6 +98,7 @@ public static object Parse(Type enumType, string value, bool ignoreCase)
     [Pure]
     public static Type GetUnderlyingType(Type enumType)
     {
+      Contract.Requires(enumType != null);
       Contract.Ensures(Contract.Result<Type>() != null);
       return default(Type);
     }
@@ -121,6 +128,7 @@ public static Type GetUnderlyingType(Type enumType)
     [Pure]
     public static Array GetValues(Type enumType)
     {
+      Contract.Requires(enumType != null);
       Contract.Ensures(Contract.Result<Array>() != null);
       return default(Array);
     }
@@ -151,6 +159,7 @@ public static Array GetValues(Type enumType)
     [Pure]
     public static object ToObject(Type enumType, byte value)
     {
+      Contract.Requires(enumType != null);
       Contract.Ensures(Contract.Result<object>() != null);
       return default(object);
     }
@@ -179,6 +188,7 @@ public static object ToObject(Type enumType, int value)
       //
       //   System.ArgumentException:
       //     enumType is not an System.Enum.
+      Contract.Requires(enumType != null);
       Contract.Ensures(Contract.Result<object>() != null);
       return default(object);
     }
@@ -208,31 +218,37 @@ public static object ToObject(Type enumType, long value)
       //     enumType is not an System.Enum.-or- value is not type System.SByte, System.Int16,
       //     System.Int32, System.Int64, System.Byte, System.UInt16, System.UInt32, or
       //     System.UInt64.
+      Contract.Requires(enumType != null);
       Contract.Ensures(Contract.Result<object>() != null);
       return default(object);
     }
 #endif
     [Pure]
     public static object ToObject(Type enumType, object value)
     {
+      Contract.Requires(enumType != null);
       Contract.Ensures(Contract.Result<object>() != null);
       return default(object);
     }
 #if !SILVERLIGHT
     [Pure]
     public static object ToObject(Type enumType, sbyte value)
     {
+      Contract.Requires(enumType != null);
+      Contract.Ensures(Contract.Result<object>() != null);
       return default(object);
     }
     [Pure]
     public static object ToObject(Type enumType, short value)
     {
+      Contract.Requires(enumType != null);
       Contract.Ensures(Contract.Result<object>() != null);
       return default(object);
     }
     [Pure]
     public static object ToObject(Type enumType, uint value)
     {
+      Contract.Requires(enumType != null);
       Contract.Ensures(Contract.Result<object>() != null);
       return default(object);
     }
@@ -242,6 +258,7 @@ public static object ToObject(Type enumType, uint value)
     [Pure]
     public static object ToObject(Type enumType, ulong value)
     {
+      Contract.Requires(enumType != null);
       Contract.Ensures(Contract.Result<object>() != null);
       return default(object);
     }
@@ -271,6 +288,7 @@ public static object ToObject(Type enumType, ulong value)
     [Pure]
     public static object ToObject(Type enumType, ushort value)
     {
+      Contract.Requires(enumType != null);
       Contract.Ensures(Contract.Result<object>() != null);
       return default(object);
     }

Microsoft.Research/Contracts/MsCorlib/System.Globalization.CultureInfo.cs

@@ -229,6 +229,8 @@ extern public bool IsReadOnly
     public static CultureInfo ReadOnly(CultureInfo ci)
     {
       Contract.Requires(ci != null);
+      Contract.Ensures(Contract.Result<CultureInfo>() != null);
+      Contract.Ensures(Contract.Result<CultureInfo>().IsReadOnly);
 
       return default(CultureInfo);
     }

Microsoft.Research/Contracts/MsCorlib/System.Globalization.DateTimeFormatInfo.cs

@@ -313,6 +313,8 @@ extern public bool IsReadOnly
     public static DateTimeFormatInfo ReadOnly(DateTimeFormatInfo dtfi)
     {
       Contract.Requires(dtfi != null);
+      Contract.Ensures(Contract.Result<DateTimeFormatInfo>() != null);
+      Contract.Ensures(Contract.Result<DateTimeFormatInfo>().IsReadOnly);
 
       return default(DateTimeFormatInfo);
     }

Microsoft.Research/Contracts/MsCorlib/System.Reflection.MethodInfo.cs

@@ -143,6 +143,7 @@ public virtual MethodInfo GetGenericMethodDefinition()
     //     This method is not supported.
     public virtual MethodInfo MakeGenericMethod(params Type[] typeArguments)
     {
+      Contract.Requires(typeArguments != null);
       Contract.Ensures(Contract.Result<MethodInfo>() != null);
       return default(MethodInfo);
     }

Microsoft.Research/Contracts/MsCorlib/System.Runtime.InteropServices.Marshal.cs

@@ -188,6 +188,7 @@ public static int GetComSlotForMethodInfo(MemberInfo m) {
     public static Delegate GetDelegateForFunctionPointer(IntPtr ptr, Type t) {
       Contract.Requires(ptr != IntPtr.Zero);
       Contract.Requires(t != null);
+      Contract.Ensures(Contract.Result<Delegate>() != null);
       return default(Delegate);
     }
     public static int GetEndComSlot(Type t) {

Microsoft.Research/Contracts/MsCorlib/System.String.cs

@@ -187,6 +187,7 @@ public static String Concat<T>(IEnumerable<T> args)
     public static String Copy(String str)
     {
       Contract.Requires(str != null);
+      Contract.Ensures(Contract.Result<String>() != null);
 
       return default(String);
     }

Microsoft.Research/Contracts/MsCorlib/System.Type.cs

@@ -267,6 +267,7 @@ public virtual Type MakeByRefType()
     public virtual Type MakeGenericType(params Type[] typeArguments)
     {
       Contract.Requires(this.IsGenericTypeDefinition);
+      Contract.Requires(typeArguments != null);
       Contract.Requires(typeArguments.Length == this.GetGenericArguments().Length);
       Contract.Ensures(Contract.Result<Type>() != null);
 

Microsoft.Research/Contracts/PresentationCore/Sources/System.Windows.Media.Media3D.Visual3D.cs

@@ -139,16 +139,19 @@ int System.Windows.Media.Composition.DUCE.IResource.GetChannelCount()
 
     public GeneralTransform3D TransformToAncestor(Visual3D ancestor)
     {
+      Contract.Requires(ancestor != null);
       return default(GeneralTransform3D);
     }
 
     public GeneralTransform3DTo2D TransformToAncestor(System.Windows.Media.Visual ancestor)
     {
+      Contract.Requires(ancestor != null);
       return default(GeneralTransform3DTo2D);
     }
 
     public GeneralTransform3D TransformToDescendant(Visual3D descendant)
     {
+      Contract.Requires(descendant != null);
       return default(GeneralTransform3D);
     }
 

Microsoft.Research/Contracts/PresentationCore/Sources/System.Windows.Media.Visual.cs

@@ -105,24 +105,27 @@ int System.Windows.Media.Composition.DUCE.IResource.GetChannelCount()
 
     public GeneralTransform TransformToAncestor(System.Windows.Media.Visual ancestor)
     {
+      Contract.Requires(ancestor != null);
       Contract.Ensures(Contract.Result<GeneralTransform>() != null);
       return default(GeneralTransform);
     }
 
     public System.Windows.Media.Media3D.GeneralTransform2DTo3D TransformToAncestor(System.Windows.Media.Media3D.Visual3D ancestor)
     {
-      Contract.Ensures(Contract.Result<GeneralTransform2DTo3D>() != null);
+      Contract.Requires(ancestor != null);
       return default(System.Windows.Media.Media3D.GeneralTransform2DTo3D);
     }
 
     public GeneralTransform TransformToDescendant(System.Windows.Media.Visual descendant)
     {
+      Contract.Requires(descendant != null);
       Contract.Ensures(Contract.Result<GeneralTransform>() != null);
       return default(GeneralTransform);
     }
 
     public GeneralTransform TransformToVisual(System.Windows.Media.Visual visual)
     {
+      Contract.Requires(visual != null);
       Contract.Ensures(Contract.Result<GeneralTransform>() != null);
       return default(GeneralTransform);
     }

Microsoft.Research/Contracts/PresentationCore/Sources/System.Windows.Media.VisualTreeHelper.cs

@@ -191,13 +191,15 @@ public static DoubleCollection GetYSnappingGuidelines(Visual reference)
     public static void HitTest(System.Windows.Media.Media3D.Visual3D reference, HitTestFilterCallback filterCallback, HitTestResultCallback resultCallback, System.Windows.Media.Media3D.HitTestParameters3D hitTestParameters)
     {
       Contract.Requires(reference != null);
-
+      Contract.Requires(resultCallback != null);
+      Contract.Requires(hitTestParameters != null);
     }
 
     public static void HitTest(Visual reference, HitTestFilterCallback filterCallback, HitTestResultCallback resultCallback, HitTestParameters hitTestParameters)
     {
       Contract.Requires(reference != null);
-
+      Contract.Requires(resultCallback != null);
+      Contract.Requires(hitTestParameters != null);
     }
 
     public static HitTestResult HitTest(Visual reference, System.Windows.Point point)

Microsoft.Research/Contracts/PresentationFramework/Sources/System.Windows.Controls.DataGrid.cs

@@ -92,6 +92,7 @@ public DataGrid()
 
     public static System.Collections.ObjectModel.Collection<DataGridColumn> GenerateColumns(System.ComponentModel.IItemProperties itemProperties)
     {
+      Contract.Requires(itemProperties != null);
       Contract.Ensures(Contract.Result<System.Collections.ObjectModel.Collection<System.Windows.Controls.DataGridColumn>>() != null);
 
       return default(System.Collections.ObjectModel.Collection<DataGridColumn>);

Microsoft.Research/Contracts/PresentationFramework/Sources/System.Windows.Controls.InkCanvas.cs

@@ -340,6 +340,7 @@ public System.Windows.Ink.StylusShape EraserShape
       }
       set
       {
+        Contract.Requires(value != null);
       }
     }
 

Microsoft.Research/Contracts/PresentationFramework/Sources/System.Windows.Documents.Serialization.SerializerDescriptor.cs

@@ -43,6 +43,7 @@ sealed public partial class SerializerDescriptor
     #region Methods and constructors
     public static SerializerDescriptor CreateFromFactoryInstance(ISerializerFactory factoryInstance)
     {
+      Contract.Requires(factoryInstance != null);
       Contract.Ensures(!string.IsNullOrEmpty(factoryInstance.GetType().FullName));
       Contract.Ensures(Contract.Result<System.Windows.Documents.Serialization.SerializerDescriptor>() != null);
       Contract.Ensures(factoryInstance.GetType().Assembly != null);

Microsoft.Research/Contracts/PresentationFramework/Sources/System.Windows.Documents.TextEffectResolver.cs

@@ -43,7 +43,9 @@ static public partial class TextEffectResolver
     #region Methods and constructors
     public static TextEffectTarget[] Resolve(TextPointer startPosition, TextPointer endPosition, System.Windows.Media.TextEffect effect)
     {
+      Contract.Requires(startPosition != null);
       Contract.Requires(endPosition != null);
+      Contract.Requires(effect != null);
       Contract.Ensures(Contract.Result<System.Windows.Documents.TextEffectTarget[]>() != null);
 
       return default(TextEffectTarget[]);