From 962f8d5252b3f5ec4d19e0cd2a430934bd55cc6d Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Sun, 28 Jun 2015 01:44:30 +0100 Subject: Normalise line endings using a .gitattributes file. Unfortunately this required that this commit globally modify most files. If you want to use git blame to see the real author of a line use the ``-w`` flag so that whitespace changes are ignored. --- .../CodeContractsExtender.csproj | 404 ++++++++++----------- Source/CodeContractsExtender/cce.cs | 366 +++++++++---------- 2 files changed, 385 insertions(+), 385 deletions(-) (limited to 'Source/CodeContractsExtender') diff --git a/Source/CodeContractsExtender/CodeContractsExtender.csproj b/Source/CodeContractsExtender/CodeContractsExtender.csproj index c87ed8ab..05701c12 100644 --- a/Source/CodeContractsExtender/CodeContractsExtender.csproj +++ b/Source/CodeContractsExtender/CodeContractsExtender.csproj @@ -1,202 +1,202 @@ - - - - Debug - AnyCPU - 9.0.30729 - 2.0 - {ACCC0156-0921-43ED-8F67-AD8BDC8CDE31} - Library - Properties - CodeContractsExtender - CodeContractsExtender - v4.0 - 512 - true - ..\InterimKey.snk - 1 - - - 3.5 - - publish\ - true - Disk - false - Foreground - 7 - Days - false - false - true - 0 - 1.0.0.%2a - false - false - true - Client - - - true - full - false - bin\Debug\ - DEBUG;TRACE - prompt - 4 - False - False - True - False - False - False - False - False - False - False - False - True - False - False - False - - - - - - - - - - - - - Full - %28none%29 - AllRules.ruleset - - - pdbonly - true - bin\Release\ - TRACE - prompt - 4 - AllRules.ruleset - - - true - bin\z3apidebug\ - DEBUG;TRACE - full - AnyCPU - - - true - GlobalSuppressions.cs - prompt - Migrated rules for CodeContractsExtender.ruleset - true - 4 - false - - - true - bin\Checked\ - DEBUG;TRACE - full - AnyCPU - bin\Debug\CodeContractsExtender.dll.CodeAnalysisLog.xml - true - GlobalSuppressions.cs - prompt - AllRules.ruleset - ;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets - ;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules - True - False - True - False - False - False - False - False - False - False - False - False - True - False - False - False - - - - - - - False - Full - Build - 0 - 4 - false - - - true - bin\QED\ - DEBUG;TRACE - full - AnyCPU - prompt - AllRules.ruleset - - - - - 3.5 - - - 3.5 - - - 3.5 - - - - - - - version.cs - - - - - - - - - False - .NET Framework 3.5 SP1 Client Profile - false - - - False - .NET Framework 3.5 SP1 - true - - - False - Windows Installer 3.1 - true - - - - - + + + + Debug + AnyCPU + 9.0.30729 + 2.0 + {ACCC0156-0921-43ED-8F67-AD8BDC8CDE31} + Library + Properties + CodeContractsExtender + CodeContractsExtender + v4.0 + 512 + true + ..\InterimKey.snk + 1 + + + 3.5 + + publish\ + true + Disk + false + Foreground + 7 + Days + false + false + true + 0 + 1.0.0.%2a + false + false + true + Client + + + true + full + false + bin\Debug\ + DEBUG;TRACE + prompt + 4 + False + False + True + False + False + False + False + False + False + False + False + True + False + False + False + + + + + + + + + + + + + Full + %28none%29 + AllRules.ruleset + + + pdbonly + true + bin\Release\ + TRACE + prompt + 4 + AllRules.ruleset + + + true + bin\z3apidebug\ + DEBUG;TRACE + full + AnyCPU + + + true + GlobalSuppressions.cs + prompt + Migrated rules for CodeContractsExtender.ruleset + true + 4 + false + + + true + bin\Checked\ + DEBUG;TRACE + full + AnyCPU + bin\Debug\CodeContractsExtender.dll.CodeAnalysisLog.xml + true + GlobalSuppressions.cs + prompt + AllRules.ruleset + ;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets + ;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules + True + False + True + False + False + False + False + False + False + False + False + False + True + False + False + False + + + + + + + False + Full + Build + 0 + 4 + false + + + true + bin\QED\ + DEBUG;TRACE + full + AnyCPU + prompt + AllRules.ruleset + + + + + 3.5 + + + 3.5 + + + 3.5 + + + + + + + version.cs + + + + + + + + + False + .NET Framework 3.5 SP1 Client Profile + false + + + False + .NET Framework 3.5 SP1 + true + + + False + Windows Installer 3.1 + true + + + + + diff --git a/Source/CodeContractsExtender/cce.cs b/Source/CodeContractsExtender/cce.cs index 02b80458..0e6a0607 100644 --- a/Source/CodeContractsExtender/cce.cs +++ b/Source/CodeContractsExtender/cce.cs @@ -1,184 +1,184 @@ -using System; -using SA=System.Attribute; -using System.Collections.Generic; -using System.Diagnostics.Contracts; -using System.Text; -//using Microsoft.Boogie; - -/// -/// A class containing static methods to extend the functionality of Code Contracts -/// - -public static class cce { - //[Pure] - //public static bool NonNullElements(Microsoft.Dafny.Graph collection) { - // return collection != null && cce.NonNullElements(collection.TopologicallySortedComponents()); - //} - [Pure] - public static T NonNull(T t) where T : class { - Contract.Requires(t != null); - Contract.Ensures(Contract.Result() != null); - return t; - } - [Pure] - public static bool NonNullElements(IEnumerable collection) where T : class { - return collection != null && Contract.ForAll(collection, c => c != null); - } - [Pure] - public static bool NonNullDictionaryAndValues(IDictionary collection) where TValue : class { - return collection != null && cce.NonNullElements(collection.Values); - } - //[Pure] - //public static bool NonNullElements(List collection) { - // return collection != null && Contract.ForAll(0, collection.Length, i => collection[i] != null); - //} - /// - /// For possibly-null lists of non-null elements - /// - /// - /// - /// If true, the collection is treated as an IEnumerable<T!>?, rather than an IEnumerable<T!>! - /// - [Pure] - public static bool NonNullElements(IEnumerable collection, bool nullability) where T : class { - return (nullability && collection == null) || cce.NonNullElements(collection); - //Should be the same as: - /*if(nullability&&collection==null) - * return true; - * return cce.NonNullElements(collection) - */ - - } - [Pure] - public static bool NonNullElements(KeyValuePair kvp) where TKey : class where TValue : class { - return kvp.Key != null && kvp.Value != null; - } - [Pure] - public static bool NonNullElements(IEnumerator iEnumerator) where T : class { - return iEnumerator != null; - } - [Pure] - public static bool NonNull(HashSet set) where T : class { - return set != null && !set.Contains(null); - } - //[Pure] - //public static bool NonNullElements(Graphing.Graph graph) { - // return cce.NonNullElements(graph.TopologicalSort()); - //} - [Pure] - public static void BeginExpose(object o) { - } - [Pure] - public static void EndExpose() { - } - [Pure] - public static bool IsPeerConsistent(object o) { - return true; - } - [Pure] - public static bool IsConsistent(object o) { - return true; - } - [Pure] - public static bool IsExposable(object o) { - return true; - } - [Pure] - public static bool IsExposed(object o) { - return true; - } - [Pure] - public static bool IsNew(object o) { - return true; - } - public static class Owner { - [Pure] - public static bool Same(object o, object p) { - return true; - } - [Pure] - public static void AssignSame(object o, object p) { - } - [Pure] - public static object ElementProxy(object o) { - return o; - } - [Pure] - public static bool None(object o) { - return true; - } - [Pure] - public static bool Different(object o, object p) { - return true; - } - [Pure] - public static bool New(object o) { - return true; - } - } - [Pure] - public static void LoopInvariant(bool p) { - Contract.Assert(p); - } - public class UnreachableException : Exception { - public UnreachableException() { - } - } - -} - -public class PeerAttribute : SA { -} -public class RepAttribute : SA { -} -public class CapturedAttribute : SA { -} -public class NotDelayedAttribute : SA { -} -public class NoDefaultContractAttribute : SA { -} -public class VerifyAttribute : SA { - public VerifyAttribute(bool b) { - - } -} -public class StrictReadonlyAttribute : SA { -} -public class AdditiveAttribute : SA { -} -public class ReadsAttribute : SA { - public enum Reads { - Nothing, - Everything, - }; - public ReadsAttribute(object o) { - } -} -public class GlobalAccessAttribute : SA { - public GlobalAccessAttribute(bool b) { - } -} -public class EscapesAttribute : SA { - public EscapesAttribute(bool b, bool b_2) { - } -} -public class NeedsContractsAttribute : SA { - public NeedsContractsAttribute() { - } - public NeedsContractsAttribute(bool ret, bool parameters) { - } - public NeedsContractsAttribute(bool ret, int[] parameters) { - } -} -public class ImmutableAttribute : SA { -} -public class InsideAttribute : SA { -} -public class SpecPublicAttribute : SA { -} -public class ElementsPeerAttribute : SA { -} -public class ResultNotNewlyAllocatedAttribute : SA { -} -public class OnceAttribute : SA { +using System; +using SA=System.Attribute; +using System.Collections.Generic; +using System.Diagnostics.Contracts; +using System.Text; +//using Microsoft.Boogie; + +/// +/// A class containing static methods to extend the functionality of Code Contracts +/// + +public static class cce { + //[Pure] + //public static bool NonNullElements(Microsoft.Dafny.Graph collection) { + // return collection != null && cce.NonNullElements(collection.TopologicallySortedComponents()); + //} + [Pure] + public static T NonNull(T t) where T : class { + Contract.Requires(t != null); + Contract.Ensures(Contract.Result() != null); + return t; + } + [Pure] + public static bool NonNullElements(IEnumerable collection) where T : class { + return collection != null && Contract.ForAll(collection, c => c != null); + } + [Pure] + public static bool NonNullDictionaryAndValues(IDictionary collection) where TValue : class { + return collection != null && cce.NonNullElements(collection.Values); + } + //[Pure] + //public static bool NonNullElements(List collection) { + // return collection != null && Contract.ForAll(0, collection.Length, i => collection[i] != null); + //} + /// + /// For possibly-null lists of non-null elements + /// + /// + /// + /// If true, the collection is treated as an IEnumerable<T!>?, rather than an IEnumerable<T!>! + /// + [Pure] + public static bool NonNullElements(IEnumerable collection, bool nullability) where T : class { + return (nullability && collection == null) || cce.NonNullElements(collection); + //Should be the same as: + /*if(nullability&&collection==null) + * return true; + * return cce.NonNullElements(collection) + */ + + } + [Pure] + public static bool NonNullElements(KeyValuePair kvp) where TKey : class where TValue : class { + return kvp.Key != null && kvp.Value != null; + } + [Pure] + public static bool NonNullElements(IEnumerator iEnumerator) where T : class { + return iEnumerator != null; + } + [Pure] + public static bool NonNull(HashSet set) where T : class { + return set != null && !set.Contains(null); + } + //[Pure] + //public static bool NonNullElements(Graphing.Graph graph) { + // return cce.NonNullElements(graph.TopologicalSort()); + //} + [Pure] + public static void BeginExpose(object o) { + } + [Pure] + public static void EndExpose() { + } + [Pure] + public static bool IsPeerConsistent(object o) { + return true; + } + [Pure] + public static bool IsConsistent(object o) { + return true; + } + [Pure] + public static bool IsExposable(object o) { + return true; + } + [Pure] + public static bool IsExposed(object o) { + return true; + } + [Pure] + public static bool IsNew(object o) { + return true; + } + public static class Owner { + [Pure] + public static bool Same(object o, object p) { + return true; + } + [Pure] + public static void AssignSame(object o, object p) { + } + [Pure] + public static object ElementProxy(object o) { + return o; + } + [Pure] + public static bool None(object o) { + return true; + } + [Pure] + public static bool Different(object o, object p) { + return true; + } + [Pure] + public static bool New(object o) { + return true; + } + } + [Pure] + public static void LoopInvariant(bool p) { + Contract.Assert(p); + } + public class UnreachableException : Exception { + public UnreachableException() { + } + } + +} + +public class PeerAttribute : SA { +} +public class RepAttribute : SA { +} +public class CapturedAttribute : SA { +} +public class NotDelayedAttribute : SA { +} +public class NoDefaultContractAttribute : SA { +} +public class VerifyAttribute : SA { + public VerifyAttribute(bool b) { + + } +} +public class StrictReadonlyAttribute : SA { +} +public class AdditiveAttribute : SA { +} +public class ReadsAttribute : SA { + public enum Reads { + Nothing, + Everything, + }; + public ReadsAttribute(object o) { + } +} +public class GlobalAccessAttribute : SA { + public GlobalAccessAttribute(bool b) { + } +} +public class EscapesAttribute : SA { + public EscapesAttribute(bool b, bool b_2) { + } +} +public class NeedsContractsAttribute : SA { + public NeedsContractsAttribute() { + } + public NeedsContractsAttribute(bool ret, bool parameters) { + } + public NeedsContractsAttribute(bool ret, int[] parameters) { + } +} +public class ImmutableAttribute : SA { +} +public class InsideAttribute : SA { +} +public class SpecPublicAttribute : SA { +} +public class ElementsPeerAttribute : SA { +} +public class ResultNotNewlyAllocatedAttribute : SA { +} +public class OnceAttribute : SA { } \ No newline at end of file -- cgit v1.2.3