From d652155ae013f36a1ee17653a8e458baad2d9c2c Mon Sep 17 00:00:00 2001 From: Checkmate50 Date: Mon, 6 Jun 2016 23:14:18 -0600 Subject: Merging complete. Everything looks good *crosses fingers* --- Source/BoogieDriver/cce.cs | 210 ++++++++++++++++++++++----------------------- 1 file changed, 105 insertions(+), 105 deletions(-) (limited to 'Source/BoogieDriver/cce.cs') diff --git a/Source/BoogieDriver/cce.cs b/Source/BoogieDriver/cce.cs index 23d79815..42cabfcb 100644 --- a/Source/BoogieDriver/cce.cs +++ b/Source/BoogieDriver/cce.cs @@ -1,105 +1,105 @@ - -using System; -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 T NonNull(T t) { - Contract.Assert(t != null); - return t; - } - [Pure] - public static bool NonNullElements(IEnumerable collection) { - return collection != null && Contract.ForAll(collection, c => c != null); - } - [Pure] - public static bool NonNullElements(IDictionary collection) { - return collection != null && NonNullElements(collection.Keys) && NonNullElements(collection.Values); - } - [Pure] - public static bool NonNullElements(VariableSeq collection) { - return collection != null && Contract.ForAll(0, collection.Length, i => collection[i] != null); - } - [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; - } - 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 void LoopInvariant(bool p) { - Contract.Assert(p); - } - - public class UnreachableException : Exception { - public UnreachableException() { - } - } -} - -public class PeerAttribute : System.Attribute { -} -public class RepAttribute : System.Attribute { -} -public class CapturedAttribute : System.Attribute { -} -public class NotDelayedAttribute : System.Attribute { -} -public class NoDefaultContractAttribute : System.Attribute { -} -public class VerifyAttribute : System.Attribute { - public VerifyAttribute(bool b) { - - } -} -public class StrictReadonlyAttribute : System.Attribute { - } -public class AdditiveAttribute : System.Attribute { -} -public class ReadsAttribute : System.Attribute { - public enum Reads { - Nothing, - }; - public ReadsAttribute(object o) { - } -} + +using System; +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 T NonNull(T t) { + Contract.Assert(t != null); + return t; + } + [Pure] + public static bool NonNullElements(IEnumerable collection) { + return collection != null && Contract.ForAll(collection, c => c != null); + } + [Pure] + public static bool NonNullElements(IDictionary collection) { + return collection != null && NonNullElements(collection.Keys) && NonNullElements(collection.Values); + } + [Pure] + public static bool NonNullElements(VariableSeq collection) { + return collection != null && Contract.ForAll(0, collection.Length, i => collection[i] != null); + } + [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; + } + 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 void LoopInvariant(bool p) { + Contract.Assert(p); + } + + public class UnreachableException : Exception { + public UnreachableException() { + } + } +} + +public class PeerAttribute : System.Attribute { +} +public class RepAttribute : System.Attribute { +} +public class CapturedAttribute : System.Attribute { +} +public class NotDelayedAttribute : System.Attribute { +} +public class NoDefaultContractAttribute : System.Attribute { +} +public class VerifyAttribute : System.Attribute { + public VerifyAttribute(bool b) { + + } +} +public class StrictReadonlyAttribute : System.Attribute { + } +public class AdditiveAttribute : System.Attribute { +} +public class ReadsAttribute : System.Attribute { + public enum Reads { + Nothing, + }; + public ReadsAttribute(object o) { + } +} -- cgit v1.2.3