Boogie: Changed BoogieDriver.cs to use a copy of cce.cs, rather than an internal cce.cs class.

3 files changed, 114 insertions, 23 deletions

diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs
index f8216069..aeb0f627 100644
--- a/Source/BoogieDriver/BoogieDriver.cs
+++ b/Source/BoogieDriver/BoogieDriver.cs
@@ -35,7 +35,7 @@ namespace Microsoft.Boogie {
     // Main

 

     public static void Main(string[] args) {

-      Contract.Requires(NonNullElements(args));

+      Contract.Requires(cce.NonNullElements(args));

       CommandLineOptions.Clo.RunningBoogieFromCommandLine = true;

       if (CommandLineOptions.Clo.Parse(args) != 1) {

         goto END;

@@ -187,7 +187,7 @@ namespace Microsoft.Boogie {
         kind = "Error";

       }

       if (node.SourceContext.Document != null) {

-        return string.Format("{0}({1},{2}): {3}: {4}", Path.GetFileName(NonNull(node.SourceContext.Document.Name)), node.SourceContext.StartLine, node.SourceContext.StartColumn, kind, message);

+        return string.Format("{0}({1},{2}): {3}: {4}", Path.GetFileName(cce.NonNull(node.SourceContext.Document.Name)), node.SourceContext.StartLine, node.SourceContext.StartColumn, kind, message);

       } else {

         return string.Format("{0}: {1}", kind, message);

       }

@@ -223,7 +223,7 @@ namespace Microsoft.Boogie {
     }

 

     static void ProcessFiles(List<string> fileNames) {

-      Contract.Requires(NonNullElements(fileNames));

+      Contract.Requires(cce.NonNullElements(fileNames));

       using (XmlFileScope xf = new XmlFileScope(CommandLineOptions.Clo.XmlSink, fileNames[fileNames.Count - 1])) {

         //BoogiePL.Errors.count = 0;

         Program program = ParseBoogieProgram(fileNames, false);

@@ -280,7 +280,7 @@ namespace Microsoft.Boogie {
       Contract.Requires(program != null);

       // We inspect the last declaration because the first comes from the prelude and therefore always has source context.

       return program.TopLevelDeclarations.Count > 0 &&

-          ((NonNull(program.TopLevelDeclarations)[program.TopLevelDeclarations.Count - 1]).tok.IsValid);

+          ((cce.NonNull(program.TopLevelDeclarations)[program.TopLevelDeclarations.Count - 1]).tok.IsValid);

     }

 

 

@@ -354,7 +354,7 @@ namespace Microsoft.Boogie {
     /// and null will be returned.  On success, a non-null program is returned.

     /// </summary>

     static Program ParseBoogieProgram(List<string> fileNames, bool suppressTraceOutput) {

-      Contract.Requires(NonNullElements(fileNames));

+      Contract.Requires(cce.NonNullElements(fileNames));

       //BoogiePL.Errors.count = 0;

       Program program = null;

       bool okay = true;

@@ -467,7 +467,7 @@ namespace Microsoft.Boogie {
 

       // Inline

       // In Spec#, there was no run-time test. The type was just List<Declaration!>

-      List<Declaration> TopLevelDeclarations = NonNull(program.TopLevelDeclarations);

+      List<Declaration> TopLevelDeclarations = cce.NonNull(program.TopLevelDeclarations);

       

       

       if (CommandLineOptions.Clo.ProcedureInlining != CommandLineOptions.Inlining.None) {

@@ -568,7 +568,7 @@ namespace Microsoft.Boogie {
       foreach (Declaration decl in program.TopLevelDeclarations) {

         Contract.Assert(decl != null);

         Implementation impl = decl as Implementation;

-        if (impl != null && CommandLineOptions.Clo.UserWantsToCheckRoutine(NonNull(impl.Name)) && !impl.SkipVerification) {

+        if (impl != null && CommandLineOptions.Clo.UserWantsToCheckRoutine(cce.NonNull(impl.Name)) && !impl.SkipVerification) {

           //TODO: Resolve arraylist nonnulls

           List<Counterexample/*!*/>/*?*/ errors;

 

@@ -611,7 +611,7 @@ namespace Microsoft.Boogie {
           switch (outcome) {

             default:

               Contract.Assert(false);  // unexpected outcome

-              throw new UnreachableException();

+              throw new cce.UnreachableException();

             case VCGen.Outcome.Correct:

               if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Doomed) {

                 Inform(String.Format("{0}credible", timeIndication));

@@ -729,27 +729,13 @@ namespace Microsoft.Boogie {
         }

       }

       vcgen.Close();

-      NonNull(CommandLineOptions.Clo.TheProverFactory).Close();

+      cce.NonNull(CommandLineOptions.Clo.TheProverFactory).Close();

 

 

       #endregion

 

       return PipelineOutcome.VerificationCompleted;

     }

-    [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);

-    }

-

-    public class UnreachableException : Exception {

-      public UnreachableException() {

-      }

-    }

 

   }

 }
\ No newline at end of file
diff --git a/Source/BoogieDriver/BoogieDriver.csproj b/Source/BoogieDriver/BoogieDriver.csproj
index f5684a2b..3a6f44ab 100644
--- a/Source/BoogieDriver/BoogieDriver.csproj
+++ b/Source/BoogieDriver/BoogieDriver.csproj
@@ -87,6 +87,7 @@
   <ItemGroup>

     <Compile Include="BoogieDriver.cs" />

     <Compile Include="..\version.cs" />

+    <Compile Include="cce.cs" />

   </ItemGroup>

   <ItemGroup>

     <ProjectReference Include="..\AbsInt\AbsInt.csproj">

diff --git a/Source/BoogieDriver/cce.cs b/Source/BoogieDriver/cce.cs
new file mode 100644
index 00000000..34749b5f
--- /dev/null
+++ b/Source/BoogieDriver/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