Code:
/ 4.0 / 4.0 / DEVDIV_TFS / Dev10 / Releases / RTMRel / ndp / clr / src / BCL / System / Diagnostics / Contracts / Contracts.cs / 1305376 / Contracts.cs
// ==++==
//
// Copyright (c) Microsoft Corporation. All rights reserved.
//
// ==--==
/*============================================================
**
** Class: Contract
**
** [....],mbarnett
**
** Purpose: The contract class allows for expressing preconditions,
** postconditions, and object invariants about methods in source
** code for runtime checking & static analysis.
**
** Two classes (Contract and ContractHelper) are split into partial classes
** in order to share the public front for multiple platforms (this file)
** while providing separate implementation details for each platform.
**
===========================================================*/
#define DEBUG // The behavior of this contract library should be consistent regardless of build type.
#if SILVERLIGHT
#define FEATURE_UNTRUSTED_CALLERS
#elif REDHAWK_RUNTIME
#elif BARTOK_RUNTIME
#else // CLR
#define FEATURE_UNTRUSTED_CALLERS
#define FEATURE_RELIABILITY_CONTRACTS
#define FEATURE_SERIALIZATION
#endif
using System;
using System.Collections.Generic;
using System.Diagnostics.CodeAnalysis;
#if FEATURE_RELIABILITY_CONTRACTS
using System.Runtime.ConstrainedExecution;
#endif
#if FEATURE_UNTRUSTED_CALLERS
using System.Security;
using System.Security.Permissions;
#endif
namespace System.Diagnostics.Contracts {
#region Attributes
///
/// Methods and classes marked with this attribute can be used within calls to Contract methods. Such methods not make any visible state changes.
///
[Conditional("CONTRACTS_FULL")]
[AttributeUsage(AttributeTargets.Constructor | AttributeTargets.Method | AttributeTargets.Property | AttributeTargets.Event | AttributeTargets.Delegate | AttributeTargets.Class | AttributeTargets.Parameter, AllowMultiple = false, Inherited = true)]
public sealed class PureAttribute : Attribute
{
}
///
/// Types marked with this attribute specify that a separate type contains the contracts for this type.
///
[Conditional("CONTRACTS_FULL")]
[Conditional("DEBUG")] // Hack: For createBclSmall, make sure to include contract classes in AMD64DBG builds.
[AttributeUsage(AttributeTargets.Class | AttributeTargets.Interface | AttributeTargets.Delegate, AllowMultiple = false, Inherited = false)]
public sealed class ContractClassAttribute : Attribute
{
private Type _typeWithContracts;
public ContractClassAttribute(Type typeContainingContracts)
{
_typeWithContracts = typeContainingContracts;
}
public Type TypeContainingContracts {
get { return _typeWithContracts; }
}
}
///
/// Types marked with this attribute specify that they are a contract for the type that is the argument of the constructor.
///
[Conditional("CONTRACTS_FULL")]
[AttributeUsage(AttributeTargets.Class, AllowMultiple = false, Inherited = false)]
public sealed class ContractClassForAttribute : Attribute
{
private Type _typeIAmAContractFor;
public ContractClassForAttribute(Type typeContractsAreFor)
{
_typeIAmAContractFor = typeContractsAreFor;
}
public Type TypeContractsAreFor {
get { return _typeIAmAContractFor; }
}
}
///
/// This attribute is used to mark a method as being the invariant
/// method for a class. The method can have any name, but it must
/// return "void" and take no parameters. The body of the method
/// must consist solely of one or more calls to the method
/// Contract.Invariant. A suggested name for the method is
/// "ObjectInvariant".
///
[Conditional("CONTRACTS_FULL")]
[AttributeUsage(AttributeTargets.Method, AllowMultiple = false, Inherited = false)]
public sealed class ContractInvariantMethodAttribute : Attribute
{
}
///
/// Attribute that specifies that an assembly is a reference assembly with contracts.
///
[AttributeUsage(AttributeTargets.Assembly)]
public sealed class ContractReferenceAssemblyAttribute : Attribute
{
}
///
/// Methods (and properties) marked with this attribute can be used within calls to Contract methods, but have no runtime behavior associated with them.
///
[Conditional("CONTRACTS_FULL")]
[AttributeUsage(AttributeTargets.Method | AttributeTargets.Property, AllowMultiple = false, Inherited = true)]
public sealed class ContractRuntimeIgnoredAttribute : Attribute
{
}
/*
#if FEATURE_SERIALIZATION
[Serializable]
#endif
internal enum Mutability
{
Immutable, // read-only after construction, except for lazy initialization & caches
// Do we need a "deeply immutable" value?
Mutable,
HasInitializationPhase, // read-only after some point.
// Do we need a value for mutable types with read-only wrapper subclasses?
}
// Note: This hasn't been thought through in any depth yet. Consider it experimental.
// We should replace this with Joe's concepts.
[Conditional("CONTRACTS_FULL")]
[AttributeUsage(AttributeTargets.Class | AttributeTargets.Struct, AllowMultiple = false, Inherited = false)]
[SuppressMessage("Microsoft.Design", "CA1019:DefineAccessorsForAttributeArguments", Justification = "Thank you very much, but we like the names we've defined for the accessors")]
internal sealed class MutabilityAttribute : Attribute
{
private Mutability _mutabilityMarker;
public MutabilityAttribute(Mutability mutabilityMarker)
{
_mutabilityMarker = mutabilityMarker;
}
public Mutability Mutability {
get { return _mutabilityMarker; }
}
}
*/
///
/// Instructs downstream tools whether to assume the correctness of this assembly, type or member without performing any verification or not.
/// Can use [ContractVerification(false)] to explicitly mark assembly, type or member as one to *not* have verification performed on it.
/// Most specific element found (member, type, then assembly) takes precedence.
/// (That is useful if downstream tools allow a user to decide which polarity is the default, unmarked case.)
///
///
/// Apply this attribute to a type to apply to all members of the type, including nested types.
/// Apply this attribute to an assembly to apply to all types and members of the assembly.
/// Apply this attribute to a property to apply to both the getter and setter.
///
[Conditional("CONTRACTS_FULL")]
[AttributeUsage(AttributeTargets.Assembly | AttributeTargets.Class | AttributeTargets.Struct | AttributeTargets.Method | AttributeTargets.Constructor | AttributeTargets.Property)]
public sealed class ContractVerificationAttribute : Attribute
{
private bool _value;
public ContractVerificationAttribute(bool value) { _value = value; }
public bool Value {
get { return _value; }
}
}
///
/// Allows a field f to be used in the method contracts for a method m when f has less visibility than m.
/// For instance, if the method is public, but the field is private.
///
[Conditional("CONTRACTS_FULL")]
[AttributeUsage(AttributeTargets.Field)]
[SuppressMessage("Microsoft.Design", "CA1019:DefineAccessorsForAttributeArguments", Justification = "Thank you very much, but we like the names we've defined for the accessors")]
public sealed class ContractPublicPropertyNameAttribute : Attribute
{
private String _publicName;
public ContractPublicPropertyNameAttribute(String name)
{
_publicName = name;
}
public String Name {
get { return _publicName; }
}
}
#endregion Attributes
///
/// Contains static methods for representing program contracts such as preconditions, postconditions, and invariants.
///
///
/// WARNING: A binary rewriter must be used to insert runtime enforcement of these contracts.
/// Otherwise some contracts like Ensures can only be checked statically and will not throw exceptions during runtime when contracts are violated.
/// Please note this class uses conditional compilation to help avoid easy mistakes. Defining the preprocessor
/// symbol CONTRACTS_PRECONDITIONS will include all preconditions expressed using Contract.Requires in your
/// build. The symbol CONTRACTS_FULL will include postconditions and object invariants, and requires the binary rewriter.
///
public static partial class Contract
{
#region User Methods
#region Assume
///
/// Instructs code analysis tools to assume the expression
/// Expression to assume will always be true.
///
/// At runtime this is equivalent to an
[Pure]
[Conditional("DEBUG")]
[Conditional("CONTRACTS_FULL")]
#if FEATURE_RELIABILITY_CONTRACTS
[ReliabilityContract(Consistency.WillNotCorruptState, Cer.MayFail)]
#endif
public static void Assume(bool condition)
{
if (!condition) {
ReportFailure(ContractFailureKind.Assume, null, null, null);
}
}
///
/// Instructs code analysis tools to assume the expression
/// Expression to assume will always be true.
/// If it is not a constant string literal, then the contract may not be understood by tools.
///
/// At runtime this is equivalent to an
[Pure]
[Conditional("DEBUG")]
[Conditional("CONTRACTS_FULL")]
#if FEATURE_RELIABILITY_CONTRACTS
[ReliabilityContract(Consistency.WillNotCorruptState, Cer.MayFail)]
#endif
public static void Assume(bool condition, String userMessage)
{
if (!condition) {
ReportFailure(ContractFailureKind.Assume, userMessage, null, null);
}
}
#endregion Assume
#region Assert
///
/// In debug builds, perform a runtime check that
/// Expression to check to always be true.
[Pure]
[Conditional("DEBUG")]
[Conditional("CONTRACTS_FULL")]
#if FEATURE_RELIABILITY_CONTRACTS
[ReliabilityContract(Consistency.WillNotCorruptState, Cer.MayFail)]
#endif
public static void Assert(bool condition)
{
if (!condition)
ReportFailure(ContractFailureKind.Assert, null, null, null);
}
///
/// In debug builds, perform a runtime check that
/// Expression to check to always be true.
/// If it is not a constant string literal, then the contract may not be understood by tools.
[Pure]
[Conditional("DEBUG")]
[Conditional("CONTRACTS_FULL")]
#if FEATURE_RELIABILITY_CONTRACTS
[ReliabilityContract(Consistency.WillNotCorruptState, Cer.MayFail)]
#endif
public static void Assert(bool condition, String userMessage)
{
if (!condition)
ReportFailure(ContractFailureKind.Assert, userMessage, null, null);
}
#endregion Assert
#region Requires
///
/// Specifies a contract such that the expression
/// Boolean expression representing the contract.
///
/// This call must happen at the beginning of a method or property before any other code.
/// This contract is exposed to clients so must only reference members at least as visible as the enclosing method.
/// Use this form when backward compatibility does not force you to throw a particular exception.
///
[Pure]
[Conditional("CONTRACTS_FULL")]
#if FEATURE_RELIABILITY_CONTRACTS
[ReliabilityContract(Consistency.WillNotCorruptState, Cer.MayFail)]
#endif
public static void Requires(bool condition)
{
AssertMustUseRewriter(ContractFailureKind.Precondition, "Requires");
}
///
/// Specifies a contract such that the expression
/// Boolean expression representing the contract.
/// If it is not a constant string literal, then the contract may not be understood by tools.
///
/// This call must happen at the beginning of a method or property before any other code.
/// This contract is exposed to clients so must only reference members at least as visible as the enclosing method.
/// Use this form when backward compatibility does not force you to throw a particular exception.
///
[Pure]
[Conditional("CONTRACTS_FULL")]
#if FEATURE_RELIABILITY_CONTRACTS
[ReliabilityContract(Consistency.WillNotCorruptState, Cer.MayFail)]
#endif
public static void Requires(bool condition, String userMessage)
{
AssertMustUseRewriter(ContractFailureKind.Precondition, "Requires");
}
///
/// Specifies a contract such that the expression
/// Boolean expression representing the contract.
///
/// This call must happen at the beginning of a method or property before any other code.
/// This contract is exposed to clients so must only reference members at least as visible as the enclosing method.
/// Use this form when you want to throw a particular exception.
///
[SuppressMessage("Microsoft.Usage", "CA1801:ReviewUnusedParameters", MessageId = "condition")]
[SuppressMessage("Microsoft.Design", "CA1004:GenericMethodsShouldProvideTypeParameter")]
[Pure]
#if FEATURE_RELIABILITY_CONTRACTS
[ReliabilityContract(Consistency.WillNotCorruptState, Cer.MayFail)]
#endif
public static void Requires(bool condition) where TException : Exception
{
AssertMustUseRewriter(ContractFailureKind.Precondition, "Requires");
}
///
/// Specifies a contract such that the expression
/// Boolean expression representing the contract.
/// If it is not a constant string literal, then the contract may not be understood by tools.
///
/// This call must happen at the beginning of a method or property before any other code.
/// This contract is exposed to clients so must only reference members at least as visible as the enclosing method.
/// Use this form when you want to throw a particular exception.
///
[SuppressMessage("Microsoft.Usage", "CA1801:ReviewUnusedParameters", MessageId = "userMessage")]
[SuppressMessage("Microsoft.Usage", "CA1801:ReviewUnusedParameters", MessageId = "condition")]
[SuppressMessage("Microsoft.Design", "CA1004:GenericMethodsShouldProvideTypeParameter")]
[Pure]
#if FEATURE_RELIABILITY_CONTRACTS
[ReliabilityContract(Consistency.WillNotCorruptState, Cer.MayFail)]
#endif
public static void Requires(bool condition, String userMessage) where TException : Exception
{
AssertMustUseRewriter(ContractFailureKind.Precondition, "Requires");
}
#endregion Requires
#region Ensures
///
/// Specifies a public contract such that the expression
/// Boolean expression representing the contract. May include
/// This call must happen at the beginning of a method or property before any other code.
/// This contract is exposed to clients so must only reference members at least as visible as the enclosing method.
/// The contract rewriter must be used for runtime enforcement of this postcondition.
///
[Pure]
[Conditional("CONTRACTS_FULL")]
#if FEATURE_RELIABILITY_CONTRACTS
[ReliabilityContract(Consistency.WillNotCorruptState, Cer.MayFail)]
#endif
public static void Ensures(bool condition)
{
AssertMustUseRewriter(ContractFailureKind.Postcondition, "Ensures");
}
///
/// Specifies a public contract such that the expression
/// Boolean expression representing the contract. May include
/// This call must happen at the beginning of a method or property before any other code.
/// This contract is exposed to clients so must only reference members at least as visible as the enclosing method.
/// The contract rewriter must be used for runtime enforcement of this postcondition.
///
[Pure]
[Conditional("CONTRACTS_FULL")]
#if FEATURE_RELIABILITY_CONTRACTS
[ReliabilityContract(Consistency.WillNotCorruptState, Cer.MayFail)]
#endif
public static void Ensures(bool condition, String userMessage)
{
AssertMustUseRewriter(ContractFailureKind.Postcondition, "Ensures");
}
///
/// Specifies a contract such that if an exception of type
/// Type of exception related to this postcondition.
/// Boolean expression representing the contract. May include
/// This call must happen at the beginning of a method or property before any other code.
/// This contract is exposed to clients so must only reference types and members at least as visible as the enclosing method.
/// The contract rewriter must be used for runtime enforcement of this postcondition.
///
[Pure]
[Conditional("CONTRACTS_FULL")]
[SuppressMessage("Microsoft.Design", "CA1004:GenericMethodsShouldProvideTypeParameter", Justification = "Exception type used in tools.")]
#if FEATURE_RELIABILITY_CONTRACTS
[ReliabilityContract(Consistency.WillNotCorruptState, Cer.MayFail)]
#endif
public static void EnsuresOnThrow(bool condition) where TException : Exception
{
AssertMustUseRewriter(ContractFailureKind.PostconditionOnException, "EnsuresOnThrow");
}
///
/// Specifies a contract such that if an exception of type
/// Type of exception related to this postcondition.
/// Boolean expression representing the contract. May include
/// This call must happen at the beginning of a method or property before any other code.
/// This contract is exposed to clients so must only reference types and members at least as visible as the enclosing method.
/// The contract rewriter must be used for runtime enforcement of this postcondition.
///
[Pure]
[Conditional("CONTRACTS_FULL")]
[SuppressMessage("Microsoft.Design", "CA1004:GenericMethodsShouldProvideTypeParameter", Justification = "Exception type used in tools.")]
#if FEATURE_RELIABILITY_CONTRACTS
[ReliabilityContract(Consistency.WillNotCorruptState, Cer.MayFail)]
#endif
public static void EnsuresOnThrow(bool condition, String userMessage) where TException : Exception
{
AssertMustUseRewriter(ContractFailureKind.PostconditionOnException, "EnsuresOnThrow");
}
#region Old, Result, and Out Parameters
///
/// Represents the result (a.k.a. return value) of a method or property.
///
/// Type of return value of the enclosing method or property.
/// Return value of the enclosing method or property.
///
/// This method can only be used within the argument to the
[SuppressMessage("Microsoft.Design", "CA1004:GenericMethodsShouldProvideTypeParameter", Justification = "Not intended to be called at runtime.")]
[Pure]
#if FEATURE_RELIABILITY_CONTRACTS
[ReliabilityContract(Consistency.WillNotCorruptState, Cer.Success)]
#endif
public static T Result() { return default(T); }
///
/// Represents the final (output) value of an out parameter when returning from a method.
///
/// Type of the out parameter.
/// The out parameter.
/// The output value of the out parameter.
///
/// This method can only be used within the argument to the
[SuppressMessage("Microsoft.Design", "CA1021:AvoidOutParameters", MessageId = "0#", Justification = "Not intended to be called at runtime.")]
[Pure]
#if FEATURE_RELIABILITY_CONTRACTS
[ReliabilityContract(Consistency.WillNotCorruptState, Cer.Success)]
#endif
public static T ValueAtReturn(out T value) { value = default(T); return value; }
///
/// Represents the value of
/// Type of
/// Value to represent. This must be a field or parameter.
/// Value of
///
/// This method can only be used within the argument to the
[SuppressMessage("Microsoft.Usage", "CA1801:ReviewUnusedParameters", MessageId = "value")]
[Pure]
#if FEATURE_RELIABILITY_CONTRACTS
[ReliabilityContract(Consistency.WillNotCorruptState, Cer.Success)]
#endif
public static T OldValue(T value) { return default(T); }
#endregion Old, Result, and Out Parameters
#endregion Ensures
#region Invariant
///
/// Specifies a contract such that the expression
/// Boolean expression representing the contract.
///
/// This contact can only be specified in a dedicated invariant method declared on a class.
/// This contract is not exposed to clients so may reference members less visible as the enclosing method.
/// The contract rewriter must be used for runtime enforcement of this invariant.
///
[Pure]
[Conditional("CONTRACTS_FULL")]
#if FEATURE_RELIABILITY_CONTRACTS
[ReliabilityContract(Consistency.WillNotCorruptState, Cer.MayFail)]
#endif
public static void Invariant(bool condition)
{
AssertMustUseRewriter(ContractFailureKind.Invariant, "Invariant");
}
///
/// Specifies a contract such that the expression
/// Boolean expression representing the contract.
/// If it is not a constant string literal, then the contract may not be understood by tools.
///
/// This contact can only be specified in a dedicated invariant method declared on a class.
/// This contract is not exposed to clients so may reference members less visible as the enclosing method.
/// The contract rewriter must be used for runtime enforcement of this invariant.
///
[Pure]
[Conditional("CONTRACTS_FULL")]
#if FEATURE_RELIABILITY_CONTRACTS
[ReliabilityContract(Consistency.WillNotCorruptState, Cer.MayFail)]
#endif
public static void Invariant(bool condition, String userMessage)
{
AssertMustUseRewriter(ContractFailureKind.Invariant, "Invariant");
}
#endregion Invariant
#region Quantifiers
#region ForAll
///
/// Returns whether the true
/// for all integers starting from
/// First integer to pass to true if true for all integers
/// starting from predicate)
{
if (fromInclusive > toExclusive)
#if INSIDE_CLR
throw new ArgumentException(Environment.GetResourceString("Argument_ToExclusiveLessThanFromExclusive"));
#else
throw new ArgumentException("fromInclusive must be less than or equal to toExclusive.");
#endif
if (predicate == null)
throw new ArgumentNullException("predicate");
Contract.EndContractBlock();
for (int i = fromInclusive; i < toExclusive; i++)
if (!predicate(i)) return false;
return true;
}
///
/// Returns whether the true
/// for all elements in the
/// The collection from which elements will be drawn from to pass to true if and only if true for all elements in
/// (IEnumerable collection, Predicate predicate)
{
if (collection == null)
throw new ArgumentNullException("collection");
if (predicate == null)
throw new ArgumentNullException("predicate");
Contract.EndContractBlock();
foreach (T t in collection)
if (!predicate(t)) return false;
return true;
}
#endregion ForAll
#region Exists
///
/// Returns whether the true
/// for any integer starting from
/// First integer to pass to true if true for any integer
/// starting from predicate)
{
if (fromInclusive > toExclusive)
#if INSIDE_CLR
throw new ArgumentException(Environment.GetResourceString("Argument_ToExclusiveLessThanFromExclusive"));
#else
throw new ArgumentException("fromInclusive must be less than or equal to toExclusive.");
#endif
if (predicate == null)
throw new ArgumentNullException("predicate");
Contract.EndContractBlock();
for (int i = fromInclusive; i < toExclusive; i++)
if (predicate(i)) return true;
return false;
}
///
/// Returns whether the true
/// for any element in the
/// The collection from which elements will be drawn from to pass to true if and only if true for an element in
/// (IEnumerable collection, Predicate predicate)
{
if (collection == null)
throw new ArgumentNullException("collection");
if (predicate == null)
throw new ArgumentNullException("predicate");
Contract.EndContractBlock();
foreach (T t in collection)
if (predicate(t)) return true;
return false;
}
#endregion Exists
#endregion Quantifiers
#region Pointers
// @
#if FEATURE_UNSAFE_CONTRACTS
///
/// Runtime checking for pointer bounds is not currently feasible. Thus, at runtime, we just return
/// a very long extent for each pointer that is writable. As long as assertions are of the form
/// WritableBytes(ptr) >= ..., the runtime assertions will not fail.
/// The runtime value is 2^64 - 1 or 2^32 - 1.
///
[SuppressMessage("Microsoft.Performance", "CA1802", Justification = "FxCop is confused")]
static readonly ulong MaxWritableExtent = (UIntPtr.Size == 4) ? UInt32.MaxValue : UInt64.MaxValue;
///
/// Allows specifying a writable extent for a UIntPtr, similar to SAL's writable extent.
/// NOTE: this is for static checking only. No useful runtime code can be generated for this
/// at the moment.
///
/// Start of memory region
/// The result is the number of bytes writable starting at
[CLSCompliant(false)]
[Pure]
[ContractRuntimeIgnored]
#if FEATURE_RELIABILITY_CONTRACTS
[ReliabilityContract(Consistency.WillNotCorruptState, Cer.MayFail)]
#endif
public static ulong WritableBytes(UIntPtr startAddress) { return MaxWritableExtent - startAddress.ToUInt64(); }
///
/// Allows specifying a writable extent for a UIntPtr, similar to SAL's writable extent.
/// NOTE: this is for static checking only. No useful runtime code can be generated for this
/// at the moment.
///
/// Start of memory region
/// The result is the number of bytes writable starting at
[CLSCompliant(false)]
[Pure]
[ContractRuntimeIgnored]
#if FEATURE_RELIABILITY_CONTRACTS
[ReliabilityContract(Consistency.WillNotCorruptState, Cer.MayFail)]
#endif
public static ulong WritableBytes(IntPtr startAddress) { return MaxWritableExtent - (ulong)startAddress; }
///
/// Allows specifying a writable extent for a UIntPtr, similar to SAL's writable extent.
/// NOTE: this is for static checking only. No useful runtime code can be generated for this
/// at the moment.
///
/// Start of memory region
/// The result is the number of bytes writable starting at
[CLSCompliant(false)]
[Pure]
[ContractRuntimeIgnored]
[SecurityCritical]
#if FEATURE_RELIABILITY_CONTRACTS
[ReliabilityContract(Consistency.WillNotCorruptState, Cer.MayFail)]
#endif
//@
unsafe public static ulong WritableBytes(void* startAddress) { return MaxWritableExtent - (ulong)startAddress; }
///
/// Allows specifying a readable extent for a UIntPtr, similar to SAL's readable extent.
/// NOTE: this is for static checking only. No useful runtime code can be generated for this
/// at the moment.
///
/// Start of memory region
/// The result is the number of bytes readable starting at
[CLSCompliant(false)]
[Pure]
[ContractRuntimeIgnored]
#if FEATURE_RELIABILITY_CONTRACTS
[ReliabilityContract(Consistency.WillNotCorruptState, Cer.MayFail)]
#endif
public static ulong ReadableBytes(UIntPtr startAddress) { return MaxWritableExtent - startAddress.ToUInt64(); }
///
/// Allows specifying a readable extent for a UIntPtr, similar to SAL's readable extent.
/// NOTE: this is for static checking only. No useful runtime code can be generated for this
/// at the moment.
///
/// Start of memory region
/// The result is the number of bytes readable starting at
[CLSCompliant(false)]
[Pure]
[ContractRuntimeIgnored]
#if FEATURE_RELIABILITY_CONTRACTS
[ReliabilityContract(Consistency.WillNotCorruptState, Cer.MayFail)]
#endif
public static ulong ReadableBytes(IntPtr startAddress) { return MaxWritableExtent - (ulong)startAddress; }
///
/// Allows specifying a readable extent for a UIntPtr, similar to SAL's readable extent.
/// NOTE: this is for static checking only. No useful runtime code can be generated for this
/// at the moment.
///
/// Start of memory region
/// The result is the number of bytes readable starting at
[CLSCompliant(false)]
[Pure]
[ContractRuntimeIgnored]
[SecurityCritical]
#if FEATURE_RELIABILITY_CONTRACTS
[ReliabilityContract(Consistency.WillNotCorruptState, Cer.MayFail)]
#endif
unsafe public static ulong ReadableBytes(void* startAddress) { return MaxWritableExtent - (ulong)startAddress; }
#endif // FEATURE_UNSAFE_CONTRACTS
#endregion
#region Misc.
///
/// Marker to indicate the end of the contract section of a method.
///
[Conditional("CONTRACTS_FULL")]
#if FEATURE_RELIABILITY_CONTRACTS
[ReliabilityContract(Consistency.WillNotCorruptState, Cer.Success)]
#endif
public static void EndContractBlock() { }
#endregion
#endregion User Methods
#region Failure Behavior
///
/// Without contract rewriting, failing Assert/Assumes end up calling this method.
/// Code going through the contract rewriter never calls this method. Instead, the rewriter produced failures call
/// Internal.ContractHelper.RaiseContractFailedEvent, followed by Internal.ContractHelper.TriggerFailure.
///
static partial void ReportFailure(ContractFailureKind failureKind, String userMessage, String conditionText, Exception innerException);
///
/// This method is used internally to trigger a failure indicating to the "programmer" that he is using the interface incorrectly.
/// It is NEVER used to indicate failure of actual contracts at runtime.
///
static partial void AssertMustUseRewriter(ContractFailureKind kind, String contractKind);
#endregion
}
public enum ContractFailureKind {
Precondition,
[SuppressMessage("Microsoft.Naming", "CA1704:IdentifiersShouldBeSpelledCorrectly", MessageId = "Postcondition")]
Postcondition,
[SuppressMessage("Microsoft.Naming", "CA1704:IdentifiersShouldBeSpelledCorrectly", MessageId = "Postcondition")]
PostconditionOnException,
Invariant,
Assert,
Assume,
}
}
namespace System.Diagnostics.Contracts.Internal
{
public static partial class ContractHelper
{
#region Rewriter Failure Hooks
///
/// Rewriter will call this method on a contract failure to allow listeners to be notified.
/// The method should not perform any failure (assert/throw) itself.
///
/// null if the event was handled and should not trigger a failure.
/// Otherwise, returns the localized failure message
[SuppressMessage("Microsoft.Design", "CA1030:UseEventsWhereAppropriate")]
#if FEATURE_UNTRUSTED_CALLERS
[SuppressMessage("Microsoft.Portability", "CA1903:UseOnlyApiFromTargetedFramework", MessageId = "System.Security.SecuritySafeCriticalAttribute")]
[SecuritySafeCritical]
#endif
[System.Diagnostics.DebuggerNonUserCode]
#if FEATURE_RELIABILITY_CONTRACTS
[ReliabilityContract(Consistency.WillNotCorruptState, Cer.MayFail)]
#endif
public static string RaiseContractFailedEvent(ContractFailureKind failureKind, String userMessage, String conditionText, Exception innerException)
{
var resultFailureMessage = "Contract failed"; // default in case implementation does not assign anything.
RaiseContractFailedEventImplementation(failureKind, userMessage, conditionText, innerException, ref resultFailureMessage);
return resultFailureMessage;
}
///
/// Rewriter calls this method to get the default failure behavior.
///
#if FEATURE_UNTRUSTED_CALLERS
[SecuritySafeCritical]
#endif
[System.Diagnostics.DebuggerNonUserCode]
#if FEATURE_RELIABILITY_CONTRACTS
[ReliabilityContract(Consistency.WillNotCorruptState, Cer.Success)]
#endif
public static void TriggerFailure(ContractFailureKind kind, String displayMessage, String userMessage, String conditionText, Exception innerException)
{
TriggerFailureImplementation(kind, displayMessage, userMessage, conditionText, innerException);
}
#endregion Rewriter Failure Hooks
#region Implementation Stubs
///
/// Rewriter will call this method on a contract failure to allow listeners to be notified.
/// The method should not perform any failure (assert/throw) itself.
/// This method has 3 functions:
/// 1. Call any contract hooks (such as listeners to Contract failed events)
/// 2. Determine if the listeneres deem the failure as handled (then resultFailureMessage should be set to null)
/// 3. Produce a localized resultFailureMessage used in advertising the failure subsequently.
///
/// Should really be out (or the return value), but partial methods are not flexible enough.
/// On exit: null if the event was handled and should not trigger a failure.
/// Otherwise, returns the localized failure message
static partial void RaiseContractFailedEventImplementation(ContractFailureKind failureKind, String userMessage, String conditionText, Exception innerException, ref string resultFailureMessage);
///
/// Implements the default failure behavior of the platform. Under the BCL, it triggers an Assert box.
///
static partial void TriggerFailureImplementation(ContractFailureKind kind, String displayMessage, String userMessage, String conditionText, Exception innerException);
#endregion Implementation Stubs
}
} // namespace System.Diagnostics.Contracts.Internal
// File provided for Reference Use Only by Microsoft Corporation (c) 2007.
// ==++==
//
// Copyright (c) Microsoft Corporation. All rights reserved.
//
// ==--==
/*============================================================
**
** Class: Contract
**
** [....],mbarnett
**
** Purpose: The contract class allows for expressing preconditions,
** postconditions, and object invariants about methods in source
** code for runtime checking & static analysis.
**
** Two classes (Contract and ContractHelper) are split into partial classes
** in order to share the public front for multiple platforms (this file)
** while providing separate implementation details for each platform.
**
===========================================================*/
#define DEBUG // The behavior of this contract library should be consistent regardless of build type.
#if SILVERLIGHT
#define FEATURE_UNTRUSTED_CALLERS
#elif REDHAWK_RUNTIME
#elif BARTOK_RUNTIME
#else // CLR
#define FEATURE_UNTRUSTED_CALLERS
#define FEATURE_RELIABILITY_CONTRACTS
#define FEATURE_SERIALIZATION
#endif
using System;
using System.Collections.Generic;
using System.Diagnostics.CodeAnalysis;
#if FEATURE_RELIABILITY_CONTRACTS
using System.Runtime.ConstrainedExecution;
#endif
#if FEATURE_UNTRUSTED_CALLERS
using System.Security;
using System.Security.Permissions;
#endif
namespace System.Diagnostics.Contracts {
#region Attributes
///
/// Methods and classes marked with this attribute can be used within calls to Contract methods. Such methods not make any visible state changes.
///
[Conditional("CONTRACTS_FULL")]
[AttributeUsage(AttributeTargets.Constructor | AttributeTargets.Method | AttributeTargets.Property | AttributeTargets.Event | AttributeTargets.Delegate | AttributeTargets.Class | AttributeTargets.Parameter, AllowMultiple = false, Inherited = true)]
public sealed class PureAttribute : Attribute
{
}
///
/// Types marked with this attribute specify that a separate type contains the contracts for this type.
///
[Conditional("CONTRACTS_FULL")]
[Conditional("DEBUG")] // Hack: For createBclSmall, make sure to include contract classes in AMD64DBG builds.
[AttributeUsage(AttributeTargets.Class | AttributeTargets.Interface | AttributeTargets.Delegate, AllowMultiple = false, Inherited = false)]
public sealed class ContractClassAttribute : Attribute
{
private Type _typeWithContracts;
public ContractClassAttribute(Type typeContainingContracts)
{
_typeWithContracts = typeContainingContracts;
}
public Type TypeContainingContracts {
get { return _typeWithContracts; }
}
}
///
/// Types marked with this attribute specify that they are a contract for the type that is the argument of the constructor.
///
[Conditional("CONTRACTS_FULL")]
[AttributeUsage(AttributeTargets.Class, AllowMultiple = false, Inherited = false)]
public sealed class ContractClassForAttribute : Attribute
{
private Type _typeIAmAContractFor;
public ContractClassForAttribute(Type typeContractsAreFor)
{
_typeIAmAContractFor = typeContractsAreFor;
}
public Type TypeContractsAreFor {
get { return _typeIAmAContractFor; }
}
}
///
/// This attribute is used to mark a method as being the invariant
/// method for a class. The method can have any name, but it must
/// return "void" and take no parameters. The body of the method
/// must consist solely of one or more calls to the method
/// Contract.Invariant. A suggested name for the method is
/// "ObjectInvariant".
///
[Conditional("CONTRACTS_FULL")]
[AttributeUsage(AttributeTargets.Method, AllowMultiple = false, Inherited = false)]
public sealed class ContractInvariantMethodAttribute : Attribute
{
}
///
/// Attribute that specifies that an assembly is a reference assembly with contracts.
///
[AttributeUsage(AttributeTargets.Assembly)]
public sealed class ContractReferenceAssemblyAttribute : Attribute
{
}
///
/// Methods (and properties) marked with this attribute can be used within calls to Contract methods, but have no runtime behavior associated with them.
///
[Conditional("CONTRACTS_FULL")]
[AttributeUsage(AttributeTargets.Method | AttributeTargets.Property, AllowMultiple = false, Inherited = true)]
public sealed class ContractRuntimeIgnoredAttribute : Attribute
{
}
/*
#if FEATURE_SERIALIZATION
[Serializable]
#endif
internal enum Mutability
{
Immutable, // read-only after construction, except for lazy initialization & caches
// Do we need a "deeply immutable" value?
Mutable,
HasInitializationPhase, // read-only after some point.
// Do we need a value for mutable types with read-only wrapper subclasses?
}
// Note: This hasn't been thought through in any depth yet. Consider it experimental.
// We should replace this with Joe's concepts.
[Conditional("CONTRACTS_FULL")]
[AttributeUsage(AttributeTargets.Class | AttributeTargets.Struct, AllowMultiple = false, Inherited = false)]
[SuppressMessage("Microsoft.Design", "CA1019:DefineAccessorsForAttributeArguments", Justification = "Thank you very much, but we like the names we've defined for the accessors")]
internal sealed class MutabilityAttribute : Attribute
{
private Mutability _mutabilityMarker;
public MutabilityAttribute(Mutability mutabilityMarker)
{
_mutabilityMarker = mutabilityMarker;
}
public Mutability Mutability {
get { return _mutabilityMarker; }
}
}
*/
///
/// Instructs downstream tools whether to assume the correctness of this assembly, type or member without performing any verification or not.
/// Can use [ContractVerification(false)] to explicitly mark assembly, type or member as one to *not* have verification performed on it.
/// Most specific element found (member, type, then assembly) takes precedence.
/// (That is useful if downstream tools allow a user to decide which polarity is the default, unmarked case.)
///
///
/// Apply this attribute to a type to apply to all members of the type, including nested types.
/// Apply this attribute to an assembly to apply to all types and members of the assembly.
/// Apply this attribute to a property to apply to both the getter and setter.
///
[Conditional("CONTRACTS_FULL")]
[AttributeUsage(AttributeTargets.Assembly | AttributeTargets.Class | AttributeTargets.Struct | AttributeTargets.Method | AttributeTargets.Constructor | AttributeTargets.Property)]
public sealed class ContractVerificationAttribute : Attribute
{
private bool _value;
public ContractVerificationAttribute(bool value) { _value = value; }
public bool Value {
get { return _value; }
}
}
///
/// Allows a field f to be used in the method contracts for a method m when f has less visibility than m.
/// For instance, if the method is public, but the field is private.
///
[Conditional("CONTRACTS_FULL")]
[AttributeUsage(AttributeTargets.Field)]
[SuppressMessage("Microsoft.Design", "CA1019:DefineAccessorsForAttributeArguments", Justification = "Thank you very much, but we like the names we've defined for the accessors")]
public sealed class ContractPublicPropertyNameAttribute : Attribute
{
private String _publicName;
public ContractPublicPropertyNameAttribute(String name)
{
_publicName = name;
}
public String Name {
get { return _publicName; }
}
}
#endregion Attributes
///
/// Contains static methods for representing program contracts such as preconditions, postconditions, and invariants.
///
///
/// WARNING: A binary rewriter must be used to insert runtime enforcement of these contracts.
/// Otherwise some contracts like Ensures can only be checked statically and will not throw exceptions during runtime when contracts are violated.
/// Please note this class uses conditional compilation to help avoid easy mistakes. Defining the preprocessor
/// symbol CONTRACTS_PRECONDITIONS will include all preconditions expressed using Contract.Requires in your
/// build. The symbol CONTRACTS_FULL will include postconditions and object invariants, and requires the binary rewriter.
///
public static partial class Contract
{
#region User Methods
#region Assume
///
/// Instructs code analysis tools to assume the expression
/// Expression to assume will always be true.
///
/// At runtime this is equivalent to an
[Pure]
[Conditional("DEBUG")]
[Conditional("CONTRACTS_FULL")]
#if FEATURE_RELIABILITY_CONTRACTS
[ReliabilityContract(Consistency.WillNotCorruptState, Cer.MayFail)]
#endif
public static void Assume(bool condition)
{
if (!condition) {
ReportFailure(ContractFailureKind.Assume, null, null, null);
}
}
///
/// Instructs code analysis tools to assume the expression
/// Expression to assume will always be true.
/// If it is not a constant string literal, then the contract may not be understood by tools.
///
/// At runtime this is equivalent to an
[Pure]
[Conditional("DEBUG")]
[Conditional("CONTRACTS_FULL")]
#if FEATURE_RELIABILITY_CONTRACTS
[ReliabilityContract(Consistency.WillNotCorruptState, Cer.MayFail)]
#endif
public static void Assume(bool condition, String userMessage)
{
if (!condition) {
ReportFailure(ContractFailureKind.Assume, userMessage, null, null);
}
}
#endregion Assume
#region Assert
///
/// In debug builds, perform a runtime check that
/// Expression to check to always be true.
[Pure]
[Conditional("DEBUG")]
[Conditional("CONTRACTS_FULL")]
#if FEATURE_RELIABILITY_CONTRACTS
[ReliabilityContract(Consistency.WillNotCorruptState, Cer.MayFail)]
#endif
public static void Assert(bool condition)
{
if (!condition)
ReportFailure(ContractFailureKind.Assert, null, null, null);
}
///
/// In debug builds, perform a runtime check that
/// Expression to check to always be true.
/// If it is not a constant string literal, then the contract may not be understood by tools.
[Pure]
[Conditional("DEBUG")]
[Conditional("CONTRACTS_FULL")]
#if FEATURE_RELIABILITY_CONTRACTS
[ReliabilityContract(Consistency.WillNotCorruptState, Cer.MayFail)]
#endif
public static void Assert(bool condition, String userMessage)
{
if (!condition)
ReportFailure(ContractFailureKind.Assert, userMessage, null, null);
}
#endregion Assert
#region Requires
///
/// Specifies a contract such that the expression
/// Boolean expression representing the contract.
///
/// This call must happen at the beginning of a method or property before any other code.
/// This contract is exposed to clients so must only reference members at least as visible as the enclosing method.
/// Use this form when backward compatibility does not force you to throw a particular exception.
///
[Pure]
[Conditional("CONTRACTS_FULL")]
#if FEATURE_RELIABILITY_CONTRACTS
[ReliabilityContract(Consistency.WillNotCorruptState, Cer.MayFail)]
#endif
public static void Requires(bool condition)
{
AssertMustUseRewriter(ContractFailureKind.Precondition, "Requires");
}
///
/// Specifies a contract such that the expression
/// Boolean expression representing the contract.
/// If it is not a constant string literal, then the contract may not be understood by tools.
///
/// This call must happen at the beginning of a method or property before any other code.
/// This contract is exposed to clients so must only reference members at least as visible as the enclosing method.
/// Use this form when backward compatibility does not force you to throw a particular exception.
///
[Pure]
[Conditional("CONTRACTS_FULL")]
#if FEATURE_RELIABILITY_CONTRACTS
[ReliabilityContract(Consistency.WillNotCorruptState, Cer.MayFail)]
#endif
public static void Requires(bool condition, String userMessage)
{
AssertMustUseRewriter(ContractFailureKind.Precondition, "Requires");
}
///
/// Specifies a contract such that the expression
/// Boolean expression representing the contract.
///
/// This call must happen at the beginning of a method or property before any other code.
/// This contract is exposed to clients so must only reference members at least as visible as the enclosing method.
/// Use this form when you want to throw a particular exception.
///
[SuppressMessage("Microsoft.Usage", "CA1801:ReviewUnusedParameters", MessageId = "condition")]
[SuppressMessage("Microsoft.Design", "CA1004:GenericMethodsShouldProvideTypeParameter")]
[Pure]
#if FEATURE_RELIABILITY_CONTRACTS
[ReliabilityContract(Consistency.WillNotCorruptState, Cer.MayFail)]
#endif
public static void Requires(bool condition) where TException : Exception
{
AssertMustUseRewriter(ContractFailureKind.Precondition, "Requires");
}
///
/// Specifies a contract such that the expression
/// Boolean expression representing the contract.
/// If it is not a constant string literal, then the contract may not be understood by tools.
///
/// This call must happen at the beginning of a method or property before any other code.
/// This contract is exposed to clients so must only reference members at least as visible as the enclosing method.
/// Use this form when you want to throw a particular exception.
///
[SuppressMessage("Microsoft.Usage", "CA1801:ReviewUnusedParameters", MessageId = "userMessage")]
[SuppressMessage("Microsoft.Usage", "CA1801:ReviewUnusedParameters", MessageId = "condition")]
[SuppressMessage("Microsoft.Design", "CA1004:GenericMethodsShouldProvideTypeParameter")]
[Pure]
#if FEATURE_RELIABILITY_CONTRACTS
[ReliabilityContract(Consistency.WillNotCorruptState, Cer.MayFail)]
#endif
public static void Requires(bool condition, String userMessage) where TException : Exception
{
AssertMustUseRewriter(ContractFailureKind.Precondition, "Requires");
}
#endregion Requires
#region Ensures
///
/// Specifies a public contract such that the expression
/// Boolean expression representing the contract. May include
/// This call must happen at the beginning of a method or property before any other code.
/// This contract is exposed to clients so must only reference members at least as visible as the enclosing method.
/// The contract rewriter must be used for runtime enforcement of this postcondition.
///
[Pure]
[Conditional("CONTRACTS_FULL")]
#if FEATURE_RELIABILITY_CONTRACTS
[ReliabilityContract(Consistency.WillNotCorruptState, Cer.MayFail)]
#endif
public static void Ensures(bool condition)
{
AssertMustUseRewriter(ContractFailureKind.Postcondition, "Ensures");
}
///
/// Specifies a public contract such that the expression
/// Boolean expression representing the contract. May include
/// This call must happen at the beginning of a method or property before any other code.
/// This contract is exposed to clients so must only reference members at least as visible as the enclosing method.
/// The contract rewriter must be used for runtime enforcement of this postcondition.
///
[Pure]
[Conditional("CONTRACTS_FULL")]
#if FEATURE_RELIABILITY_CONTRACTS
[ReliabilityContract(Consistency.WillNotCorruptState, Cer.MayFail)]
#endif
public static void Ensures(bool condition, String userMessage)
{
AssertMustUseRewriter(ContractFailureKind.Postcondition, "Ensures");
}
///
/// Specifies a contract such that if an exception of type
/// Type of exception related to this postcondition.
/// Boolean expression representing the contract. May include
/// This call must happen at the beginning of a method or property before any other code.
/// This contract is exposed to clients so must only reference types and members at least as visible as the enclosing method.
/// The contract rewriter must be used for runtime enforcement of this postcondition.
///
[Pure]
[Conditional("CONTRACTS_FULL")]
[SuppressMessage("Microsoft.Design", "CA1004:GenericMethodsShouldProvideTypeParameter", Justification = "Exception type used in tools.")]
#if FEATURE_RELIABILITY_CONTRACTS
[ReliabilityContract(Consistency.WillNotCorruptState, Cer.MayFail)]
#endif
public static void EnsuresOnThrow(bool condition) where TException : Exception
{
AssertMustUseRewriter(ContractFailureKind.PostconditionOnException, "EnsuresOnThrow");
}
///
/// Specifies a contract such that if an exception of type
/// Type of exception related to this postcondition.
/// Boolean expression representing the contract. May include
/// This call must happen at the beginning of a method or property before any other code.
/// This contract is exposed to clients so must only reference types and members at least as visible as the enclosing method.
/// The contract rewriter must be used for runtime enforcement of this postcondition.
///
[Pure]
[Conditional("CONTRACTS_FULL")]
[SuppressMessage("Microsoft.Design", "CA1004:GenericMethodsShouldProvideTypeParameter", Justification = "Exception type used in tools.")]
#if FEATURE_RELIABILITY_CONTRACTS
[ReliabilityContract(Consistency.WillNotCorruptState, Cer.MayFail)]
#endif
public static void EnsuresOnThrow(bool condition, String userMessage) where TException : Exception
{
AssertMustUseRewriter(ContractFailureKind.PostconditionOnException, "EnsuresOnThrow");
}
#region Old, Result, and Out Parameters
///
/// Represents the result (a.k.a. return value) of a method or property.
///
/// Type of return value of the enclosing method or property.
/// Return value of the enclosing method or property.
///
/// This method can only be used within the argument to the
[SuppressMessage("Microsoft.Design", "CA1004:GenericMethodsShouldProvideTypeParameter", Justification = "Not intended to be called at runtime.")]
[Pure]
#if FEATURE_RELIABILITY_CONTRACTS
[ReliabilityContract(Consistency.WillNotCorruptState, Cer.Success)]
#endif
public static T Result() { return default(T); }
///
/// Represents the final (output) value of an out parameter when returning from a method.
///
/// Type of the out parameter.
/// The out parameter.
/// The output value of the out parameter.
///
/// This method can only be used within the argument to the
[SuppressMessage("Microsoft.Design", "CA1021:AvoidOutParameters", MessageId = "0#", Justification = "Not intended to be called at runtime.")]
[Pure]
#if FEATURE_RELIABILITY_CONTRACTS
[ReliabilityContract(Consistency.WillNotCorruptState, Cer.Success)]
#endif
public static T ValueAtReturn(out T value) { value = default(T); return value; }
///
/// Represents the value of
/// Type of
/// Value to represent. This must be a field or parameter.
/// Value of
///
/// This method can only be used within the argument to the
[SuppressMessage("Microsoft.Usage", "CA1801:ReviewUnusedParameters", MessageId = "value")]
[Pure]
#if FEATURE_RELIABILITY_CONTRACTS
[ReliabilityContract(Consistency.WillNotCorruptState, Cer.Success)]
#endif
public static T OldValue(T value) { return default(T); }
#endregion Old, Result, and Out Parameters
#endregion Ensures
#region Invariant
///
/// Specifies a contract such that the expression
/// Boolean expression representing the contract.
///
/// This contact can only be specified in a dedicated invariant method declared on a class.
/// This contract is not exposed to clients so may reference members less visible as the enclosing method.
/// The contract rewriter must be used for runtime enforcement of this invariant.
///
[Pure]
[Conditional("CONTRACTS_FULL")]
#if FEATURE_RELIABILITY_CONTRACTS
[ReliabilityContract(Consistency.WillNotCorruptState, Cer.MayFail)]
#endif
public static void Invariant(bool condition)
{
AssertMustUseRewriter(ContractFailureKind.Invariant, "Invariant");
}
///
/// Specifies a contract such that the expression
/// Boolean expression representing the contract.
/// If it is not a constant string literal, then the contract may not be understood by tools.
///
/// This contact can only be specified in a dedicated invariant method declared on a class.
/// This contract is not exposed to clients so may reference members less visible as the enclosing method.
/// The contract rewriter must be used for runtime enforcement of this invariant.
///
[Pure]
[Conditional("CONTRACTS_FULL")]
#if FEATURE_RELIABILITY_CONTRACTS
[ReliabilityContract(Consistency.WillNotCorruptState, Cer.MayFail)]
#endif
public static void Invariant(bool condition, String userMessage)
{
AssertMustUseRewriter(ContractFailureKind.Invariant, "Invariant");
}
#endregion Invariant
#region Quantifiers
#region ForAll
///
/// Returns whether the true
/// for all integers starting from
/// First integer to pass to true if true for all integers
/// starting from predicate)
{
if (fromInclusive > toExclusive)
#if INSIDE_CLR
throw new ArgumentException(Environment.GetResourceString("Argument_ToExclusiveLessThanFromExclusive"));
#else
throw new ArgumentException("fromInclusive must be less than or equal to toExclusive.");
#endif
if (predicate == null)
throw new ArgumentNullException("predicate");
Contract.EndContractBlock();
for (int i = fromInclusive; i < toExclusive; i++)
if (!predicate(i)) return false;
return true;
}
///
/// Returns whether the true
/// for all elements in the
/// The collection from which elements will be drawn from to pass to true if and only if true for all elements in
/// (IEnumerable collection, Predicate predicate)
{
if (collection == null)
throw new ArgumentNullException("collection");
if (predicate == null)
throw new ArgumentNullException("predicate");
Contract.EndContractBlock();
foreach (T t in collection)
if (!predicate(t)) return false;
return true;
}
#endregion ForAll
#region Exists
///
/// Returns whether the true
/// for any integer starting from
/// First integer to pass to true if true for any integer
/// starting from predicate)
{
if (fromInclusive > toExclusive)
#if INSIDE_CLR
throw new ArgumentException(Environment.GetResourceString("Argument_ToExclusiveLessThanFromExclusive"));
#else
throw new ArgumentException("fromInclusive must be less than or equal to toExclusive.");
#endif
if (predicate == null)
throw new ArgumentNullException("predicate");
Contract.EndContractBlock();
for (int i = fromInclusive; i < toExclusive; i++)
if (predicate(i)) return true;
return false;
}
///
/// Returns whether the true
/// for any element in the
/// The collection from which elements will be drawn from to pass to true if and only if true for an element in
/// (IEnumerable collection, Predicate predicate)
{
if (collection == null)
throw new ArgumentNullException("collection");
if (predicate == null)
throw new ArgumentNullException("predicate");
Contract.EndContractBlock();
foreach (T t in collection)
if (predicate(t)) return true;
return false;
}
#endregion Exists
#endregion Quantifiers
#region Pointers
// @
#if FEATURE_UNSAFE_CONTRACTS
///
/// Runtime checking for pointer bounds is not currently feasible. Thus, at runtime, we just return
/// a very long extent for each pointer that is writable. As long as assertions are of the form
/// WritableBytes(ptr) >= ..., the runtime assertions will not fail.
/// The runtime value is 2^64 - 1 or 2^32 - 1.
///
[SuppressMessage("Microsoft.Performance", "CA1802", Justification = "FxCop is confused")]
static readonly ulong MaxWritableExtent = (UIntPtr.Size == 4) ? UInt32.MaxValue : UInt64.MaxValue;
///
/// Allows specifying a writable extent for a UIntPtr, similar to SAL's writable extent.
/// NOTE: this is for static checking only. No useful runtime code can be generated for this
/// at the moment.
///
/// Start of memory region
/// The result is the number of bytes writable starting at
[CLSCompliant(false)]
[Pure]
[ContractRuntimeIgnored]
#if FEATURE_RELIABILITY_CONTRACTS
[ReliabilityContract(Consistency.WillNotCorruptState, Cer.MayFail)]
#endif
public static ulong WritableBytes(UIntPtr startAddress) { return MaxWritableExtent - startAddress.ToUInt64(); }
///
/// Allows specifying a writable extent for a UIntPtr, similar to SAL's writable extent.
/// NOTE: this is for static checking only. No useful runtime code can be generated for this
/// at the moment.
///
/// Start of memory region
/// The result is the number of bytes writable starting at
[CLSCompliant(false)]
[Pure]
[ContractRuntimeIgnored]
#if FEATURE_RELIABILITY_CONTRACTS
[ReliabilityContract(Consistency.WillNotCorruptState, Cer.MayFail)]
#endif
public static ulong WritableBytes(IntPtr startAddress) { return MaxWritableExtent - (ulong)startAddress; }
///
/// Allows specifying a writable extent for a UIntPtr, similar to SAL's writable extent.
/// NOTE: this is for static checking only. No useful runtime code can be generated for this
/// at the moment.
///
/// Start of memory region
/// The result is the number of bytes writable starting at
[CLSCompliant(false)]
[Pure]
[ContractRuntimeIgnored]
[SecurityCritical]
#if FEATURE_RELIABILITY_CONTRACTS
[ReliabilityContract(Consistency.WillNotCorruptState, Cer.MayFail)]
#endif
//@
unsafe public static ulong WritableBytes(void* startAddress) { return MaxWritableExtent - (ulong)startAddress; }
///
/// Allows specifying a readable extent for a UIntPtr, similar to SAL's readable extent.
/// NOTE: this is for static checking only. No useful runtime code can be generated for this
/// at the moment.
///
/// Start of memory region
/// The result is the number of bytes readable starting at
[CLSCompliant(false)]
[Pure]
[ContractRuntimeIgnored]
#if FEATURE_RELIABILITY_CONTRACTS
[ReliabilityContract(Consistency.WillNotCorruptState, Cer.MayFail)]
#endif
public static ulong ReadableBytes(UIntPtr startAddress) { return MaxWritableExtent - startAddress.ToUInt64(); }
///
/// Allows specifying a readable extent for a UIntPtr, similar to SAL's readable extent.
/// NOTE: this is for static checking only. No useful runtime code can be generated for this
/// at the moment.
///
/// Start of memory region
/// The result is the number of bytes readable starting at
[CLSCompliant(false)]
[Pure]
[ContractRuntimeIgnored]
#if FEATURE_RELIABILITY_CONTRACTS
[ReliabilityContract(Consistency.WillNotCorruptState, Cer.MayFail)]
#endif
public static ulong ReadableBytes(IntPtr startAddress) { return MaxWritableExtent - (ulong)startAddress; }
///
/// Allows specifying a readable extent for a UIntPtr, similar to SAL's readable extent.
/// NOTE: this is for static checking only. No useful runtime code can be generated for this
/// at the moment.
///
/// Start of memory region
/// The result is the number of bytes readable starting at
[CLSCompliant(false)]
[Pure]
[ContractRuntimeIgnored]
[SecurityCritical]
#if FEATURE_RELIABILITY_CONTRACTS
[ReliabilityContract(Consistency.WillNotCorruptState, Cer.MayFail)]
#endif
unsafe public static ulong ReadableBytes(void* startAddress) { return MaxWritableExtent - (ulong)startAddress; }
#endif // FEATURE_UNSAFE_CONTRACTS
#endregion
#region Misc.
///
/// Marker to indicate the end of the contract section of a method.
///
[Conditional("CONTRACTS_FULL")]
#if FEATURE_RELIABILITY_CONTRACTS
[ReliabilityContract(Consistency.WillNotCorruptState, Cer.Success)]
#endif
public static void EndContractBlock() { }
#endregion
#endregion User Methods
#region Failure Behavior
///
/// Without contract rewriting, failing Assert/Assumes end up calling this method.
/// Code going through the contract rewriter never calls this method. Instead, the rewriter produced failures call
/// Internal.ContractHelper.RaiseContractFailedEvent, followed by Internal.ContractHelper.TriggerFailure.
///
static partial void ReportFailure(ContractFailureKind failureKind, String userMessage, String conditionText, Exception innerException);
///
/// This method is used internally to trigger a failure indicating to the "programmer" that he is using the interface incorrectly.
/// It is NEVER used to indicate failure of actual contracts at runtime.
///
static partial void AssertMustUseRewriter(ContractFailureKind kind, String contractKind);
#endregion
}
public enum ContractFailureKind {
Precondition,
[SuppressMessage("Microsoft.Naming", "CA1704:IdentifiersShouldBeSpelledCorrectly", MessageId = "Postcondition")]
Postcondition,
[SuppressMessage("Microsoft.Naming", "CA1704:IdentifiersShouldBeSpelledCorrectly", MessageId = "Postcondition")]
PostconditionOnException,
Invariant,
Assert,
Assume,
}
}
namespace System.Diagnostics.Contracts.Internal
{
public static partial class ContractHelper
{
#region Rewriter Failure Hooks
///
/// Rewriter will call this method on a contract failure to allow listeners to be notified.
/// The method should not perform any failure (assert/throw) itself.
///
/// null if the event was handled and should not trigger a failure.
/// Otherwise, returns the localized failure message
[SuppressMessage("Microsoft.Design", "CA1030:UseEventsWhereAppropriate")]
#if FEATURE_UNTRUSTED_CALLERS
[SuppressMessage("Microsoft.Portability", "CA1903:UseOnlyApiFromTargetedFramework", MessageId = "System.Security.SecuritySafeCriticalAttribute")]
[SecuritySafeCritical]
#endif
[System.Diagnostics.DebuggerNonUserCode]
#if FEATURE_RELIABILITY_CONTRACTS
[ReliabilityContract(Consistency.WillNotCorruptState, Cer.MayFail)]
#endif
public static string RaiseContractFailedEvent(ContractFailureKind failureKind, String userMessage, String conditionText, Exception innerException)
{
var resultFailureMessage = "Contract failed"; // default in case implementation does not assign anything.
RaiseContractFailedEventImplementation(failureKind, userMessage, conditionText, innerException, ref resultFailureMessage);
return resultFailureMessage;
}
///
/// Rewriter calls this method to get the default failure behavior.
///
#if FEATURE_UNTRUSTED_CALLERS
[SecuritySafeCritical]
#endif
[System.Diagnostics.DebuggerNonUserCode]
#if FEATURE_RELIABILITY_CONTRACTS
[ReliabilityContract(Consistency.WillNotCorruptState, Cer.Success)]
#endif
public static void TriggerFailure(ContractFailureKind kind, String displayMessage, String userMessage, String conditionText, Exception innerException)
{
TriggerFailureImplementation(kind, displayMessage, userMessage, conditionText, innerException);
}
#endregion Rewriter Failure Hooks
#region Implementation Stubs
///
/// Rewriter will call this method on a contract failure to allow listeners to be notified.
/// The method should not perform any failure (assert/throw) itself.
/// This method has 3 functions:
/// 1. Call any contract hooks (such as listeners to Contract failed events)
/// 2. Determine if the listeneres deem the failure as handled (then resultFailureMessage should be set to null)
/// 3. Produce a localized resultFailureMessage used in advertising the failure subsequently.
///
/// Should really be out (or the return value), but partial methods are not flexible enough.
/// On exit: null if the event was handled and should not trigger a failure.
/// Otherwise, returns the localized failure message
static partial void RaiseContractFailedEventImplementation(ContractFailureKind failureKind, String userMessage, String conditionText, Exception innerException, ref string resultFailureMessage);
///
/// Implements the default failure behavior of the platform. Under the BCL, it triggers an Assert box.
///
static partial void TriggerFailureImplementation(ContractFailureKind kind, String displayMessage, String userMessage, String conditionText, Exception innerException);
#endregion Implementation Stubs
}
} // namespace System.Diagnostics.Contracts.Internal
// File provided for Reference Use Only by Microsoft Corporation (c) 2007.
Link Menu
This book is available now!
Buy at Amazon US or
Buy at Amazon UK
- ImageDrawing.cs
- MissingMemberException.cs
- Int32EqualityComparer.cs
- cookie.cs
- FilterElement.cs
- ListSortDescriptionCollection.cs
- CollectionViewGroupRoot.cs
- TraceContext.cs
- BitmapEffectGroup.cs
- ClickablePoint.cs
- LazyLoadBehavior.cs
- AutoResizedEvent.cs
- FrameAutomationPeer.cs
- TextRenderer.cs
- MessageDesigner.cs
- ImageMetadata.cs
- HttpMethodAttribute.cs
- MergeFailedEvent.cs
- SettingsProviderCollection.cs
- ClientScriptManager.cs
- PackageStore.cs
- SystemIPv6InterfaceProperties.cs
- StyleXamlTreeBuilder.cs
- Perspective.cs
- AnimationStorage.cs
- DesignBinding.cs
- basecomparevalidator.cs
- ReferenceAssemblyAttribute.cs
- WebCategoryAttribute.cs
- DirectoryObjectSecurity.cs
- FixedFindEngine.cs
- ShellProvider.cs
- Point3DConverter.cs
- ProcessHostFactoryHelper.cs
- ZipIOBlockManager.cs
- BindingManagerDataErrorEventArgs.cs
- ContractMapping.cs
- ForeignKeyConstraint.cs
- SeekStoryboard.cs
- MULTI_QI.cs
- ContractComponent.cs
- PeerSecurityManager.cs
- TemplateBindingExpressionConverter.cs
- XmlWrappingReader.cs
- SqlSelectStatement.cs
- RoutedCommand.cs
- RowsCopiedEventArgs.cs
- SessionStateUtil.cs
- InstanceKeyNotReadyException.cs
- oledbmetadatacolumnnames.cs
- TdsParameterSetter.cs
- SqlConnectionString.cs
- DataSvcMapFileSerializer.cs
- AssemblyResourceLoader.cs
- CodeTypeParameter.cs
- VBCodeProvider.cs
- InkCanvas.cs
- FieldAccessException.cs
- PointF.cs
- ObjectFactoryCodeDomTreeGenerator.cs
- LinqExpressionNormalizer.cs
- DataGridViewComboBoxCell.cs
- ViewStateException.cs
- NonClientArea.cs
- StreamInfo.cs
- XPathChildIterator.cs
- AutomationPatternInfo.cs
- UiaCoreTypesApi.cs
- UInt32Converter.cs
- PipelineModuleStepContainer.cs
- ShaderEffect.cs
- UncommonField.cs
- FileDialog.cs
- DetailsViewDeleteEventArgs.cs
- DataAdapter.cs
- LoginUtil.cs
- RenderDataDrawingContext.cs
- FrameworkName.cs
- DSASignatureFormatter.cs
- DropSource.cs
- OverrideMode.cs
- ClientScriptItem.cs
- ConnectionProviderAttribute.cs
- EmbeddedMailObjectCollectionEditor.cs
- XmlSchemaDocumentation.cs
- SQLInt32Storage.cs
- Label.cs
- SafeNativeMethods.cs
- EnumUnknown.cs
- StandardToolWindows.cs
- UndirectedGraph.cs
- Utils.cs
- TypeElementCollection.cs
- Translator.cs
- UniqueIdentifierService.cs
- Pkcs7Signer.cs
- sqlinternaltransaction.cs
- RSACryptoServiceProvider.cs
- SortExpressionBuilder.cs
- ProfileEventArgs.cs