diff options
| author |  tabarbe <unknown> | 2010-08-27 17:23:51 +0000 |
|---|---|---|
| committer | tabarbe <unknown> | 2010-08-27 17:23:51 +0000 |
| commit | 6de3f9c9f86be13bbd4f0bd6e4edf7d7785db0a4 (patch) | |
| tree | 087d90276b93254a98cbd1e3c898d5b2d48af1e8 /Source/CodeContractsExtender | |
| parent | 5b3285b1261b27a5a6bdeac05ab836c0947280da (diff) | |
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.
Diffstat (limited to 'Source/CodeContractsExtender')
| -rw-r--r-- | Source/CodeContractsExtender/CodeContractsExtender.csproj | 67 | ||||
| -rw-r--r-- | Source/CodeContractsExtender/cce.cs | 193 |
2 files changed, 260 insertions, 0 deletions
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<T!>?, rather than an IEnumerable<T!>!</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 |