From f513d6f3716b7c963e30ca3d004cf6a40d2f68c5 Mon Sep 17 00:00:00 2001 From: tabarbe Date: Fri, 30 Jul 2010 23:51:12 +0000 Subject: Boogie: The deletion of those files did not hold, lemme try again. --- Source/Provers/Simplify/cce.cs | 82 ------------------------------------------ 1 file changed, 82 deletions(-) delete mode 100644 Source/Provers/Simplify/cce.cs (limited to 'Source/Provers/Simplify') diff --git a/Source/Provers/Simplify/cce.cs b/Source/Provers/Simplify/cce.cs deleted file mode 100644 index 1799d4ab..00000000 --- a/Source/Provers/Simplify/cce.cs +++ /dev/null @@ -1,82 +0,0 @@ -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); - } - public class UnreachableException : Exception { - public UnreachableException() { - } - } - [Pure] - public static void BeginExpose(object o) { - } - [Pure] - public static void EndExpose() { - } - public static bool IsPeerConsistent(object o) { - return true; - } - public static bool IsConsistent(object o) { - return true; - } - public static bool IsExposable(object o) { - return true; - } - internal static bool IsExposed(object o) { - return true; - } - public static class Owner { - [Pure] - public static bool Same(object o, object p) { - return true; - } - public static void AssignSame(object o, object p) { - } - public static object ElementProxy(object o) { - return o; - } - public static bool None(object o) { - return true; - } - } - internal static void LoopInvariant(bool p) { - Contract.Assert(p); - } -} - -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 { -} \ No newline at end of file -- cgit v1.2.3