diff options
| author |  tabarbe <unknown> | 2010-07-28 22:21:47 +0000 |
|---|---|---|
| committer | tabarbe <unknown> | 2010-07-28 22:21:47 +0000 |
| commit | 3150ac77d93f4279a9660ac61bab176602b22037 (patch) | |
| tree | 166d16e75344959255659d824be2404a9eb522fc | |
| parent | a8c8ffb249d39f2e2a29d3e26888e269019d6fe2 (diff) | |
Boogie: VCGeneration port part 2/3: Adding new dependent files, removing unnecessary one.
| -rw-r--r-- | Source/VCGeneration/..svnbridge/InterimKey.snk | 1 | ||||
| -rw-r--r-- | Source/VCGeneration/AssemblyInfo.ssc | 4 | ||||
| -rw-r--r-- | Source/VCGeneration/InterimKey.snk | bin | 0 -> 596 bytes | |||
| -rw-r--r-- | Source/VCGeneration/cce.cs | 104 | ||||
| -rw-r--r-- | Source/VCGeneration/version.cs | 8 |
5 files changed, 113 insertions, 4 deletions
diff --git a/Source/VCGeneration/..svnbridge/InterimKey.snk b/Source/VCGeneration/..svnbridge/InterimKey.snk new file mode 100644 index 00000000..08149303 --- /dev/null +++ b/Source/VCGeneration/..svnbridge/InterimKey.snk @@ -0,0 +1 @@ +<?xml version="1.0" encoding="utf-8"?><ItemProperties xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xmlns:xsd="http://www.w3.org/2001/XMLSchema"><Properties><Property><Name>svn:mime-type</Name><Value>application/octet-stream</Value></Property></Properties></ItemProperties>
\ No newline at end of file diff --git a/Source/VCGeneration/AssemblyInfo.ssc b/Source/VCGeneration/AssemblyInfo.ssc deleted file mode 100644 index 6ed99a25..00000000 --- a/Source/VCGeneration/AssemblyInfo.ssc +++ /dev/null @@ -1,4 +0,0 @@ -using System.Reflection;
-using System.Runtime.CompilerServices;
-
-[assembly: AssemblyKeyFile("..\\InterimKey.snk")]
diff --git a/Source/VCGeneration/InterimKey.snk b/Source/VCGeneration/InterimKey.snk Binary files differnew file mode 100644 index 00000000..8fc79508 --- /dev/null +++ b/Source/VCGeneration/InterimKey.snk diff --git a/Source/VCGeneration/cce.cs b/Source/VCGeneration/cce.cs new file mode 100644 index 00000000..34749b5f --- /dev/null +++ b/Source/VCGeneration/cce.cs @@ -0,0 +1,104 @@ +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 diff --git a/Source/VCGeneration/version.cs b/Source/VCGeneration/version.cs new file mode 100644 index 00000000..2804c330 --- /dev/null +++ b/Source/VCGeneration/version.cs @@ -0,0 +1,8 @@ +//-----------------------------------------------------------------------------
+//
+// Copyright (C) Microsoft Corporation. All Rights Reserved.
+//
+//-----------------------------------------------------------------------------
+using System.Reflection;
+[assembly: AssemblyVersion("2.0.0.0")]
+[assembly: AssemblyFileVersion("2.0.0.0")]
|