summaryrefslogtreecommitdiff
path: root/Source/AbsInt/cce.cs
diff options
context:
space:
mode:
Diffstat (limited to 'Source/AbsInt/cce.cs')
-rw-r--r--Source/AbsInt/cce.cs124
1 files changed, 62 insertions, 62 deletions
diff --git a/Source/AbsInt/cce.cs b/Source/AbsInt/cce.cs
index 693d608c..627add75 100644
--- a/Source/AbsInt/cce.cs
+++ b/Source/AbsInt/cce.cs
@@ -1,62 +1,62 @@
-
-using System;
-using System.Collections.Generic;
-using System.Diagnostics.Contracts;
-using System.Text;
-using Microsoft.Boogie;
-
- /// <summary>
- /// A class containing static methods to extend the functionality of Code Contracts
- /// </summary>
-
-public static class cce {
- [Pure]
- public static T NonNull<T>(T t) {
- Contract.Assert(t != null);
- return t;
- }
- [Pure]
- public static bool NonNullElements<T>(IEnumerable<T> collection) {
- return collection != null && Contract.ForAll(collection, c => c != null);
- }
- [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(this object o) {
- return true;
- }
-
- public static bool IsConsistent(this object o) {
- return true;
- }
-
- public static bool IsExposable(this object o) {
- return true;
- }
- public static class Owner {
- [Pure]
- public static bool Same(object o, object p) {
- return true;
- }
- }
-}
-public class PeerAttribute : System.Attribute {
-}
-public class RepAttribute : System.Attribute {
-}
-public class CapturedAttribute : System.Attribute {
-}
+
+using System;
+using System.Collections.Generic;
+using System.Diagnostics.Contracts;
+using System.Text;
+using Microsoft.Boogie;
+
+ /// <summary>
+ /// A class containing static methods to extend the functionality of Code Contracts
+ /// </summary>
+
+public static class cce {
+ [Pure]
+ public static T NonNull<T>(T t) {
+ Contract.Assert(t != null);
+ return t;
+ }
+ [Pure]
+ public static bool NonNullElements<T>(IEnumerable<T> collection) {
+ return collection != null && Contract.ForAll(collection, c => c != null);
+ }
+ [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(this object o) {
+ return true;
+ }
+
+ public static bool IsConsistent(this object o) {
+ return true;
+ }
+
+ public static bool IsExposable(this object o) {
+ return true;
+ }
+ public static class Owner {
+ [Pure]
+ public static bool Same(object o, object p) {
+ return true;
+ }
+ }
+}
+public class PeerAttribute : System.Attribute {
+}
+public class RepAttribute : System.Attribute {
+}
+public class CapturedAttribute : System.Attribute {
+}