diff options
| author |  rustanleino <unknown> | 2011-01-13 01:20:30 +0000 |
|---|---|---|
| committer | rustanleino <unknown> | 2011-01-13 01:20:30 +0000 |
| commit | 4a3b3e6d50109c4f39c33f8d5af68d329e2b1354 (patch) | |
| tree | dc9bf39607e301232b598f92ed70eb104b7aa454 /Source/DafnyDriver | |
| parent | ee4867783495bba5a4d2041990cba5ebf4067078 (diff) | |
Dafny: Fixed some build issues with duplicated and malformed Code Contracts.
Diffstat (limited to 'Source/DafnyDriver')
| -rw-r--r-- | Source/DafnyDriver/DafnyDriver.csproj | 1 | ||||
| -rw-r--r-- | Source/DafnyDriver/cce.cs | 104 |
2 files changed, 0 insertions, 105 deletions
diff --git a/Source/DafnyDriver/DafnyDriver.csproj b/Source/DafnyDriver/DafnyDriver.csproj index d577c048..fb68eefd 100644 --- a/Source/DafnyDriver/DafnyDriver.csproj +++ b/Source/DafnyDriver/DafnyDriver.csproj @@ -110,7 +110,6 @@ </Reference>
</ItemGroup>
<ItemGroup>
- <Compile Include="cce.cs" />
<Compile Include="DafnyDriver.cs" />
<Compile Include="..\version.cs" />
</ItemGroup>
diff --git a/Source/DafnyDriver/cce.cs b/Source/DafnyDriver/cce.cs deleted file mode 100644 index 34749b5f..00000000 --- a/Source/DafnyDriver/cce.cs +++ /dev/null @@ -1,104 +0,0 @@ -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);
- }
- [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) {
- }
-}
\ No newline at end of file |