From 6de3f9c9f86be13bbd4f0bd6e4edf7d7785db0a4 Mon Sep 17 00:00:00 2001
From: tabarbe <unknown>
Date: Fri, 27 Aug 2010 17:23:51 +0000
Subject: Boogie: Changed the cce classes into one separate project, which
 every other project in the Boogie solution references.  Dafny.csproj has an
 internal copy of cce, so does not reference this project, because the Dafny
 cce uses some Dafny-defined types in its helper methods.

---
 .../CodeContractsExtender.csproj                   |  67 +++++++
 Source/CodeContractsExtender/cce.cs                | 193 +++++++++++++++++++++
 2 files changed, 260 insertions(+)
 create mode 100644 Source/CodeContractsExtender/CodeContractsExtender.csproj
 create mode 100644 Source/CodeContractsExtender/cce.cs

(limited to 'Source/CodeContractsExtender')

diff --git a/Source/CodeContractsExtender/CodeContractsExtender.csproj b/Source/CodeContractsExtender/CodeContractsExtender.csproj
new file mode 100644
index 00000000..46edbd5e
--- /dev/null
+++ b/Source/CodeContractsExtender/CodeContractsExtender.csproj
@@ -0,0 +1,67 @@
+<?xml version="1.0" encoding="utf-8"?>
+<Project ToolsVersion="3.5" DefaultTargets="Build" xmlns="http://schemas.microsoft.com/developer/msbuild/2003">
+  <PropertyGroup>
+    <Configuration Condition=" '$(Configuration)' == '' ">Debug</Configuration>
+    <Platform Condition=" '$(Platform)' == '' ">AnyCPU</Platform>
+    <ProductVersion>9.0.30729</ProductVersion>
+    <SchemaVersion>2.0</SchemaVersion>
+    <ProjectGuid>{ACCC0156-0921-43ED-8F67-AD8BDC8CDE31}</ProjectGuid>
+    <OutputType>Library</OutputType>
+    <AppDesignerFolder>Properties</AppDesignerFolder>
+    <RootNamespace>CodeContractsExtender</RootNamespace>
+    <AssemblyName>CodeContractsExtender</AssemblyName>
+    <TargetFrameworkVersion>v3.5</TargetFrameworkVersion>
+    <FileAlignment>512</FileAlignment>
+    <SignAssembly>true</SignAssembly>
+    <AssemblyOriginatorKeyFile>..\InterimKey.snk</AssemblyOriginatorKeyFile>
+  </PropertyGroup>
+  <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Debug|AnyCPU' ">
+    <DebugSymbols>true</DebugSymbols>
+    <DebugType>full</DebugType>
+    <Optimize>false</Optimize>
+    <OutputPath>bin\Debug\</OutputPath>
+    <DefineConstants>DEBUG;TRACE</DefineConstants>
+    <ErrorReport>prompt</ErrorReport>
+    <WarningLevel>4</WarningLevel>
+  </PropertyGroup>
+  <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Release|AnyCPU' ">
+    <DebugType>pdbonly</DebugType>
+    <Optimize>true</Optimize>
+    <OutputPath>bin\Release\</OutputPath>
+    <DefineConstants>TRACE</DefineConstants>
+    <ErrorReport>prompt</ErrorReport>
+    <WarningLevel>4</WarningLevel>
+  </PropertyGroup>
+  <ItemGroup>
+    <Reference Include="Microsoft.Contracts, Version=1.0.0.0, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">
+      <SpecificVersion>False</SpecificVersion>
+      <HintPath>..\..\Binaries\Microsoft.Contracts.dll</HintPath>
+    </Reference>
+    <Reference Include="System" />
+    <Reference Include="System.Core">
+      <RequiredTargetFramework>3.5</RequiredTargetFramework>
+    </Reference>
+    <Reference Include="System.Xml.Linq">
+      <RequiredTargetFramework>3.5</RequiredTargetFramework>
+    </Reference>
+    <Reference Include="System.Data.DataSetExtensions">
+      <RequiredTargetFramework>3.5</RequiredTargetFramework>
+    </Reference>
+    <Reference Include="System.Data" />
+    <Reference Include="System.Xml" />
+  </ItemGroup>
+  <ItemGroup>
+    <Compile Include="cce.cs" />
+  </ItemGroup>
+  <ItemGroup>
+    <Folder Include="Properties\" />
+  </ItemGroup>
+  <Import Project="$(MSBuildToolsPath)\Microsoft.CSharp.targets" />
+  <!-- To modify your build process, add your task inside one of the targets below and uncomment it. 
+       Other similar extension points exist, see Microsoft.Common.targets.
+  <Target Name="BeforeBuild">
+  </Target>
+  <Target Name="AfterBuild">
+  </Target>
+  -->
+</Project>
\ No newline at end of file
diff --git a/Source/CodeContractsExtender/cce.cs b/Source/CodeContractsExtender/cce.cs
new file mode 100644
index 00000000..ef594484
--- /dev/null
+++ b/Source/CodeContractsExtender/cce.cs
@@ -0,0 +1,193 @@
+using System;
+using SA=System.Attribute;
+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 bool NonNullElements<T>(Microsoft.Dafny.Graph<T> collection) {
+  //  return collection != null && cce.NonNullElements(collection.TopologicallySortedComponents());
+  //}
+  [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 && 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);
+  //}
+  /// <summary>
+  /// For possibly-null lists of non-null elements
+  /// </summary>
+  /// <typeparam name="T"></typeparam>
+  /// <param name="collection"></param>
+  /// <param name="nullability">If true, the collection is treated as an IEnumerable&lt;T!&gt;?, rather than an IEnumerable&lt;T!&gt;!</param>
+  /// <returns></returns>
+  [Pure]
+  public static bool NonNullElements<T>(IEnumerable<T> 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<TKey, TValue>(KeyValuePair<TKey, TValue> kvp) {
+    return kvp.Key != null && kvp.Value != null;
+  }
+  [Pure]
+  public static bool NonNullElements<T>(IEnumerator<T> iEnumerator) {
+    return iEnumerator != null;
+  }
+  //[Pure]
+  //public static bool NonNullElements<T>(Graphing.Graph<T> graph) {
+  //  return cce.NonNullElements(graph.TopologicalSort());
+  //}
+  [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;
+  }
+  [Pure]
+  public static bool IsNew(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 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() {
+    }
+  }
+  //[Pure]
+  //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;
+  //}
+
+  //internal static bool NonNullElements(Set set) {
+  //  return set != null && Contract.ForAll(0,set.Count, i => set[i] != null);
+  //}
+}
+
+public class PeerAttribute : SA {
+}
+public class RepAttribute : SA {
+}
+public class CapturedAttribute : SA {
+}
+public class NotDelayedAttribute : SA {
+}
+public class NoDefaultContractAttribute : SA {
+}
+public class VerifyAttribute : SA {
+  public VerifyAttribute(bool b) {
+
+  }
+}
+public class StrictReadonlyAttribute : SA {
+}
+public class AdditiveAttribute : SA {
+}
+public class ReadsAttribute : SA {
+  public enum Reads {
+    Nothing,
+    Everything,
+  };
+  public ReadsAttribute(object o) {
+  }
+}
+public class GlobalAccessAttribute : SA {
+  public GlobalAccessAttribute(bool b) {
+  }
+}
+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