Boogie: Graph port 3/3: Committing changed references; also, adding back cce files, to ease between-project conflict. Will trim these back off after commit of Basetypes port in ~20 min.

1 files changed, 18 insertions, 12 deletions

diff --git a/Source/Core/cce.cs b/Source/Core/cce.cs
index 7aade95e..ef594484 100644
--- a/Source/Core/cce.cs
+++ b/Source/Core/cce.cs
@@ -3,7 +3,7 @@ using SA=System.Attribute;
 using System.Collections.Generic;

 using System.Diagnostics.Contracts;

 using System.Text;

-using Microsoft.Boogie;

+//using Microsoft.Boogie;

 

 /// <summary>

 /// A class containing static methods to extend the functionality of Code Contracts

@@ -27,10 +27,10 @@ public static class cce {
   public static bool NonNullElements<TKey, TValue>(IDictionary<TKey, TValue> collection) {

     return collection != null && Contract.ForAll(collection, pair => NonNullElements(pair));

   }

-  [Pure]

-  public static bool NonNullElements(VariableSeq collection) {

-    return collection != null && Contract.ForAll(0, collection.Length, i => collection[i] != null);

-  }

+  //[Pure]

+  //public static bool NonNullElements(VariableSeq collection) {

+  //  return collection != null && Contract.ForAll(0, collection.Length, i => collection[i] != null);

+  //}

   /// <summary>

   /// For possibly-null lists of non-null elements

   /// </summary>

@@ -123,13 +123,17 @@ public static class cce {
   //public static bool IsValid(Microsoft.Dafny.Expression expression) {

   //  return true;

   //}

-  public static List<T> toList<T>(PureCollections.Sequence s) {

-    List<T> toRet = new List<T>();

-    foreach (T t in s.elems)

-      if(t!=null)

-      toRet.Add(t);

-    return toRet;

-  }

+  //public static List<T> toList<T>(PureCollections.Sequence s) {

+  //  List<T> toRet = new List<T>();

+  //  foreach (T t in s.elems)

+  //    if(t!=null)

+  //    toRet.Add(t);

+  //  return toRet;

+  //}

+

+  //internal static bool NonNullElements(Set set) {

+  //  return set != null && Contract.ForAll(0,set.Count, i => set[i] != null);

+  //}

 }

 

 public class PeerAttribute : SA {

@@ -184,4 +188,6 @@ public class SpecPublicAttribute : SA {
 public class ElementsPeerAttribute : SA {

 }

 public class ResultNotNewlyAllocatedAttribute : SA {

+}

+public class OnceAttribute : SA {

 }
\ No newline at end of file