summaryrefslogtreecommitdiff
path: root/Source/Provers
diff options
context:
space:
mode:
authorGravatar tabarbe <unknown>2010-07-23 15:39:06 +0000
committerGravatar tabarbe <unknown>2010-07-23 15:39:06 +0000
commitdc34935912fb578e1cf1107f3ad0707695d2f98a (patch)
treeb48971c360521ed892272e9c24ea0bcd19b2ef6c /Source/Provers
parente42bc4dbc928260d0652f6c6575a71745b215ab5 (diff)
Boogie: AssemblyInfo.cs is no longer required for the build; cce.cs is.
Diffstat (limited to 'Source/Provers')
-rw-r--r--Source/Provers/Simplify/AssemblyInfo.cs4
-rw-r--r--Source/Provers/Simplify/cce.cs82
2 files changed, 82 insertions, 4 deletions
diff --git a/Source/Provers/Simplify/AssemblyInfo.cs b/Source/Provers/Simplify/AssemblyInfo.cs
deleted file mode 100644
index ed1d3451..00000000
--- a/Source/Provers/Simplify/AssemblyInfo.cs
+++ /dev/null
@@ -1,4 +0,0 @@
-using System.Reflection;
-using System.Runtime.CompilerServices;
-
-[assembly: AssemblyKeyFile("..\\..\\InterimKey.snk")]
diff --git a/Source/Provers/Simplify/cce.cs b/Source/Provers/Simplify/cce.cs
new file mode 100644
index 00000000..1799d4ab
--- /dev/null
+++ b/Source/Provers/Simplify/cce.cs
@@ -0,0 +1,82 @@
+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<TKey, TValue>(IDictionary<TKey, TValue> 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