From 0faac5618039d3617b676c24e9465f712072adf3 Mon Sep 17 00:00:00 2001 From: tabarbe Date: Fri, 27 Aug 2010 00:29:15 +0000 Subject: 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. --- Source/VCExpr/VCExpr.csproj | 1 + Source/VCExpr/cce.cs | 117 ++++++++++++++++++++++++++++++++++---------- 2 files changed, 91 insertions(+), 27 deletions(-) (limited to 'Source/VCExpr') diff --git a/Source/VCExpr/VCExpr.csproj b/Source/VCExpr/VCExpr.csproj index 05b12234..b2f61e8c 100644 --- a/Source/VCExpr/VCExpr.csproj +++ b/Source/VCExpr/VCExpr.csproj @@ -75,6 +75,7 @@ + diff --git a/Source/VCExpr/cce.cs b/Source/VCExpr/cce.cs index ff619b7c..ef594484 100644 --- a/Source/VCExpr/cce.cs +++ b/Source/VCExpr/cce.cs @@ -1,14 +1,19 @@ using System; +using SA=System.Attribute; using System.Collections.Generic; using System.Diagnostics.Contracts; using System.Text; -using Microsoft.Boogie; +//using Microsoft.Boogie; - /// - /// A class containing static methods to extend the functionality of Code Contracts - /// +/// +/// A class containing static methods to extend the functionality of Code Contracts +/// public static class cce { + //[Pure] + //public static bool NonNullElements(Microsoft.Dafny.Graph collection) { + // return collection != null && cce.NonNullElements(collection.TopologicallySortedComponents()); + //} [Pure] public static T NonNull(T t) { Contract.Assert(t != null); @@ -22,20 +27,39 @@ public static class cce { public static bool NonNullElements(IDictionary 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(Microsoft.Dafny.Graph collection) { - // return collection != null && cce.NonNullElements(collection.TopologicallySortedComponents()); + //public static bool NonNullElements(VariableSeq collection) { + // return collection != null && Contract.ForAll(0, collection.Length, i => collection[i] != null); //} + /// + /// For possibly-null lists of non-null elements + /// + /// + /// + /// If true, the collection is treated as an IEnumerable<T!>?, rather than an IEnumerable<T!>! + /// + [Pure] + public static bool NonNullElements(IEnumerable collection, bool nullability) { + return (nullability && collection == null) || cce.NonNullElements(collection); + //Should be the same as: + /*if(nullability&&collection==null) + * return true; + * return cce.NonNullElements(collection) + */ + } [Pure] public static bool NonNullElements(KeyValuePair kvp) { return kvp.Key != null && kvp.Value != null; } - + [Pure] + public static bool NonNullElements(IEnumerator iEnumerator) { + return iEnumerator != null; + } + //[Pure] + //public static bool NonNullElements(Graphing.Graph graph) { + // return cce.NonNullElements(graph.TopologicalSort()); + //} [Pure] public static void BeginExpose(object o) { } @@ -58,6 +82,10 @@ public static class cce { public static bool IsExposed(object o) { return true; } + [Pure] + public static bool IsNew(object o) { + return true; + } public static class Owner { [Pure] public static bool Same(object o, object p) { @@ -74,12 +102,19 @@ public static class cce { public static bool None(object o) { return true; } + [Pure] + public static bool Different(object o, object p) { + return true; + } + [Pure] + public static bool New(object o) { + return true; + } } [Pure] public static void LoopInvariant(bool p) { Contract.Assert(p); } - public class UnreachableException : Exception { public UnreachableException() { } @@ -88,43 +123,71 @@ public static class cce { //public static bool IsValid(Microsoft.Dafny.Expression expression) { // return true; //} + //public static List toList(PureCollections.Sequence s) { + // List toRet = new List(); + // foreach (T t in s.elems) + // if(t!=null) + // toRet.Add(t); + // return toRet; + //} - internal static bool NonNullElements(IEnumerator iEnumerator) { - return iEnumerator != null; - } + //internal static bool NonNullElements(Set set) { + // return set != null && Contract.ForAll(0,set.Count, i => set[i] != null); + //} } -public class PeerAttribute : System.Attribute { +public class PeerAttribute : SA { } -public class RepAttribute : System.Attribute { +public class RepAttribute : SA { } -public class CapturedAttribute : System.Attribute { +public class CapturedAttribute : SA { } -public class NotDelayedAttribute : System.Attribute { +public class NotDelayedAttribute : SA { } -public class NoDefaultContractAttribute : System.Attribute { +public class NoDefaultContractAttribute : SA { } -public class VerifyAttribute : System.Attribute { +public class VerifyAttribute : SA { public VerifyAttribute(bool b) { } } -public class StrictReadonlyAttribute : System.Attribute { - } -public class AdditiveAttribute : System.Attribute { +public class StrictReadonlyAttribute : SA { +} +public class AdditiveAttribute : SA { } -public class ReadsAttribute : System.Attribute { +public class ReadsAttribute : SA { public enum Reads { Nothing, + Everything, }; public ReadsAttribute(object o) { } } -public class GlobalAccessAttribute : System.Attribute { +public class GlobalAccessAttribute : SA { public GlobalAccessAttribute(bool b) { } } -public class EscapesAttribute : System.Attribute { +public class EscapesAttribute : SA { public EscapesAttribute(bool b, bool b_2) { } +} +public class NeedsContractsAttribute : SA { + public NeedsContractsAttribute() { + } + public NeedsContractsAttribute(bool ret, bool parameters) { + } + public NeedsContractsAttribute(bool ret, int[] parameters) { + } +} +public class ImmutableAttribute : SA { +} +public class InsideAttribute : SA { +} +public class SpecPublicAttribute : SA { +} +public class ElementsPeerAttribute : SA { +} +public class ResultNotNewlyAllocatedAttribute : SA { +} +public class OnceAttribute : SA { } \ No newline at end of file -- cgit v1.2.3