diff --git a/Microsoft.Research/Contracts/MsCorlib/System.ActivationContext.cs b/Microsoft.Research/Contracts/MsCorlib/System.ActivationContext.cs index bae65c57..075265cd 100644 --- a/Microsoft.Research/Contracts/MsCorlib/System.ActivationContext.cs +++ b/Microsoft.Research/Contracts/MsCorlib/System.ActivationContext.cs @@ -58,6 +58,7 @@ private ActivationContext () public static System.ActivationContext CreatePartialActivationContext (ApplicationIdentity identity) { + Contract.Requires(identity != null); Contract.Ensures (Contract.Result() != null); return default(System.ActivationContext); @@ -65,8 +66,9 @@ public static System.ActivationContext CreatePartialActivationContext (Applicati public static System.ActivationContext CreatePartialActivationContext (ApplicationIdentity identity, string[] manifestPaths) { + Contract.Requires(identity != null); + Contract.Requires(manifestPaths != null); Contract.Ensures (Contract.Result() != null); - Contract.Ensures (manifestPaths.Length >= 0); return default(System.ActivationContext); } diff --git a/Microsoft.Research/Contracts/MsCorlib/System.Collections.ArrayList.cs b/Microsoft.Research/Contracts/MsCorlib/System.Collections.ArrayList.cs index c489bb0a..82e33668 100644 --- a/Microsoft.Research/Contracts/MsCorlib/System.Collections.ArrayList.cs +++ b/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() != 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() != null); Contract.Ensures(Contract.Result().IsReadOnly); - Contract.Ensures(Contract.Result() != null); return default(ArrayList); } public static IList ReadOnly(IList list) { Contract.Requires(list != null); - Contract.Ensures(Contract.Result().IsReadOnly); - Contract.Ensures(Contract.Result() != null); + Contract.Ensures(Contract.Result().IsReadOnly); return default(IList); } [Pure] @@ -222,6 +221,7 @@ public virtual IEnumerator GetEnumerator(int index, int count) public static ArrayList FixedSize(ArrayList list) { Contract.Requires(list != null); + Contract.Ensures(Contract.Result() != null); Contract.Ensures(Contract.Result().IsFixedSize); return default(ArrayList); @@ -229,6 +229,7 @@ public static ArrayList FixedSize(ArrayList list) public static IList FixedSize(IList list) { Contract.Requires(list != null); + Contract.Ensures(Contract.Result() != null); Contract.Ensures(Contract.Result().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() != null); return default(ArrayList); } diff --git a/Microsoft.Research/Contracts/MsCorlib/System.Collections.BitArray.cs b/Microsoft.Research/Contracts/MsCorlib/System.Collections.BitArray.cs index 39b657b3..6d9bea5c 100644 --- a/Microsoft.Research/Contracts/MsCorlib/System.Collections.BitArray.cs +++ b/Microsoft.Research/Contracts/MsCorlib/System.Collections.BitArray.cs @@ -57,6 +57,7 @@ extern public virtual int Count public BitArray Xor(BitArray value) { Contract.Requires(value != null); + Contract.Ensures(Contract.Result() != null); return default(BitArray); } @@ -64,6 +65,7 @@ public BitArray Xor(BitArray value) public BitArray Or(BitArray value) { Contract.Requires(value != null); + Contract.Ensures(Contract.Result() != null); return default(BitArray); } @@ -71,6 +73,7 @@ public BitArray Or(BitArray value) public BitArray And(BitArray value) { Contract.Requires(value != null); + Contract.Ensures(Contract.Result() != null); return default(BitArray); } diff --git a/Microsoft.Research/Contracts/MsCorlib/System.Collections.SortedList.cs b/Microsoft.Research/Contracts/MsCorlib/System.Collections.SortedList.cs index 8746583c..95431946 100644 --- a/Microsoft.Research/Contracts/MsCorlib/System.Collections.SortedList.cs +++ b/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() != null); return default(SortedList); } diff --git a/Microsoft.Research/Contracts/MsCorlib/System.Enum.cs b/Microsoft.Research/Contracts/MsCorlib/System.Enum.cs index 88f3e4f0..8e62b764 100644 --- a/Microsoft.Research/Contracts/MsCorlib/System.Enum.cs +++ b/Microsoft.Research/Contracts/MsCorlib/System.Enum.cs @@ -23,6 +23,9 @@ 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() != null); return default(string); } @@ -30,6 +33,8 @@ public static string Format(Type enumType, object value, string format) [Pure] public static string GetName(Type enumType, object value) { + Contract.Requires(enumType != null); + Contract.Requires(value != null); Contract.Ensures(Contract.Result() != 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() != 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() != 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() != 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() != 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() != null); return default(object); } @@ -208,6 +218,7 @@ 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() != null); return default(object); } @@ -215,6 +226,7 @@ public static object ToObject(Type enumType, long value) [Pure] public static object ToObject(Type enumType, object value) { + Contract.Requires(enumType != null); Contract.Ensures(Contract.Result() != null); return default(object); } @@ -222,17 +234,21 @@ public static object ToObject(Type enumType, object value) [Pure] public static object ToObject(Type enumType, sbyte value) { + Contract.Requires(enumType != null); + Contract.Ensures(Contract.Result() != null); return default(object); } [Pure] public static object ToObject(Type enumType, short value) { + Contract.Requires(enumType != null); Contract.Ensures(Contract.Result() != null); return default(object); } [Pure] public static object ToObject(Type enumType, uint value) { + Contract.Requires(enumType != null); Contract.Ensures(Contract.Result() != 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() != 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() != null); return default(object); } diff --git a/Microsoft.Research/Contracts/MsCorlib/System.Globalization.CultureInfo.cs b/Microsoft.Research/Contracts/MsCorlib/System.Globalization.CultureInfo.cs index 8b90ebc9..6eb692df 100644 --- a/Microsoft.Research/Contracts/MsCorlib/System.Globalization.CultureInfo.cs +++ b/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() != null); + Contract.Ensures(Contract.Result().IsReadOnly); return default(CultureInfo); } diff --git a/Microsoft.Research/Contracts/MsCorlib/System.Globalization.DateTimeFormatInfo.cs b/Microsoft.Research/Contracts/MsCorlib/System.Globalization.DateTimeFormatInfo.cs index a8d7c93d..f80f174d 100644 --- a/Microsoft.Research/Contracts/MsCorlib/System.Globalization.DateTimeFormatInfo.cs +++ b/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() != null); + Contract.Ensures(Contract.Result().IsReadOnly); return default(DateTimeFormatInfo); } diff --git a/Microsoft.Research/Contracts/MsCorlib/System.Reflection.MethodInfo.cs b/Microsoft.Research/Contracts/MsCorlib/System.Reflection.MethodInfo.cs index adaf9d74..6e9818a3 100644 --- a/Microsoft.Research/Contracts/MsCorlib/System.Reflection.MethodInfo.cs +++ b/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() != null); return default(MethodInfo); } diff --git a/Microsoft.Research/Contracts/MsCorlib/System.Runtime.InteropServices.Marshal.cs b/Microsoft.Research/Contracts/MsCorlib/System.Runtime.InteropServices.Marshal.cs index 68380dd8..9500a92c 100644 --- a/Microsoft.Research/Contracts/MsCorlib/System.Runtime.InteropServices.Marshal.cs +++ b/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() != null); return default(Delegate); } public static int GetEndComSlot(Type t) { diff --git a/Microsoft.Research/Contracts/MsCorlib/System.String.cs b/Microsoft.Research/Contracts/MsCorlib/System.String.cs index 49d7b0e2..21a9f1f0 100644 --- a/Microsoft.Research/Contracts/MsCorlib/System.String.cs +++ b/Microsoft.Research/Contracts/MsCorlib/System.String.cs @@ -187,6 +187,7 @@ public static String Concat(IEnumerable args) public static String Copy(String str) { Contract.Requires(str != null); + Contract.Ensures(Contract.Result() != null); return default(String); } diff --git a/Microsoft.Research/Contracts/MsCorlib/System.Type.cs b/Microsoft.Research/Contracts/MsCorlib/System.Type.cs index 74cb325a..2af0a3db 100644 --- a/Microsoft.Research/Contracts/MsCorlib/System.Type.cs +++ b/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() != null); diff --git a/Microsoft.Research/Contracts/PresentationCore/Sources/System.Windows.Media.Media3D.Visual3D.cs b/Microsoft.Research/Contracts/PresentationCore/Sources/System.Windows.Media.Media3D.Visual3D.cs index f5a7483c..ebb71f90 100644 --- a/Microsoft.Research/Contracts/PresentationCore/Sources/System.Windows.Media.Media3D.Visual3D.cs +++ b/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); } diff --git a/Microsoft.Research/Contracts/PresentationCore/Sources/System.Windows.Media.Visual.cs b/Microsoft.Research/Contracts/PresentationCore/Sources/System.Windows.Media.Visual.cs index af92f926..dc4bb1bb 100644 --- a/Microsoft.Research/Contracts/PresentationCore/Sources/System.Windows.Media.Visual.cs +++ b/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() != null); return default(GeneralTransform); } public System.Windows.Media.Media3D.GeneralTransform2DTo3D TransformToAncestor(System.Windows.Media.Media3D.Visual3D ancestor) { - Contract.Ensures(Contract.Result() != 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() != null); return default(GeneralTransform); } public GeneralTransform TransformToVisual(System.Windows.Media.Visual visual) { + Contract.Requires(visual != null); Contract.Ensures(Contract.Result() != null); return default(GeneralTransform); } diff --git a/Microsoft.Research/Contracts/PresentationCore/Sources/System.Windows.Media.VisualTreeHelper.cs b/Microsoft.Research/Contracts/PresentationCore/Sources/System.Windows.Media.VisualTreeHelper.cs index 673ccfce..6245edd0 100644 --- a/Microsoft.Research/Contracts/PresentationCore/Sources/System.Windows.Media.VisualTreeHelper.cs +++ b/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) diff --git a/Microsoft.Research/Contracts/PresentationFramework/Sources/System.Windows.Controls.DataGrid.cs b/Microsoft.Research/Contracts/PresentationFramework/Sources/System.Windows.Controls.DataGrid.cs index f6072106..3f3a13e7 100644 --- a/Microsoft.Research/Contracts/PresentationFramework/Sources/System.Windows.Controls.DataGrid.cs +++ b/Microsoft.Research/Contracts/PresentationFramework/Sources/System.Windows.Controls.DataGrid.cs @@ -92,6 +92,7 @@ public DataGrid() public static System.Collections.ObjectModel.Collection GenerateColumns(System.ComponentModel.IItemProperties itemProperties) { + Contract.Requires(itemProperties != null); Contract.Ensures(Contract.Result>() != null); return default(System.Collections.ObjectModel.Collection); diff --git a/Microsoft.Research/Contracts/PresentationFramework/Sources/System.Windows.Controls.InkCanvas.cs b/Microsoft.Research/Contracts/PresentationFramework/Sources/System.Windows.Controls.InkCanvas.cs index b2591b54..84afa613 100644 --- a/Microsoft.Research/Contracts/PresentationFramework/Sources/System.Windows.Controls.InkCanvas.cs +++ b/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); } } diff --git a/Microsoft.Research/Contracts/PresentationFramework/Sources/System.Windows.Documents.Serialization.SerializerDescriptor.cs b/Microsoft.Research/Contracts/PresentationFramework/Sources/System.Windows.Documents.Serialization.SerializerDescriptor.cs index f40e0a46..7d3ac795 100644 --- a/Microsoft.Research/Contracts/PresentationFramework/Sources/System.Windows.Documents.Serialization.SerializerDescriptor.cs +++ b/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() != null); Contract.Ensures(factoryInstance.GetType().Assembly != null); diff --git a/Microsoft.Research/Contracts/PresentationFramework/Sources/System.Windows.Documents.TextEffectResolver.cs b/Microsoft.Research/Contracts/PresentationFramework/Sources/System.Windows.Documents.TextEffectResolver.cs index 2a6fe2ad..94d38e96 100644 --- a/Microsoft.Research/Contracts/PresentationFramework/Sources/System.Windows.Documents.TextEffectResolver.cs +++ b/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() != null); return default(TextEffectTarget[]); diff --git a/Microsoft.Research/Contracts/PresentationFramework/Sources/System.Windows.LogicalTreeHelper.cs b/Microsoft.Research/Contracts/PresentationFramework/Sources/System.Windows.LogicalTreeHelper.cs index a307dc83..b9425d0a 100644 --- a/Microsoft.Research/Contracts/PresentationFramework/Sources/System.Windows.LogicalTreeHelper.cs +++ b/Microsoft.Research/Contracts/PresentationFramework/Sources/System.Windows.LogicalTreeHelper.cs @@ -43,15 +43,19 @@ static public partial class LogicalTreeHelper #region Methods and constructors public static void BringIntoView(DependencyObject current) { + Contract.Requires(current != null); } public static DependencyObject FindLogicalNode(DependencyObject logicalTreeNode, string elementName) { + Contract.Requires(logicalTreeNode != null); + Contract.Requires(!string.IsNullOrEmpty(elementName)); return default(DependencyObject); } public static System.Collections.IEnumerable GetChildren(FrameworkContentElement current) { + Contract.Requires(current != null); Contract.Ensures(Contract.Result() != null); return default(System.Collections.IEnumerable); @@ -59,6 +63,7 @@ public static System.Collections.IEnumerable GetChildren(FrameworkContentElement public static System.Collections.IEnumerable GetChildren(DependencyObject current) { + Contract.Requires(current != null); Contract.Ensures(Contract.Result() != null); return default(System.Collections.IEnumerable); @@ -66,6 +71,7 @@ public static System.Collections.IEnumerable GetChildren(DependencyObject curren public static System.Collections.IEnumerable GetChildren(FrameworkElement current) { + Contract.Requires(current != null); Contract.Ensures(Contract.Result() != null); return default(System.Collections.IEnumerable); @@ -73,6 +79,7 @@ public static System.Collections.IEnumerable GetChildren(FrameworkElement curren public static DependencyObject GetParent(DependencyObject current) { + Contract.Requires(current != null); return default(DependencyObject); } #endregion diff --git a/Microsoft.Research/Contracts/PresentationFramework/Sources/System.Windows.Markup.ParserContext.cs b/Microsoft.Research/Contracts/PresentationFramework/Sources/System.Windows.Markup.ParserContext.cs index 31359a9f..2486b547 100644 --- a/Microsoft.Research/Contracts/PresentationFramework/Sources/System.Windows.Markup.ParserContext.cs +++ b/Microsoft.Research/Contracts/PresentationFramework/Sources/System.Windows.Markup.ParserContext.cs @@ -47,10 +47,12 @@ public ParserContext() public ParserContext(System.Xml.XmlParserContext xmlParserContext) { + Contract.Requires(xmlParserContext != null); } public static implicit operator System.Xml.XmlParserContext(System.Windows.Markup.ParserContext parserContext) { + Contract.Requires(parserContext != null); Contract.Ensures(0 <= parserContext.XmlLang.Length); Contract.Ensures(Contract.Result() != null); @@ -59,6 +61,7 @@ public static implicit operator System.Xml.XmlParserContext(System.Windows.Marku public static System.Xml.XmlParserContext ToXmlParserContext(System.Windows.Markup.ParserContext parserContext) { + Contract.Requires(parserContext != null); Contract.Ensures(Contract.Result() != null); return default(System.Xml.XmlParserContext); diff --git a/Microsoft.Research/Contracts/System.ComponentModel.Composition/Sources/System.ComponentModel.Composition.Hosting.CompositionBatch.cs b/Microsoft.Research/Contracts/System.ComponentModel.Composition/Sources/System.ComponentModel.Composition.Hosting.CompositionBatch.cs index 65558efb..5097b5e0 100644 --- a/Microsoft.Research/Contracts/System.ComponentModel.Composition/Sources/System.ComponentModel.Composition.Hosting.CompositionBatch.cs +++ b/Microsoft.Research/Contracts/System.ComponentModel.Composition/Sources/System.ComponentModel.Composition.Hosting.CompositionBatch.cs @@ -45,6 +45,7 @@ public partial class CompositionBatch #region Methods and constructors public System.ComponentModel.Composition.Primitives.ComposablePart AddExport(System.ComponentModel.Composition.Primitives.Export export) { + Contract.Requires(export != null); Contract.Ensures(Contract.Result() != null); return default(System.ComponentModel.Composition.Primitives.ComposablePart); diff --git a/Microsoft.Research/Contracts/System.DirectoryServices/Sources/System.DirectoryServices.ActiveDirectory.DomainController.cs b/Microsoft.Research/Contracts/System.DirectoryServices/Sources/System.DirectoryServices.ActiveDirectory.DomainController.cs index c1120031..dbd2a145 100644 --- a/Microsoft.Research/Contracts/System.DirectoryServices/Sources/System.DirectoryServices.ActiveDirectory.DomainController.cs +++ b/Microsoft.Research/Contracts/System.DirectoryServices/Sources/System.DirectoryServices.ActiveDirectory.DomainController.cs @@ -62,6 +62,7 @@ public static DomainControllerCollection FindAll(DirectoryContext context) { Contract.Requires(context != null); Contract.Requires(context.ContextType == DirectoryContextType.Domain); + Contract.Ensures(Contract.Result() != null); return default(DomainControllerCollection); } @@ -71,6 +72,7 @@ public static DomainControllerCollection FindAll(DirectoryContext context, strin Contract.Requires(context != null); Contract.Requires(context.ContextType == DirectoryContextType.Domain); Contract.Requires(siteName != null); + Contract.Ensures(Contract.Result() != null); return default(DomainControllerCollection); } @@ -80,6 +82,7 @@ public static System.DirectoryServices.ActiveDirectory.DomainController FindOne( Contract.Requires(context != null); Contract.Requires(context.ContextType == DirectoryContextType.Domain); Contract.Requires(siteName != null); + Contract.Ensures(Contract.Result() != null); return default(System.DirectoryServices.ActiveDirectory.DomainController); } @@ -88,6 +91,7 @@ public static System.DirectoryServices.ActiveDirectory.DomainController FindOne( { Contract.Requires(context != null); Contract.Requires(context.ContextType == DirectoryContextType.Domain); + Contract.Ensures(Contract.Result() != null); return default(System.DirectoryServices.ActiveDirectory.DomainController); } @@ -97,19 +101,27 @@ public static System.DirectoryServices.ActiveDirectory.DomainController FindOne( Contract.Requires(context != null); Contract.Requires(context.ContextType == DirectoryContextType.Domain); Contract.Requires(siteName != null); + Contract.Ensures(Contract.Result() != null); return default(System.DirectoryServices.ActiveDirectory.DomainController); } - public static System.DirectoryServices.ActiveDirectory.DomainController FindOne(DirectoryContext context, LocatorOptions flag) - { - Contract.Requires(context != null); - Contract.Requires(context.ContextType == DirectoryContextType.Domain); + /// + /// Finds the one. + /// + /// The context. + /// The flag. + /// + public static System.DirectoryServices.ActiveDirectory.DomainController FindOne(DirectoryContext context, LocatorOptions flag) + { + Contract.Requires(context != null); + Contract.Requires(context.ContextType == DirectoryContextType.Domain); + Contract.Ensures(Contract.Result() != null); - return default(System.DirectoryServices.ActiveDirectory.DomainController); - } + return default(System.DirectoryServices.ActiveDirectory.DomainController); + } - public override ReplicationNeighborCollection GetAllReplicationNeighbors() + public override ReplicationNeighborCollection GetAllReplicationNeighbors() { return default(ReplicationNeighborCollection); } diff --git a/Microsoft.Research/Contracts/System.DirectoryServices/Sources/System.DirectoryServices.DirectoryEntry.cs b/Microsoft.Research/Contracts/System.DirectoryServices/Sources/System.DirectoryServices.DirectoryEntry.cs index 7361150c..787befba 100644 --- a/Microsoft.Research/Contracts/System.DirectoryServices/Sources/System.DirectoryServices.DirectoryEntry.cs +++ b/Microsoft.Research/Contracts/System.DirectoryServices/Sources/System.DirectoryServices.DirectoryEntry.cs @@ -51,6 +51,7 @@ public void CommitChanges() public System.DirectoryServices.DirectoryEntry CopyTo(System.DirectoryServices.DirectoryEntry newParent) { + Contract.Requires(newParent != null); Contract.Ensures(Contract.Result() != null); return default(System.DirectoryServices.DirectoryEntry); } @@ -58,6 +59,7 @@ public System.DirectoryServices.DirectoryEntry CopyTo(System.DirectoryServices.D // newname can be null public System.DirectoryServices.DirectoryEntry CopyTo(System.DirectoryServices.DirectoryEntry newParent, string newName) { + Contract.Requires(newParent != null); Contract.Ensures(Contract.Result() != null); return default(System.DirectoryServices.DirectoryEntry); } diff --git a/Microsoft.Research/Contracts/System.Drawing/System.Drawing.Graphics.cs b/Microsoft.Research/Contracts/System.Drawing/System.Drawing.Graphics.cs index 9ab98912..47fbd14f 100644 --- a/Microsoft.Research/Contracts/System.Drawing/System.Drawing.Graphics.cs +++ b/Microsoft.Research/Contracts/System.Drawing/System.Drawing.Graphics.cs @@ -4074,7 +4074,7 @@ private Graphics() { } //// System.Exception: //// image has an indexed pixel format or its format is undefined. public static Graphics FromImage(Image image) { - Contract.Requires(image != null, "image"); + Contract.Requires(image != null); Contract.Requires((image.PixelFormat & PixelFormat.Indexed) == 0); Contract.Ensures(Contract.Result() != null); return default(Graphics); diff --git a/Microsoft.Research/Contracts/System.ServiceModel/Sources/System.ServiceModel.Channels.MessageFault.cs b/Microsoft.Research/Contracts/System.ServiceModel/Sources/System.ServiceModel.Channels.MessageFault.cs index 7d313db3..c85a94d0 100644 --- a/Microsoft.Research/Contracts/System.ServiceModel/Sources/System.ServiceModel.Channels.MessageFault.cs +++ b/Microsoft.Research/Contracts/System.ServiceModel/Sources/System.ServiceModel.Channels.MessageFault.cs @@ -43,6 +43,8 @@ abstract public partial class MessageFault #region Methods and constructors public static MessageFault CreateFault(System.ServiceModel.FaultCode code, System.ServiceModel.FaultReason reason, Object detail, System.Runtime.Serialization.XmlObjectSerializer serializer, string actor, string node) { + Contract.Requires(code != null); + Contract.Requires(reason != null); Contract.Ensures(Contract.Result() != null); return default(MessageFault); @@ -55,6 +57,8 @@ public static MessageFault CreateFault(Message message, int maxBufferSize) public static MessageFault CreateFault(System.ServiceModel.FaultCode code, string reason) { + Contract.Requires(code != null); + Contract.Requires(reason != null); Contract.Ensures(Contract.Result() != null); return default(MessageFault); @@ -62,6 +66,8 @@ public static MessageFault CreateFault(System.ServiceModel.FaultCode code, strin public static MessageFault CreateFault(System.ServiceModel.FaultCode code, System.ServiceModel.FaultReason reason) { + Contract.Requires(code != null); + Contract.Requires(reason != null); Contract.Ensures(Contract.Result() != null); return default(MessageFault); @@ -69,6 +75,8 @@ public static MessageFault CreateFault(System.ServiceModel.FaultCode code, Syste public static MessageFault CreateFault(System.ServiceModel.FaultCode code, System.ServiceModel.FaultReason reason, Object detail) { + Contract.Requires(code != null); + Contract.Requires(reason != null); Contract.Ensures(Contract.Result() != null); return default(MessageFault); @@ -76,6 +84,8 @@ public static MessageFault CreateFault(System.ServiceModel.FaultCode code, Syste public static MessageFault CreateFault(System.ServiceModel.FaultCode code, System.ServiceModel.FaultReason reason, Object detail, System.Runtime.Serialization.XmlObjectSerializer serializer, string actor) { + Contract.Requires(code != null); + Contract.Requires(reason != null); Contract.Ensures(Contract.Result() != null); return default(MessageFault); @@ -83,6 +93,8 @@ public static MessageFault CreateFault(System.ServiceModel.FaultCode code, Syste public static MessageFault CreateFault(System.ServiceModel.FaultCode code, System.ServiceModel.FaultReason reason, Object detail, System.Runtime.Serialization.XmlObjectSerializer serializer) { + Contract.Requires(code != null); + Contract.Requires(reason != null); Contract.Ensures(Contract.Result() != null); return default(MessageFault); diff --git a/Microsoft.Research/Contracts/System.ServiceModel/Sources/System.ServiceModel.Channels.MessageHeader.cs b/Microsoft.Research/Contracts/System.ServiceModel/Sources/System.ServiceModel.Channels.MessageHeader.cs index 964fbb41..2c0dc112 100644 --- a/Microsoft.Research/Contracts/System.ServiceModel/Sources/System.ServiceModel.Channels.MessageHeader.cs +++ b/Microsoft.Research/Contracts/System.ServiceModel/Sources/System.ServiceModel.Channels.MessageHeader.cs @@ -129,26 +129,37 @@ protected MessageHeader() protected virtual new void OnWriteStartHeader(System.Xml.XmlDictionaryWriter writer, MessageVersion messageVersion) { Contract.Requires(writer != null); + Contract.Requires(messageVersion != null); } public void WriteHeader(System.Xml.XmlDictionaryWriter writer, MessageVersion messageVersion) { + Contract.Requires(writer != null); + Contract.Requires(messageVersion != null); } public void WriteHeader(System.Xml.XmlWriter writer, MessageVersion messageVersion) { + Contract.Requires(writer != null); + Contract.Requires(messageVersion != null); } protected void WriteHeaderAttributes(System.Xml.XmlDictionaryWriter writer, MessageVersion messageVersion) { + Contract.Requires(writer != null); + Contract.Requires(messageVersion != null); } public void WriteHeaderContents(System.Xml.XmlDictionaryWriter writer, MessageVersion messageVersion) { + Contract.Requires(writer != null); + Contract.Requires(messageVersion != null); } public void WriteStartHeader(System.Xml.XmlDictionaryWriter writer, MessageVersion messageVersion) { + Contract.Requires(writer != null); + Contract.Requires(messageVersion != null); } #endregion diff --git a/Microsoft.Research/Contracts/System.ServiceModel/Sources/System.ServiceModel.Channels.MessageVersion.cs b/Microsoft.Research/Contracts/System.ServiceModel/Sources/System.ServiceModel.Channels.MessageVersion.cs index 27a3ccae..312ad65b 100644 --- a/Microsoft.Research/Contracts/System.ServiceModel/Sources/System.ServiceModel.Channels.MessageVersion.cs +++ b/Microsoft.Research/Contracts/System.ServiceModel/Sources/System.ServiceModel.Channels.MessageVersion.cs @@ -43,6 +43,7 @@ sealed public partial class MessageVersion #region Methods and constructors public static MessageVersion CreateVersion(System.ServiceModel.EnvelopeVersion envelopeVersion) { + Contract.Requires(envelopeVersion != null); Contract.Ensures(Contract.Result() != null); return default(MessageVersion); @@ -50,6 +51,8 @@ public static MessageVersion CreateVersion(System.ServiceModel.EnvelopeVersion e public static MessageVersion CreateVersion(System.ServiceModel.EnvelopeVersion envelopeVersion, AddressingVersion addressingVersion) { + Contract.Requires(envelopeVersion != null); + Contract.Requires(addressingVersion != null); Contract.Ensures(Contract.Result() != null); return default(MessageVersion); diff --git a/Microsoft.Research/Contracts/System.ServiceModel/Sources/System.ServiceModel.Channels.SecurityBindingElement.cs b/Microsoft.Research/Contracts/System.ServiceModel/Sources/System.ServiceModel.Channels.SecurityBindingElement.cs index 2304d34a..b2cc222e 100644 --- a/Microsoft.Research/Contracts/System.ServiceModel/Sources/System.ServiceModel.Channels.SecurityBindingElement.cs +++ b/Microsoft.Research/Contracts/System.ServiceModel/Sources/System.ServiceModel.Channels.SecurityBindingElement.cs @@ -80,6 +80,7 @@ public static TransportSecurityBindingElement CreateCertificateOverTransportBind public static TransportSecurityBindingElement CreateCertificateOverTransportBindingElement(System.ServiceModel.MessageSecurityVersion version) { + Contract.Requires(version != null); Contract.Ensures(Contract.Result() != null); return default(TransportSecurityBindingElement); @@ -94,6 +95,7 @@ public static AsymmetricSecurityBindingElement CreateCertificateSignatureBinding public static SymmetricSecurityBindingElement CreateIssuedTokenBindingElement(System.ServiceModel.Security.Tokens.IssuedSecurityTokenParameters issuedTokenParameters) { + Contract.Requires(issuedTokenParameters != null); Contract.Ensures(Contract.Result() != null); return default(SymmetricSecurityBindingElement); @@ -101,24 +103,31 @@ public static SymmetricSecurityBindingElement CreateIssuedTokenBindingElement(Sy public static SymmetricSecurityBindingElement CreateIssuedTokenForCertificateBindingElement(System.ServiceModel.Security.Tokens.IssuedSecurityTokenParameters issuedTokenParameters) { + Contract.Requires(issuedTokenParameters != null); + Contract.Ensures(Contract.Result() != null); return default(SymmetricSecurityBindingElement); } public static SymmetricSecurityBindingElement CreateIssuedTokenForSslBindingElement(System.ServiceModel.Security.Tokens.IssuedSecurityTokenParameters issuedTokenParameters, bool requireCancellation) { + Contract.Requires(issuedTokenParameters != null); + Contract.Ensures(Contract.Result() != null); return default(SymmetricSecurityBindingElement); } public static SymmetricSecurityBindingElement CreateIssuedTokenForSslBindingElement(System.ServiceModel.Security.Tokens.IssuedSecurityTokenParameters issuedTokenParameters) { + Contract.Ensures(Contract.Result() != null); + Contract.Requires(issuedTokenParameters != null); return default(SymmetricSecurityBindingElement); } public static TransportSecurityBindingElement CreateIssuedTokenOverTransportBindingElement(System.ServiceModel.Security.Tokens.IssuedSecurityTokenParameters issuedTokenParameters) { + Contract.Requires(issuedTokenParameters != null); Contract.Ensures(Contract.Result() != null); return default(TransportSecurityBindingElement); @@ -140,6 +149,7 @@ public static TransportSecurityBindingElement CreateKerberosOverTransportBinding public static SecurityBindingElement CreateMutualCertificateBindingElement(System.ServiceModel.MessageSecurityVersion version) { + Contract.Requires(version != null); Contract.Ensures(Contract.Result() != null); return default(SecurityBindingElement); @@ -147,6 +157,7 @@ public static SecurityBindingElement CreateMutualCertificateBindingElement(Syste public static SecurityBindingElement CreateMutualCertificateBindingElement(System.ServiceModel.MessageSecurityVersion version, bool allowSerializedSigningTokenOnReply) { + Contract.Requires(version != null); Contract.Ensures(Contract.Result() != null); return default(SecurityBindingElement); @@ -168,6 +179,7 @@ public static AsymmetricSecurityBindingElement CreateMutualCertificateDuplexBind public static AsymmetricSecurityBindingElement CreateMutualCertificateDuplexBindingElement(System.ServiceModel.MessageSecurityVersion version) { + Contract.Requires(version != null); Contract.Ensures(Contract.Result() != null); return default(AsymmetricSecurityBindingElement); @@ -175,6 +187,7 @@ public static AsymmetricSecurityBindingElement CreateMutualCertificateDuplexBind public static SecurityBindingElement CreateSecureConversationBindingElement(SecurityBindingElement bootstrapSecurity, bool requireCancellation) { + Contract.Requires(bootstrapSecurity != null); Contract.Ensures(Contract.Result() != null); return default(SecurityBindingElement); @@ -182,6 +195,7 @@ public static SecurityBindingElement CreateSecureConversationBindingElement(Secu public static SecurityBindingElement CreateSecureConversationBindingElement(SecurityBindingElement bootstrapSecurity, bool requireCancellation, System.ServiceModel.Security.ChannelProtectionRequirements bootstrapProtectionRequirements) { + Contract.Requires(bootstrapSecurity != null); Contract.Ensures(Contract.Result() != null); return default(SecurityBindingElement); @@ -189,6 +203,7 @@ public static SecurityBindingElement CreateSecureConversationBindingElement(Secu public static SecurityBindingElement CreateSecureConversationBindingElement(SecurityBindingElement bootstrapSecurity) { + Contract.Requires(bootstrapSecurity != null); Contract.Ensures(Contract.Result() != null); return default(SecurityBindingElement); diff --git a/Microsoft.Research/Contracts/System.ServiceModel/Sources/System.ServiceModel.Description.MetadataResolver.cs b/Microsoft.Research/Contracts/System.ServiceModel/Sources/System.ServiceModel.Description.MetadataResolver.cs index 955a0d63..a899f5f6 100644 --- a/Microsoft.Research/Contracts/System.ServiceModel/Sources/System.ServiceModel.Description.MetadataResolver.cs +++ b/Microsoft.Research/Contracts/System.ServiceModel/Sources/System.ServiceModel.Description.MetadataResolver.cs @@ -98,7 +98,9 @@ public static ServiceEndpointCollection EndResolve(IAsyncResult result) public static ServiceEndpointCollection Resolve(IEnumerable contracts, System.ServiceModel.EndpointAddress address, MetadataExchangeClient client) { + Contract.Requires(contracts != null); Contract.Requires(address != null); + Contract.Requires(client != null); Contract.Ensures(Contract.Result() != null); return default(ServiceEndpointCollection); @@ -106,6 +108,7 @@ public static ServiceEndpointCollection Resolve(IEnumerable public static ServiceEndpointCollection Resolve(IEnumerable contracts, System.ServiceModel.EndpointAddress address) { + Contract.Requires(contracts != null); Contract.Requires(address != null); Contract.Ensures(Contract.Result() != null); @@ -114,6 +117,7 @@ public static ServiceEndpointCollection Resolve(IEnumerable public static ServiceEndpointCollection Resolve(Type contract, System.ServiceModel.EndpointAddress address) { + Contract.Requires(contract != null); Contract.Requires(address != null); Contract.Ensures(Contract.Result() != null); @@ -122,6 +126,9 @@ public static ServiceEndpointCollection Resolve(Type contract, System.ServiceMod public static ServiceEndpointCollection Resolve(IEnumerable contracts, Uri address, MetadataExchangeClientMode mode, MetadataExchangeClient client) { + Contract.Requires(contracts != null); + Contract.Requires(address != null); + Contract.Requires(client != null); Contract.Ensures(Contract.Result() != null); return default(ServiceEndpointCollection); @@ -129,6 +136,7 @@ public static ServiceEndpointCollection Resolve(IEnumerable public static ServiceEndpointCollection Resolve(IEnumerable contracts, Uri address, MetadataExchangeClientMode mode) { + Contract.Requires(contracts != null); Contract.Requires(address != null); Contract.Ensures(Contract.Result() != null); @@ -137,6 +145,7 @@ public static ServiceEndpointCollection Resolve(IEnumerable public static ServiceEndpointCollection Resolve(Type contract, Uri address, MetadataExchangeClientMode mode) { + Contract.Requires(contract != null); Contract.Requires(address != null); Contract.Ensures(Contract.Result() != null); diff --git a/Microsoft.Research/Contracts/System.ServiceModel/Sources/System.ServiceModel.Description.MetadataSection.cs b/Microsoft.Research/Contracts/System.ServiceModel/Sources/System.ServiceModel.Description.MetadataSection.cs index cc413a88..1b08f6be 100644 --- a/Microsoft.Research/Contracts/System.ServiceModel/Sources/System.ServiceModel.Description.MetadataSection.cs +++ b/Microsoft.Research/Contracts/System.ServiceModel/Sources/System.ServiceModel.Description.MetadataSection.cs @@ -50,6 +50,7 @@ public static System.ServiceModel.Description.MetadataSection CreateFromPolicy(S public static System.ServiceModel.Description.MetadataSection CreateFromSchema(System.Xml.Schema.XmlSchema schema) { + Contract.Requires(schema != null); Contract.Ensures(Contract.Result() != null); return default(System.ServiceModel.Description.MetadataSection); @@ -57,6 +58,7 @@ public static System.ServiceModel.Description.MetadataSection CreateFromSchema(S public static System.ServiceModel.Description.MetadataSection CreateFromServiceDescription(System.Web.Services.Description.ServiceDescription serviceDescription) { + Contract.Requires(serviceDescription != null); Contract.Ensures(Contract.Result() != null); return default(System.ServiceModel.Description.MetadataSection); diff --git a/Microsoft.Research/Contracts/System.ServiceModel/Sources/System.ServiceModel.Description.ServiceDescription.cs b/Microsoft.Research/Contracts/System.ServiceModel/Sources/System.ServiceModel.Description.ServiceDescription.cs index 1f741bb9..4e39c822 100644 --- a/Microsoft.Research/Contracts/System.ServiceModel/Sources/System.ServiceModel.Description.ServiceDescription.cs +++ b/Microsoft.Research/Contracts/System.ServiceModel/Sources/System.ServiceModel.Description.ServiceDescription.cs @@ -50,6 +50,7 @@ public static System.ServiceModel.Description.ServiceDescription GetService(Obje public static System.ServiceModel.Description.ServiceDescription GetService(Type serviceType) { + Contract.Requires(serviceType != null); Contract.Ensures(Contract.Result() != null); return default(System.ServiceModel.Description.ServiceDescription); @@ -57,6 +58,7 @@ public static System.ServiceModel.Description.ServiceDescription GetService(Type public ServiceDescription(IEnumerable endpoints) { + Contract.Requires(endpoints != null); } public ServiceDescription() diff --git a/Microsoft.Research/Contracts/System.Web/System.Web.HttpResponse.cs b/Microsoft.Research/Contracts/System.Web/System.Web.HttpResponse.cs index 192ae9a2..227d1dda 100644 --- a/Microsoft.Research/Contracts/System.Web/System.Web.HttpResponse.cs +++ b/Microsoft.Research/Contracts/System.Web/System.Web.HttpResponse.cs @@ -437,6 +437,7 @@ public string Status { get { + Contract.Ensures(Contract.Result() != null); return default(string); } set diff --git a/Microsoft.Research/Contracts/System.Web/System.Web.UI.Page.cs b/Microsoft.Research/Contracts/System.Web/System.Web.UI.Page.cs index 1cc6706f..b0376b0e 100644 --- a/Microsoft.Research/Contracts/System.Web/System.Web.UI.Page.cs +++ b/Microsoft.Research/Contracts/System.Web/System.Web.UI.Page.cs @@ -463,7 +463,8 @@ public string Culture { get { - Contract.Ensures (Contract.Result() == System.Threading.Thread.CurrentThread.CurrentCulture.DisplayName); + Contract.Ensures(Contract.Result() != null); + Contract.Ensures(Contract.Result() == System.Threading.Thread.CurrentThread.CurrentCulture.DisplayName); return default(string); } @@ -910,6 +911,7 @@ public string UICulture { get { + Contract.Ensures(Contract.Result() != null); Contract.Ensures (Contract.Result() == System.Threading.Thread.CurrentThread.CurrentUICulture.DisplayName); return default(string); diff --git a/Microsoft.Research/Contracts/System.Web/System.Web.UI.ThemeProvider.cs b/Microsoft.Research/Contracts/System.Web/System.Web.UI.ThemeProvider.cs index f516886a..409dd19c 100644 --- a/Microsoft.Research/Contracts/System.Web/System.Web.UI.ThemeProvider.cs +++ b/Microsoft.Research/Contracts/System.Web/System.Web.UI.ThemeProvider.cs @@ -53,6 +53,7 @@ public System.Collections.IDictionary GetSkinControlBuildersForControlType (Type public System.Collections.ICollection GetSkinsForControl (Type type) { + Contract.Requires(type != null); Contract.Ensures (Contract.Result() != null); return default(System.Collections.ICollection); diff --git a/Microsoft.Research/Contracts/System.Web/System.Web.UI.WebControls.GridView.cs b/Microsoft.Research/Contracts/System.Web/System.Web.UI.WebControls.GridView.cs index 20ba036e..57def18a 100644 --- a/Microsoft.Research/Contracts/System.Web/System.Web.UI.WebControls.GridView.cs +++ b/Microsoft.Research/Contracts/System.Web/System.Web.UI.WebControls.GridView.cs @@ -48,6 +48,7 @@ public partial class GridView : CompositeDataBoundControl, IPostBackContainer, S protected virtual new AutoGeneratedField CreateAutoGeneratedColumn (AutoGeneratedFieldProperties fieldProperties) { Contract.Requires (fieldProperties != null); + Contract.Ensures(Contract.Result() != null); return default(AutoGeneratedField); } diff --git a/Microsoft.Research/Contracts/System.Windows.Forms/System.Windows.Forms.ToolStripItemCollection.cs b/Microsoft.Research/Contracts/System.Windows.Forms/System.Windows.Forms.ToolStripItemCollection.cs index 77687f68..eeee8520 100644 --- a/Microsoft.Research/Contracts/System.Windows.Forms/System.Windows.Forms.ToolStripItemCollection.cs +++ b/Microsoft.Research/Contracts/System.Windows.Forms/System.Windows.Forms.ToolStripItemCollection.cs @@ -42,6 +42,7 @@ public class ToolStripItemCollection public ToolStripItemCollection(ToolStrip owner, ToolStripItem[] value) { Contract.Requires(owner != null); + Contract.Requires(value != null); } // Summary: diff --git a/Microsoft.Research/Contracts/System.Xml/System.Xml.XPath.XPathNavigator.cs b/Microsoft.Research/Contracts/System.Xml/System.Xml.XPath.XPathNavigator.cs index c676788c..76136f1f 100644 --- a/Microsoft.Research/Contracts/System.Xml/System.Xml.XPath.XPathNavigator.cs +++ b/Microsoft.Research/Contracts/System.Xml/System.Xml.XPath.XPathNavigator.cs @@ -1743,7 +1743,9 @@ public virtual XPathNodeIterator Select(string xpath) { // // System.Xml.XPath.XPathException: // The XPath expression is not valid. - public virtual XPathNodeIterator Select(XPathExpression expr) { + public virtual XPathNodeIterator Select(XPathExpression expr) + { + Contract.Requires(expr != null); Contract.Ensures(Contract.Result() != null); return default(XPathNodeIterator); } diff --git a/Microsoft.Research/Contracts/System.Xml/System.Xml.XmlNode.cs b/Microsoft.Research/Contracts/System.Xml/System.Xml.XmlNode.cs index 72211818..b11fbe9e 100644 --- a/Microsoft.Research/Contracts/System.Xml/System.Xml.XmlNode.cs +++ b/Microsoft.Research/Contracts/System.Xml/System.Xml.XmlNode.cs @@ -500,6 +500,7 @@ public virtual string GetPrefixOfNamespace(string namespaceURI) // this node. The refChild is not a child of this node. This node is read-only. public virtual XmlNode InsertAfter(XmlNode newChild, XmlNode refChild) { + Contract.Requires(newChild != null); Contract.Requires(newChild != this); Contract.Requires(refChild == null || refChild.ParentNode == this); Contract.Ensures(Contract.Result() != null); @@ -531,6 +532,7 @@ public virtual XmlNode InsertAfter(XmlNode newChild, XmlNode refChild) // this node. The refChild is not a child of this node. This node is read-only. public virtual XmlNode InsertBefore(XmlNode newChild, XmlNode refChild) { + Contract.Requires(newChild != null); Contract.Requires(newChild != this); Contract.Requires(refChild == null || refChild.ParentNode == this); Contract.Ensures(Contract.Result() != null); @@ -567,6 +569,7 @@ public virtual XmlNode InsertBefore(XmlNode newChild, XmlNode refChild) // this node. This node is read-only. public virtual XmlNode PrependChild(XmlNode newChild) { + Contract.Requires(newChild != null); Contract.Ensures(Contract.Result() != null); return default(XmlNode); @@ -621,6 +624,8 @@ public virtual XmlNode RemoveChild(XmlNode oldChild) // node. public virtual XmlNode ReplaceChild(XmlNode newChild, XmlNode oldChild) { + Contract.Requires(newChild != null); + Contract.Requires(oldChild != null); Contract.Ensures(Contract.Result() != null); return default(XmlNode); diff --git a/Microsoft.Research/Contracts/System.Xml/System.Xml.XmlSchemaSet.cs b/Microsoft.Research/Contracts/System.Xml/System.Xml.XmlSchemaSet.cs index 07d79245..20b52f79 100644 --- a/Microsoft.Research/Contracts/System.Xml/System.Xml.XmlSchemaSet.cs +++ b/Microsoft.Research/Contracts/System.Xml/System.Xml.XmlSchemaSet.cs @@ -416,6 +416,7 @@ public bool RemoveRecursive(XmlSchema schemaToRemove) public XmlSchema Reprocess(XmlSchema schema) { Contract.Requires(schema != null); + Contract.Ensures(Contract.Result() != null); return default(XmlSchema); } diff --git a/Microsoft.Research/Contracts/System/System.Collections.Generic.LinkedList.cs b/Microsoft.Research/Contracts/System/System.Collections.Generic.LinkedList.cs index 08e9c5cb..3e35ed1a 100644 --- a/Microsoft.Research/Contracts/System/System.Collections.Generic.LinkedList.cs +++ b/Microsoft.Research/Contracts/System/System.Collections.Generic.LinkedList.cs @@ -158,7 +158,7 @@ public void AddAfter(LinkedListNode node, LinkedListNode newNode) public LinkedListNode AddAfter(LinkedListNode node, T value) { Contract.Requires(node != null); - + Contract.Ensures(Contract.Result>() != null); Contract.Ensures(Count == Contract.OldValue(Count) + 1); return default(LinkedListNode); @@ -213,7 +213,7 @@ public void AddBefore(LinkedListNode node, LinkedListNode newNode) public LinkedListNode AddBefore(LinkedListNode node, T value) { Contract.Requires(node != null); - + Contract.Ensures(Contract.Result>() != null); Contract.Ensures(Count == Contract.OldValue(Count) + 1); return default(LinkedListNode); diff --git a/Microsoft.Research/Contracts/System/System.Collections.Specialized.NameObjectCollectionBase.cs b/Microsoft.Research/Contracts/System/System.Collections.Specialized.NameObjectCollectionBase.cs index 97e875b6..63ada648 100644 --- a/Microsoft.Research/Contracts/System/System.Collections.Specialized.NameObjectCollectionBase.cs +++ b/Microsoft.Research/Contracts/System/System.Collections.Specialized.NameObjectCollectionBase.cs @@ -248,6 +248,7 @@ protected object[] BaseGetAllValues() [Pure] protected object[] BaseGetAllValues(Type type) { + Contract.Requires(type != null); Contract.Ensures(Contract.Result() != null); return default(object[]); } diff --git a/Microsoft.Research/Contracts/System/System.ComponentModel.PropertyDescriptor.cs b/Microsoft.Research/Contracts/System/System.ComponentModel.PropertyDescriptor.cs index 51c55a43..4605d09d 100644 --- a/Microsoft.Research/Contracts/System/System.ComponentModel.PropertyDescriptor.cs +++ b/Microsoft.Research/Contracts/System/System.ComponentModel.PropertyDescriptor.cs @@ -178,6 +178,7 @@ public virtual void AddValueChanged(object component, EventHandler handler) // A new instance of the type. protected object CreateInstance(Type type) { + Contract.Requires(type != null); Contract.Ensures(Contract.Result() != null); return default(object); diff --git a/Microsoft.Research/Contracts/System/System.ComponentModel.TypeDescriptor.cs b/Microsoft.Research/Contracts/System/System.ComponentModel.TypeDescriptor.cs index 1b974e92..6acbc7ef 100644 --- a/Microsoft.Research/Contracts/System/System.ComponentModel.TypeDescriptor.cs +++ b/Microsoft.Research/Contracts/System/System.ComponentModel.TypeDescriptor.cs @@ -1195,6 +1195,7 @@ public static TypeDescriptionProvider GetProvider(object instance) public static TypeDescriptionProvider GetProvider(Type type) { Contract.Requires(type != null); + Contract.Ensures(Contract.Result() != null); return default(TypeDescriptionProvider); } diff --git a/Microsoft.Research/Contracts/System/System.Net.CookieContainer.cs b/Microsoft.Research/Contracts/System/System.Net.CookieContainer.cs index 9263d0c9..82571f6e 100644 --- a/Microsoft.Research/Contracts/System/System.Net.CookieContainer.cs +++ b/Microsoft.Research/Contracts/System/System.Net.CookieContainer.cs @@ -65,8 +65,9 @@ public string GetCookieHeader (Uri uri) { } public CookieCollection GetCookies (Uri uri) { Contract.Requires(uri != null); + Contract.Ensures(Contract.Result() != null); - return default(CookieCollection); + return default(CookieCollection); } public void Add (Uri uri, CookieCollection cookies) { Contract.Requires(uri != null); diff --git a/Microsoft.Research/Contracts/System/System.Net.HttpWebRequest.cs b/Microsoft.Research/Contracts/System/System.Net.HttpWebRequest.cs index 1efda260..f4410885 100644 --- a/Microsoft.Research/Contracts/System/System.Net.HttpWebRequest.cs +++ b/Microsoft.Research/Contracts/System/System.Net.HttpWebRequest.cs @@ -244,6 +244,7 @@ public virtual WebResponse GetResponse() { } public virtual WebResponse EndGetResponse(IAsyncResult asyncResult) { Contract.Requires(asyncResult != null); + Contract.Ensures(Contract.Result() != null); return default(WebResponse); } @@ -258,6 +259,7 @@ public virtual System.IO.Stream GetRequestStream() { } public virtual System.IO.Stream EndGetRequestStream(IAsyncResult asyncResult) { Contract.Requires(asyncResult != null); + Contract.Ensures(Contract.Result() != null); return default(System.IO.Stream); } diff --git a/Microsoft.Research/Contracts/System/System.Net.Sockets.TcpListener.cs b/Microsoft.Research/Contracts/System/System.Net.Sockets.TcpListener.cs index 37a8cd26..97850301 100644 --- a/Microsoft.Research/Contracts/System/System.Net.Sockets.TcpListener.cs +++ b/Microsoft.Research/Contracts/System/System.Net.Sockets.TcpListener.cs @@ -222,6 +222,7 @@ public Socket EndAcceptSocket(IAsyncResult asyncResult) // A System.Net.Sockets.TcpClient. public TcpClient EndAcceptTcpClient(IAsyncResult asyncResult) { + Contract.Requires(asyncResult != null); Contract.Ensures(Contract.Result() != null); return null; diff --git a/Microsoft.Research/Contracts/System/System.Uri.cs b/Microsoft.Research/Contracts/System/System.Uri.cs index 672b1338..5cb10b14 100644 --- a/Microsoft.Research/Contracts/System/System.Uri.cs +++ b/Microsoft.Research/Contracts/System/System.Uri.cs @@ -397,8 +397,9 @@ public static bool IsWellFormedUriString(string uriString, UriKind uriKind) } [Pure] - public Uri MakeRelativeUri(Uri toUri) + public Uri MakeRelativeUri(Uri uri) { + Contract.Requires(uri != null); Contract.Ensures(Contract.Result() != null); return default(Uri); } diff --git a/Microsoft.Research/Contracts/WindowsBase/System.Windows.DependencyProperty.cs b/Microsoft.Research/Contracts/WindowsBase/System.Windows.DependencyProperty.cs index 47bf34c4..d6d828ab 100644 --- a/Microsoft.Research/Contracts/WindowsBase/System.Windows.DependencyProperty.cs +++ b/Microsoft.Research/Contracts/WindowsBase/System.Windows.DependencyProperty.cs @@ -124,6 +124,7 @@ public Type PropertyType // by the adding class as a public static readonly field. public DependencyProperty AddOwner(Type ownerType) { + Contract.Requires(ownerType != null); Contract.Ensures(Contract.Result() != null); return null; diff --git a/Microsoft.Research/Contracts/WindowsBase/System.Windows.Threading.Dispatcher.cs b/Microsoft.Research/Contracts/WindowsBase/System.Windows.Threading.Dispatcher.cs index c2776d6b..033b54e1 100644 --- a/Microsoft.Research/Contracts/WindowsBase/System.Windows.Threading.Dispatcher.cs +++ b/Microsoft.Research/Contracts/WindowsBase/System.Windows.Threading.Dispatcher.cs @@ -60,24 +60,28 @@ public DispatcherOperation BeginInvoke(Delegate method, params object[] args) public DispatcherOperation BeginInvoke(DispatcherPriority priority, Delegate method) { + Contract.Requires(method != null); Contract.Ensures(Contract.Result() != null); return null; } public DispatcherOperation BeginInvoke(Delegate method, DispatcherPriority priority, params object[] args) { + Contract.Requires(method != null); Contract.Ensures(Contract.Result() != null); return null; } public DispatcherOperation BeginInvoke(DispatcherPriority priority, Delegate method, object arg) { + Contract.Requires(method != null); Contract.Ensures(Contract.Result() != null); return null; } public DispatcherOperation BeginInvoke(DispatcherPriority priority, Delegate method, object arg, params object[] args) { + Contract.Requires(method != null); Contract.Ensures(Contract.Result() != null); return null; }