diff options
| author |  tabarbe <unknown> | 2010-07-16 22:44:33 +0000 |
|---|---|---|
| committer | tabarbe <unknown> | 2010-07-16 22:44:33 +0000 |
| commit | f6f281a60449aea24b257b73cd45fd970afbc57c (patch) | |
| tree | 879f030745bf494e95624aa2878039fe5ca0dd37 /Source/AbsInt/cce.cs | |
| parent | 951ae331104cd20be6241b009ead77bef850fdb9 (diff) | |
Boogie: I have successfully ported the AbsInt project. It passes all regressions, although DAFNY NEEDS TO BE REBUILT TO RECOGNIZE the changed AbsInt DLL.
Address any error complaints to t-abarbe@microsoft.com
Diffstat (limited to 'Source/AbsInt/cce.cs')
| -rw-r--r-- | Source/AbsInt/cce.cs | 62 |
1 files changed, 62 insertions, 0 deletions
diff --git a/Source/AbsInt/cce.cs b/Source/AbsInt/cce.cs new file mode 100644 index 00000000..c8d7a4ab --- /dev/null +++ b/Source/AbsInt/cce.cs @@ -0,0 +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 {
+}
\ No newline at end of file |