<Boogie> <BoogieDriver> Committing my porting of BoogieDriver.cs and the changes made to the .csproj and Boogie.sln file that are necessary for the port.

My Microsoft alias is t-abarbe, so if any of this stuff breaks for you, you can contact me.
</BoogieDriver> </Boogie>

2 files changed, 459 insertions, 424 deletions

diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs
index 74ad7b8e..f8216069 100644
--- a/Source/BoogieDriver/BoogieDriver.cs
+++ b/Source/BoogieDriver/BoogieDriver.cs
@@ -8,8 +8,7 @@
 //       - main program for taking a BPL program and verifying it

 //---------------------------------------------------------------------------------------------

 

-namespace Microsoft.Boogie 

-{

+namespace Microsoft.Boogie {

   using System;

   using System.IO;

   using System.Collections;

@@ -17,34 +16,31 @@ namespace Microsoft.Boogie
   using PureCollections;

   using Microsoft.Boogie;

   using Microsoft.Boogie.AbstractInterpretation;

+  using System.Diagnostics.Contracts;

   using System.Diagnostics;

   using VC;

   using Cci = System.Compiler;

   using AI = Microsoft.AbstractInterpretationFramework;

   using BoogiePL = Microsoft.Boogie;

 

-/* 

-  The following assemblies are referenced because they are needed at runtime, not at compile time:

-    BaseTypes

-    Provers.Z3

-    System.Compiler.Framework

-*/

+  /* 

+    The following assemblies are referenced because they are needed at runtime, not at compile time:

+      BaseTypes

+      Provers.Z3

+      System.Compiler.Framework

+  */

 

-  public class OnlyBoogie

-  {

+  public class OnlyBoogie {

     // ------------------------------------------------------------------------

     // Main

-    

-    public static void Main (string[]! args) 

-    {

-      assert forall{int i in (0:args.Length); args[i] != null};

+

+    public static void Main(string[] args) {

+      Contract.Requires(NonNullElements(args));

       CommandLineOptions.Clo.RunningBoogieFromCommandLine = true;

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

-      {

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

         goto END;

       }

-      if (CommandLineOptions.Clo.Files.Count == 0)

-      {

+      if (CommandLineOptions.Clo.Files.Count == 0) {

         ErrorWriteLine("*** Error: No input files were specified.");

         goto END;

       }

@@ -55,17 +51,16 @@ namespace Microsoft.Boogie
           goto END;

         }

       }

-      if (!CommandLineOptions.Clo.DontShowLogo)

-      {

+      if (!CommandLineOptions.Clo.DontShowLogo) {

         Console.WriteLine(CommandLineOptions.Clo.Version);

       }

-      if (CommandLineOptions.Clo.ShowEnv == CommandLineOptions.ShowEnvironment.Always) 

-      {

+      if (CommandLineOptions.Clo.ShowEnv == CommandLineOptions.ShowEnvironment.Always) {

         Console.WriteLine("---Command arguments");

-        foreach (string! arg in args) 

-        {

+        foreach (string arg in args) {

+          Contract.Assert(arg != null);

           Console.WriteLine(arg);

         }

+

         Console.WriteLine("--------------------");

       }

 

@@ -79,98 +74,111 @@ namespace Microsoft.Boogie
       // and then the types in it do not get unique representations.

       if (System.Type.GetType("Mono.Runtime") == null) {  // MONO

         Cci.AssemblyNode a = Microsoft.SpecSharp.Runtime.RuntimeAssembly;

-        assert a != null;

+        Contract.Assert(a != null);

       }

 

-      foreach (string! file in CommandLineOptions.Clo.Files) 

-      {

+      foreach (string file in CommandLineOptions.Clo.Files) {

+        Contract.Assert(file != null);

         string extension = Path.GetExtension(file);

-        if (extension != null) { extension = extension.ToLower(); }

-        if (extension != ".bpl")

-        {

-            ErrorWriteLine("*** Error: '{0}': Filename extension '{1}' is not supported. Input files must be BoogiePL programs (.bpl).", file,

-                extension == null ? "" : extension);

-            goto END;

+        if (extension != null) {

+          extension = extension.ToLower();

+        }

+        if (extension != ".bpl") {

+          ErrorWriteLine("*** Error: '{0}': Filename extension '{1}' is not supported. Input files must be BoogiePL programs (.bpl).", file,

+              extension == null ? "" : extension);

+          goto END;

         }

       }

       CommandLineOptions.Clo.RunningBoogieOnSsc = false;

       ProcessFiles(CommandLineOptions.Clo.Files);

 

-      END:

-        if (CommandLineOptions.Clo.XmlSink != null) {

-          CommandLineOptions.Clo.XmlSink.Close();

-        }

-        if (CommandLineOptions.Clo.Wait) 

-        {

-          Console.WriteLine("Press Enter to exit.");

-          Console.ReadLine();

-        }

+    END:

+      if (CommandLineOptions.Clo.XmlSink != null) {

+        CommandLineOptions.Clo.XmlSink.Close();

+      }

+      if (CommandLineOptions.Clo.Wait) {

+        Console.WriteLine("Press Enter to exit.");

+        Console.ReadLine();

+      }

     }

 

-    public static void ErrorWriteLine(string! s) {

+    public static void ErrorWriteLine(string s) {

+      Contract.Requires(s != null);

       if (!s.Contains("Error: ") && !s.Contains("Error BP")) {

         Console.WriteLine(s);

         return;

       }

-      

+

       // split the string up into its first line and the remaining lines

       string remaining = null;

       int i = s.IndexOf('\r');

       if (0 <= i) {

-        remaining = s.Substring(i+1);

+        remaining = s.Substring(i + 1);

         if (remaining.StartsWith("\n")) {

           remaining = remaining.Substring(1);

         }

         s = s.Substring(0, i);

       }

-      

+

       ConsoleColor col = Console.ForegroundColor;

       Console.ForegroundColor = ConsoleColor.Red;

       Console.WriteLine(s);

       Console.ForegroundColor = col;

-      

+

       if (remaining != null) {

         Console.WriteLine(remaining);

       }

     }

 

-    public static void ErrorWriteLine(string! format, params object[] args) {

+    public static void ErrorWriteLine(string format, params object[] args) {

+      Contract.Requires(format != null);

       string s = string.Format(format, args);

       ErrorWriteLine(s);

     }

 

-    public static void AdvisoryWriteLine(string! format, params object[] args) {

+    public static void AdvisoryWriteLine(string format, params object[] args) {

+      Contract.Requires(format != null);

       ConsoleColor col = Console.ForegroundColor;

       Console.ForegroundColor = ConsoleColor.Yellow;

       Console.WriteLine(format, args);

       Console.ForegroundColor = col;

     }

 

-	  public static void SelectPlatform(CommandLineOptions! options)

-	  {

-		  if (options.TargetPlatformLocation != null) {

-			  // Make sure static constructor runs before we start setting locations, etc.

-			  System.Compiler.SystemTypes.Clear();

-

-			  switch (options.TargetPlatform){

-			  case CommandLineOptions.PlatformType.v1: Microsoft.SpecSharp.TargetPlatform.SetToV1(options.TargetPlatformLocation); break;

-			  case CommandLineOptions.PlatformType.v11: Microsoft.SpecSharp.TargetPlatform.SetToV1_1(options.TargetPlatformLocation); break;

-			  case CommandLineOptions.PlatformType.v2: Microsoft.SpecSharp.TargetPlatform.SetToV2(options.TargetPlatformLocation); break;

-			  case CommandLineOptions.PlatformType.cli1: Microsoft.SpecSharp.TargetPlatform.SetToPostV1_1(options.TargetPlatformLocation); break;

-			  }

-  			

-			  if (options.StandardLibraryLocation != null && options.StandardLibraryLocation.Length > 0){

-				  System.Compiler.SystemAssemblyLocation.Location = options.StandardLibraryLocation;

-			  }

-			  System.Compiler.SystemCompilerRuntimeAssemblyLocation.Location = options.TargetPlatformLocation + @"\System.Compiler.Runtime.dll";

-  	            

-			  System.Compiler.SystemTypes.Initialize(true, true);

-		  }

-	  }

-	

-    static string! GetErrorLine(Cci.ErrorNode! node)

-        requires node.SourceContext.Document != null ==> node.SourceContext.Document.Name != null;

-    {

+    public static void SelectPlatform(CommandLineOptions options) {

+      Contract.Requires(options != null);

+      if (options.TargetPlatformLocation != null) {

+        // Make sure static constructor runs before we start setting locations, etc.

+        System.Compiler.SystemTypes.Clear();

+

+        switch (options.TargetPlatform) {

+          case CommandLineOptions.PlatformType.v1:

+            Microsoft.SpecSharp.TargetPlatform.SetToV1(options.TargetPlatformLocation);

+            break;

+          case CommandLineOptions.PlatformType.v11:

+            Microsoft.SpecSharp.TargetPlatform.SetToV1_1(options.TargetPlatformLocation);

+            break;

+          case CommandLineOptions.PlatformType.v2:

+            Microsoft.SpecSharp.TargetPlatform.SetToV2(options.TargetPlatformLocation);

+            break;

+          case CommandLineOptions.PlatformType.cli1:

+            Microsoft.SpecSharp.TargetPlatform.SetToPostV1_1(options.TargetPlatformLocation);

+            break;

+        }

+

+        if (options.StandardLibraryLocation != null && options.StandardLibraryLocation.Length > 0) {

+          System.Compiler.SystemAssemblyLocation.Location = options.StandardLibraryLocation;

+        }

+        System.Compiler.SystemCompilerRuntimeAssemblyLocation.Location = options.TargetPlatformLocation + @"\System.Compiler.Runtime.dll";

+

+        System.Compiler.SystemTypes.Initialize(true, true);

+      }

+    }

+

+    static string GetErrorLine(Cci.ErrorNode node) {

+      Contract.Requires(node != null);

+      Contract.Requires(node.SourceContext.Document == null || (node.SourceContext.Document.Name != null));

+      

+      Contract.Ensures(Contract.Result<string>() != null);

       string message = node.GetMessage(System.Threading.Thread.CurrentThread.CurrentUICulture);

       string kind;

       if (message.Contains("(trace position)")) {

@@ -179,48 +187,60 @@ namespace Microsoft.Boogie
         kind = "Error";

       }

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

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

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

       } else {

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

       }

+

+

     }

 

-    enum FileType { Unknown, Cil, Bpl, Dafny };

-

-    class ErrorReporter

-    {

-        public Cci.ErrorNodeList! errors = new Cci.ErrorNodeList();

-        public int errorsReported;

-        

-        public void ReportErrors()

-        {

-            //sort the portion of the array that will be reported to make output more deterministic

-            errors.Sort(errorsReported,errors.Count-errorsReported);

-            for(;errorsReported < errors.Count; errorsReported++) {

-                Cci.ErrorNode error = errors[errorsReported];

-                if (error != null)

-                    ErrorWriteLine(GetErrorLine(error));

-            } 

+    enum FileType {

+      Unknown,

+      Cil,

+      Bpl,

+      Dafny

+    };

+

+    class ErrorReporter {

+      public Cci.ErrorNodeList errors = new Cci.ErrorNodeList();

+      [ContractInvariantMethod]

+      void ObjectInvariant() {

+        Contract.Invariant(errors != null);

+      }

+

+      public int errorsReported;

+

+      public void ReportErrors() {

+        //sort the portion of the array that will be reported to make output more deterministic

+        errors.Sort(errorsReported, errors.Count - errorsReported);

+        for (; errorsReported < errors.Count; errorsReported++) {

+          Cci.ErrorNode error = errors[errorsReported];

+          if (error != null)

+            ErrorWriteLine(GetErrorLine(error));

         }

+      }

     }

 

-    static void ProcessFiles (List<string!>! fileNames)

-    {

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

+    static void ProcessFiles(List<string> fileNames) {

+      Contract.Requires(NonNullElements(fileNames));

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

         //BoogiePL.Errors.count = 0;

         Program program = ParseBoogieProgram(fileNames, false);

-        if (program == null) return;

+        if (program == null)

+          return;

         if (CommandLineOptions.Clo.PrintFile != null) {

-           PrintBplFile(CommandLineOptions.Clo.PrintFile, program, false);

+          PrintBplFile(CommandLineOptions.Clo.PrintFile, program, false);

         }

 

-        PipelineOutcome oc = ResolveAndTypecheck(program, fileNames[fileNames.Count-1]);

-        if (oc != PipelineOutcome.ResolvedAndTypeChecked) return;

+        PipelineOutcome oc = ResolveAndTypecheck(program, fileNames[fileNames.Count - 1]);

+        if (oc != PipelineOutcome.ResolvedAndTypeChecked)

+          return;

         //BoogiePL.Errors.count = 0;

-        

+

         oc = EliminateDeadVariablesAndInline(program);

         //BoogiePL.Errors.count = 0;

-        

+

         int errorCount, verified, inconclusives, timeOuts, outOfMemories;

         oc = InferAndVerify(program, null, out errorCount, out verified, out inconclusives, out timeOuts, out outOfMemories);

         switch (oc) {

@@ -233,54 +253,55 @@ namespace Microsoft.Boogie
         }

       }

     }

-    

-    

-    static void PrintBplFile (string! filename, Program! program, bool allowPrintDesugaring)

-    {

-        bool oldPrintDesugaring = CommandLineOptions.Clo.PrintDesugarings;

-        if (!allowPrintDesugaring) {

-          CommandLineOptions.Clo.PrintDesugarings = false;

-        }

-        using (TokenTextWriter writer = filename == "-" ?

-                                        new TokenTextWriter("<console>", Console.Out) :

-                                        new TokenTextWriter(filename))

-        {

-          if (CommandLineOptions.Clo.ShowEnv != CommandLineOptions.ShowEnvironment.Never) {

-            writer.WriteLine("// " + CommandLineOptions.Clo.Version);

-            writer.WriteLine("// " + CommandLineOptions.Clo.Environment);

-          }

-          writer.WriteLine();

-          program.Emit(writer);

+

+

+    static void PrintBplFile(string filename, Program program, bool allowPrintDesugaring) {

+      Contract.Requires(program != null);

+      Contract.Requires(filename != null);

+      bool oldPrintDesugaring = CommandLineOptions.Clo.PrintDesugarings;

+      if (!allowPrintDesugaring) {

+        CommandLineOptions.Clo.PrintDesugarings = false;

+      }

+      using (TokenTextWriter writer = filename == "-" ?

+                                      new TokenTextWriter("<console>", Console.Out) :

+                                      new TokenTextWriter(filename)) {

+        if (CommandLineOptions.Clo.ShowEnv != CommandLineOptions.ShowEnvironment.Never) {

+          writer.WriteLine("// " + CommandLineOptions.Clo.Version);

+          writer.WriteLine("// " + CommandLineOptions.Clo.Environment);

         }

-        CommandLineOptions.Clo.PrintDesugarings = oldPrintDesugaring;

+        writer.WriteLine();

+        program.Emit(writer);

+      }

+      CommandLineOptions.Clo.PrintDesugarings = oldPrintDesugaring;

     }

-    

-    

-    static bool ProgramHasDebugInfo (Program! program)

-    {

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

-        return program.TopLevelDeclarations.Count > 0 && 

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

+

+

+    static bool ProgramHasDebugInfo(Program program) {

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

     }

-    

-    

+

+

     /// <summary>

     /// Inform the user about something and proceed with translation normally.

     /// Print newline after the message.

     /// </summary>

     public static void Inform(string s) {

-      if ( ! CommandLineOptions.Clo.Trace) { return; }

+      if (!CommandLineOptions.Clo.Trace) {

+        return;

+      }

       Console.WriteLine(s);

     }

 

-    static void WriteTrailer(int verified, int errors, int inconclusives, int timeOuts, int outOfMemories)

-      requires 0 <= errors && 0 <= inconclusives && 0 <= timeOuts && 0 <= outOfMemories;

-    {

+    static void WriteTrailer(int verified, int errors, int inconclusives, int timeOuts, int outOfMemories) {

+      Contract.Requires(0 <= errors && 0 <= inconclusives && 0 <= timeOuts && 0 <= outOfMemories);

       Console.WriteLine();

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

-      Console.Write("{0} finished with {1} credible, {2} doomed{3}", CommandLineOptions.Clo.ToolName, verified, errors, errors == 1 ? "" : "s");

+        Console.Write("{0} finished with {1} credible, {2} doomed{3}", CommandLineOptions.Clo.ToolName, verified, errors, errors == 1 ? "" : "s");

       } else {

-      Console.Write("{0} finished with {1} verified, {2} error{3}", CommandLineOptions.Clo.ToolName, verified, errors, errors == 1 ? "" : "s");      

+        Console.Write("{0} finished with {1} verified, {2} error{3}", CommandLineOptions.Clo.ToolName, verified, errors, errors == 1 ? "" : "s");

       }

       if (inconclusives != 0) {

         Console.Write(", {0} inconclusive{1}", inconclusives, inconclusives == 1 ? "" : "s");

@@ -295,10 +316,11 @@ namespace Microsoft.Boogie
       Console.Out.Flush();

     }

 

-    

 

-    static void ReportBplError(Absy! node, string! message, bool error, bool showBplLocation)

-    {

+

+    static void ReportBplError(Absy node, string message, bool error, bool showBplLocation) {

+      Contract.Requires(message != null);

+      Contract.Requires(node != null);

       IToken tok = node.tok;

       string s;

       if (tok != null && showBplLocation) {

@@ -331,8 +353,8 @@ namespace Microsoft.Boogie
     /// Parse the given files into one Boogie program.  If an I/O or parse error occurs, an error will be printed

     /// and null will be returned.  On success, a non-null program is returned.

     /// </summary>

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

-    {

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

+      Contract.Requires(NonNullElements(fileNames));

       //BoogiePL.Errors.count = 0;

       Program program = null;

       bool okay = true;

@@ -374,10 +396,17 @@ namespace Microsoft.Boogie
         return program;

       }

     }

-    

 

-    enum PipelineOutcome { Done, ResolutionError, TypeCheckingError, ResolvedAndTypeChecked, FatalError, VerificationCompleted }

-    

+

+    enum PipelineOutcome {

+      Done,

+      ResolutionError,

+      TypeCheckingError,

+      ResolvedAndTypeChecked,

+      FatalError,

+      VerificationCompleted

+    }

+

     /// <summary>

     /// Resolves and type checks the given Boogie program.  Any errors are reported to the

     /// console.  Returns:

@@ -386,11 +415,14 @@ namespace Microsoft.Boogie
     ///  - TypeCheckingError if a type checking error occurred

     ///  - ResolvedAndTypeChecked if both resolution and type checking succeeded

     /// </summary>

-    static PipelineOutcome ResolveAndTypecheck (Program! program, string! bplFileName)

-    {

+    static PipelineOutcome ResolveAndTypecheck(Program program, string bplFileName) {

+      Contract.Requires(program != null);

+      Contract.Requires(bplFileName != null);

       // ---------- Resolve ------------------------------------------------------------

 

-      if (CommandLineOptions.Clo.NoResolve) { return PipelineOutcome.Done; }

+      if (CommandLineOptions.Clo.NoResolve) {

+        return PipelineOutcome.Done;

+      }

 

       int errorCount = program.Resolve();

       if (errorCount != 0) {

@@ -399,40 +431,45 @@ namespace Microsoft.Boogie
       }

 

       // ---------- Type check ------------------------------------------------------------

-      

-      if (CommandLineOptions.Clo.NoTypecheck) { return PipelineOutcome.Done; }

-      

+

+      if (CommandLineOptions.Clo.NoTypecheck) {

+        return PipelineOutcome.Done;

+      }

+

       errorCount = program.Typecheck();

       if (errorCount != 0) {

         Console.WriteLine("{0} type checking errors detected in {1}", errorCount, bplFileName);

         return PipelineOutcome.TypeCheckingError;

       }

-    

-      if (CommandLineOptions.Clo.PrintFile != null && CommandLineOptions.Clo.PrintDesugarings) 

-      {

+

+      if (CommandLineOptions.Clo.PrintFile != null && CommandLineOptions.Clo.PrintDesugarings) {

         // if PrintDesugaring option is engaged, print the file here, after resolution and type checking

         PrintBplFile(CommandLineOptions.Clo.PrintFile, program, true);

       }

 

       return PipelineOutcome.ResolvedAndTypeChecked;

     }

-    

-    static PipelineOutcome EliminateDeadVariablesAndInline(Program! program) {

+

+    static PipelineOutcome EliminateDeadVariablesAndInline(Program program) {

+      Contract.Requires(program != null);

       // Eliminate dead variables

       Microsoft.Boogie.UnusedVarEliminator.Eliminate(program);

-      

+

       // Collect mod sets

       if (CommandLineOptions.Clo.DoModSetAnalysis) {

         Microsoft.Boogie.ModSetCollector.DoModSetAnalysis(program);

       }

-      

+

       // Coalesce blocks

       if (CommandLineOptions.Clo.CoalesceBlocks) {

         Microsoft.Boogie.BlockCoalescer.CoalesceBlocks(program);

       }

-      

+

       // Inline

-      List<Declaration!> TopLevelDeclarations = program.TopLevelDeclarations;

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

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

+      

+      

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

         bool inline = false;

         foreach (Declaration d in TopLevelDeclarations) {

@@ -441,7 +478,7 @@ namespace Microsoft.Boogie
           }

         }

         if (inline && CommandLineOptions.Clo.LazyInlining == 0 &&

-            CommandLineOptions.Clo.StratifiedInlining == 0) {

+          CommandLineOptions.Clo.StratifiedInlining == 0) {

           foreach (Declaration d in TopLevelDeclarations) {

             Implementation impl = d as Implementation;

             if (impl != null) {

@@ -466,7 +503,7 @@ namespace Microsoft.Boogie
       }

       return PipelineOutcome.Done;

     }

-    

+

     /// <summary>

     /// Given a resolved and type checked Boogie program, infers invariants for the program

     /// and then attempts to verify it.  Returns:

@@ -475,21 +512,22 @@ namespace Microsoft.Boogie
     ///  - VerificationCompleted if inference and verification completed, in which the out

     ///    parameters contain meaningful values

     /// </summary>

-    static PipelineOutcome InferAndVerify (Program! program,

+    static PipelineOutcome InferAndVerify(Program program,

                                            ErrorReporter errorReporter,

-                                           out int errorCount, out int verified, out int inconclusives, out int timeOuts, out int outOfMemories)

-      ensures 0 <= inconclusives && 0 <= timeOuts;

-    {

+                                           out int errorCount, out int verified, out int inconclusives, out int timeOuts, out int outOfMemories) {

+      Contract.Requires(program != null);

+      Contract.Ensures(0 <= Contract.ValueAtReturn(out inconclusives) && 0 <= Contract.ValueAtReturn(out timeOuts));

+

       errorCount = verified = inconclusives = timeOuts = outOfMemories = 0;

-  

+

       // ---------- Infer invariants --------------------------------------------------------

-      

+

       // Abstract interpretation -> Always use (at least) intervals, if not specified otherwise (e.g. with the "/noinfer" switch)

       Microsoft.Boogie.AbstractInterpretation.AbstractInterpretation.RunAbstractInterpretation(program);

-       

-	    if (CommandLineOptions.Clo.LoopUnrollCount != -1) {

-	      program.UnrollLoops(CommandLineOptions.Clo.LoopUnrollCount);

-	    }

+

+      if (CommandLineOptions.Clo.LoopUnrollCount != -1) {

+        program.UnrollLoops(CommandLineOptions.Clo.LoopUnrollCount);

+      }

 

       if (CommandLineOptions.Clo.PrintInstrumented) {

         program.Emit(new TokenTextWriter(Console.Out));

@@ -502,10 +540,12 @@ namespace Microsoft.Boogie
 

       // ---------- Verify ------------------------------------------------------------

 

-      if (!CommandLineOptions.Clo.Verify) { return PipelineOutcome.Done; }

-            

+      if (!CommandLineOptions.Clo.Verify) {

+        return PipelineOutcome.Done;

+      }

+

       #region Verify each implementation

-      

+

 #if ROB_DEBUG

       string now = DateTime.Now.ToString().Replace(' ','-').Replace('/','-').Replace(':','-');

       System.IO.StreamWriter w = new System.IO.StreamWriter(@"\temp\batch_"+now+".bpl");

@@ -514,27 +554,23 @@ namespace Microsoft.Boogie
 #endif

 

       ConditionGeneration vcgen = null;

-      try

-      {

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

-        {

+      try {

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

           vcgen = new DCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend);

-        } else

-        {

+        } else {

           vcgen = new VCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend);

         }

-      }

-      catch (ProverException e)

-      {

+      } catch (ProverException e) {

         ErrorWriteLine("Fatal Error: ProverException: {0}", e);

         return PipelineOutcome.FatalError;

       }

-      

-      foreach ( Declaration! decl in program.TopLevelDeclarations )

-      {

+

+      foreach (Declaration decl in program.TopLevelDeclarations) {

+        Contract.Assert(decl != null);

         Implementation impl = decl as Implementation;

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

-          List<Counterexample!>? errors;

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

+          //TODO: Resolve arraylist nonnulls

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

 

           DateTime start = new DateTime();  // to please compiler's definite assignment rules

           if (CommandLineOptions.Clo.Trace || CommandLineOptions.Clo.XmlSink != null) {

@@ -549,24 +585,20 @@ namespace Microsoft.Boogie
           }

 

           VCGen.Outcome outcome;

-          try

-          {

+          try {

             outcome = vcgen.VerifyImplementation(impl, program, out errors);

-          }

-          catch (VCGenException e)

-          {

+          } catch (VCGenException e) {

             ReportBplError(impl, String.Format("Error BP5010: {0}  Encountered in implementation {1}.", e.Message, impl.Name), true, true);

             errors = null;

             outcome = VCGen.Outcome.Inconclusive;

-          }

-          catch (UnexpectedProverOutputException upo)

-          {

+          } catch (UnexpectedProverOutputException upo) {

             AdvisoryWriteLine("Advisory: {0} SKIPPED because of internal error: unexpected prover output: {1}", impl.Name, upo.Message);

             errors = null;

             outcome = VCGen.Outcome.Inconclusive;

           }

 

           string timeIndication = "";

+

           DateTime end = DateTime.Now;

           TimeSpan elapsed = end - start;

           if (CommandLineOptions.Clo.Trace || CommandLineOptions.Clo.XmlSink != null) {

@@ -574,11 +606,12 @@ namespace Microsoft.Boogie
               timeIndication = string.Format("  [{0} s]  ", elapsed.TotalSeconds);

             }

           }

-          

+

 

           switch (outcome) {

             default:

-              assert false;  // unexpected outcome

+              Contract.Assert(false);  // unexpected outcome

+              throw new UnreachableException();

             case VCGen.Outcome.Correct:

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

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

@@ -603,93 +636,85 @@ namespace Microsoft.Boogie
             case VCGen.Outcome.Errors:

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

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

-                errorCount++;                

+                errorCount++;

               } //else {

-                assert errors != null;  // guaranteed by postcondition of VerifyImplementation

-                if (errorReporter != null)

-                {

-  //                assert translatedProgram != null;

-  //                ErrorReporting h = new ErrorReporting();

-  //                h.errorReportingWithTrace(translatedProgram, errors, impl);

-                  

-                  errorReporter.ReportErrors();

-                }

-                else

-                {

-                  // BP1xxx: Parsing errors

-                  // BP2xxx: Name resolution errors

-                  // BP3xxx: Typechecking errors

-                  // BP4xxx: Abstract interpretation errors (Is there such a thing?)

-                  // BP5xxx: Verification errors

-                  

-                  errors.Sort(new CounterexampleComparer());

-                  foreach (Counterexample error in errors)

-                  {

-                    if (error is CallCounterexample)

+              Contract.Assert(errors != null);  // guaranteed by postcondition of VerifyImplementation

+              if (errorReporter != null) {

+                //                assert translatedProgram != null;

+                //                ErrorReporting h = new ErrorReporting();

+                //                h.errorReportingWithTrace(translatedProgram, errors, impl);

+

+                errorReporter.ReportErrors();

+              } else {

+                // BP1xxx: Parsing errors

+                // BP2xxx: Name resolution errors

+                // BP3xxx: Typechecking errors

+                // BP4xxx: Abstract interpretation errors (Is there such a thing?)

+                // BP5xxx: Verification errors

+

+                errors.Sort(new CounterexampleComparer());

+                foreach (Counterexample error in errors) {

+                  if (error is CallCounterexample) {

+                    CallCounterexample err = (CallCounterexample)error;

+                    if (!CommandLineOptions.Clo.ForceBplErrors && err.FailingRequires.ErrorMessage != null) {

+                      ReportBplError(err.FailingRequires, err.FailingRequires.ErrorMessage, true, false);

+                    } else {

+                      ReportBplError(err.FailingCall, "Error BP5002: A precondition for this call might not hold.", true, true);

+                      ReportBplError(err.FailingRequires, "Related location: This is the precondition that might not hold.", false, true);

+                    }

+                    if (CommandLineOptions.Clo.XmlSink != null) {

+                      CommandLineOptions.Clo.XmlSink.WriteError("precondition violation", err.FailingCall.tok, err.FailingRequires.tok, error.Trace);

+                    }

+                  } else if (error is ReturnCounterexample) {

+                    ReturnCounterexample err = (ReturnCounterexample)error;

+                    if (!CommandLineOptions.Clo.ForceBplErrors && err.FailingEnsures.ErrorMessage != null) {

+                      ReportBplError(err.FailingEnsures, err.FailingEnsures.ErrorMessage, true, false);

+                    } else {

+                      ReportBplError(err.FailingReturn, "Error BP5003: A postcondition might not hold at this return statement.", true, true);

+                      ReportBplError(err.FailingEnsures, "Related location: This is the postcondition that might not hold.", false, true);

+                    }

+                    if (CommandLineOptions.Clo.XmlSink != null) {

+                      CommandLineOptions.Clo.XmlSink.WriteError("postcondition violation", err.FailingReturn.tok, err.FailingEnsures.tok, error.Trace);

+                    }

+                  } else // error is AssertCounterexample

                     {

-                      CallCounterexample err = (CallCounterexample) error;

-                      if (!CommandLineOptions.Clo.ForceBplErrors && err.FailingRequires.ErrorMessage != null) {

-                        ReportBplError(err.FailingRequires, err.FailingRequires.ErrorMessage, true, false);

-                      } else {

-                        ReportBplError(err.FailingCall, "Error BP5002: A precondition for this call might not hold.", true, true);

-                        ReportBplError(err.FailingRequires, "Related location: This is the precondition that might not hold.", false, true);

+                    AssertCounterexample err = (AssertCounterexample)error;

+                    if (err.FailingAssert is LoopInitAssertCmd) {

+                      ReportBplError(err.FailingAssert, "Error BP5004: This loop invariant might not hold on entry.", true, true);

+                      if (CommandLineOptions.Clo.XmlSink != null) {

+                        CommandLineOptions.Clo.XmlSink.WriteError("loop invariant entry violation", err.FailingAssert.tok, null, error.Trace);

                       }

+                    } else if (err.FailingAssert is LoopInvMaintainedAssertCmd) {

+                      // this assertion is a loop invariant which is not maintained

+                      ReportBplError(err.FailingAssert, "Error BP5005: This loop invariant might not be maintained by the loop.", true, true);

                       if (CommandLineOptions.Clo.XmlSink != null) {

-                        CommandLineOptions.Clo.XmlSink.WriteError("precondition violation", err.FailingCall.tok, err.FailingRequires.tok, error.Trace);

+                        CommandLineOptions.Clo.XmlSink.WriteError("loop invariant maintenance violation", err.FailingAssert.tok, null, error.Trace);

                       }

-                    }

-                    else if (error is ReturnCounterexample)

-                    {

-                      ReturnCounterexample err = (ReturnCounterexample) error;

-                      if (!CommandLineOptions.Clo.ForceBplErrors && err.FailingEnsures.ErrorMessage != null) { 

-                        ReportBplError(err.FailingEnsures, err.FailingEnsures.ErrorMessage, true, false);

+                    } else {

+                      if (!CommandLineOptions.Clo.ForceBplErrors && err.FailingAssert.ErrorMessage != null) {

+                        ReportBplError(err.FailingAssert, err.FailingAssert.ErrorMessage, true, false);

+                      } else if (err.FailingAssert.ErrorData is string) {

+                        ReportBplError(err.FailingAssert, (string)err.FailingAssert.ErrorData, true, true);

                       } else {

-                        ReportBplError(err.FailingReturn, "Error BP5003: A postcondition might not hold at this return statement.", true, true);

-                        ReportBplError(err.FailingEnsures, "Related location: This is the postcondition that might not hold.", false, true);

+                        ReportBplError(err.FailingAssert, "Error BP5001: This assertion might not hold.", true, true);

                       }

                       if (CommandLineOptions.Clo.XmlSink != null) {

-                        CommandLineOptions.Clo.XmlSink.WriteError("postcondition violation", err.FailingReturn.tok, err.FailingEnsures.tok, error.Trace);

+                        CommandLineOptions.Clo.XmlSink.WriteError("assertion violation", err.FailingAssert.tok, null, error.Trace);

                       }

                     }

-                    else // error is AssertCounterexample

-                    {

-                      AssertCounterexample err = (AssertCounterexample) error;

-                      if (err.FailingAssert is LoopInitAssertCmd) {

-                        ReportBplError(err.FailingAssert, "Error BP5004: This loop invariant might not hold on entry.", true, true);

-                        if (CommandLineOptions.Clo.XmlSink != null) {

-                          CommandLineOptions.Clo.XmlSink.WriteError("loop invariant entry violation", err.FailingAssert.tok, null, error.Trace);

-                        }

-                      }

-                      else if (err.FailingAssert is LoopInvMaintainedAssertCmd) {

-                        // this assertion is a loop invariant which is not maintained

-                        ReportBplError(err.FailingAssert, "Error BP5005: This loop invariant might not be maintained by the loop.", true, true);

-                        if (CommandLineOptions.Clo.XmlSink != null) {

-                          CommandLineOptions.Clo.XmlSink.WriteError("loop invariant maintenance violation", err.FailingAssert.tok, null, error.Trace);

-                        }

-                      } else {

-                        if (!CommandLineOptions.Clo.ForceBplErrors && err.FailingAssert.ErrorMessage != null) {

-                          ReportBplError(err.FailingAssert, err.FailingAssert.ErrorMessage, true, false);

-                        } else if (err.FailingAssert.ErrorData is string) {

-                          ReportBplError(err.FailingAssert, (string)err.FailingAssert.ErrorData, true, true);

-                        } else {

-                          ReportBplError(err.FailingAssert, "Error BP5001: This assertion might not hold.", true, true);

-                        }

-                        if (CommandLineOptions.Clo.XmlSink != null) {

-                          CommandLineOptions.Clo.XmlSink.WriteError("assertion violation", err.FailingAssert.tok, null, error.Trace);

-                        }

-                      }

-                    }

-                    if (CommandLineOptions.Clo.EnhancedErrorMessages == 1) { 

-                      foreach (string! info in error.relatedInformation) {

-                        Console.WriteLine("       " + info);

-                      } 

-                    }

-                    if (CommandLineOptions.Clo.ErrorTrace > 0) {

-                      Console.WriteLine("Execution trace:");

-                      error.Print(4);

-                    }

-                    errorCount++;

+                  }

+                  if (CommandLineOptions.Clo.EnhancedErrorMessages == 1) {

+                    foreach (string info in error.relatedInformation) {

+                      Contract.Assert(info != null);

+                      Console.WriteLine("       " + info);

                     }

+                  }

+                  if (CommandLineOptions.Clo.ErrorTrace > 0) {

+                    Console.WriteLine("Execution trace:");

+                    error.Print(4);

+                  }

+                  errorCount++;

+                }

                 //}

                 Inform(String.Format("{0}error{1}", timeIndication, errors.Count == 1 ? "" : "s"));

               }

@@ -704,12 +729,27 @@ namespace Microsoft.Boogie
         }

       }

       vcgen.Close();

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

+      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 bf95f536..f323f58f 100644
--- a/Source/BoogieDriver/BoogieDriver.csproj
+++ b/Source/BoogieDriver/BoogieDriver.csproj
@@ -1,148 +1,143 @@
-<?xml version="1.0" encoding="utf-8"?>

-<VisualStudioProject>

-  <XEN ProjectType="Local"

-     SchemaVersion="1.0"

-     Name="BoogieDriver"

-     ProjectGuid="d2b98e4a-2eab-4065-abfa-709ac5ca7d4c"

-    >

-    <Build>

-      <Settings ApplicationIcon=""

-         AssemblyName="Boogie"

-         OutputType="Exe"

-         RootNamespace="Boogie"

-         StartupObject=""

-         StandardLibraryLocation=""

-         TargetPlatform="v2"

-         TargetPlatformLocation=""

-        >

-        <Config Name="Debug"

-           AllowUnsafeBlocks="False"

-           BaseAddress="285212672"

-           CheckForOverflowUnderflow="False"

-           ConfigurationOverrideFile=""

-           DefineConstants="DEBUG;TRACE"

-           DocumentationFile=""

-           DebugSymbols="True"

-           FileAlignment="4096"

-           IncrementalBuild="True"

-           Optimize="False"

-           OutputPath="..\..\Binaries"

-           RegisterForComInterop="False"

-           RemoveIntegerChecks="false"

-           TreatWarningsAsErrors="False"

-           WarningLevel="4"

-           CheckContractAdmissibility="True"

-           CheckPurity="False"

-           />

-        <Config Name="Release"

-           AllowUnsafeBlocks="false"

-           BaseAddress="285212672"

-           CheckForOverflowUnderflow="false"

-           ConfigurationOverrideFile=""

-           DefineConstants="TRACE"

-           DocumentationFile=""

-           DebugSymbols="false"

-           FileAlignment="4096"

-           IncrementalBuild="false"

-           Optimize="true"

-           OutputPath="bin\release"

-           RegisterForComInterop="false"

-           RemoveIntegerChecks="false"

-           TreatWarningsAsErrors="false"

-           WarningLevel="4"

-           CheckContractAdmissibility="True"

-           CheckPurity="False"

-           />

-      </Settings>

-      <References>

-        <Reference Name="System"

-             AssemblyName="System"

-             Private="false"

-             />

-        <Reference Name="System.Data"

-             AssemblyName="System.Data"

-             Private="false"

-             />

-        <Reference Name="System.Xml"

-             AssemblyName="System.Xml"

-             Private="false"

-             />

-        <Reference Name="System.Compiler"

-             AssemblyName="System.Compiler"

-             Private="false"

-             HintPath="../../Binaries/System.Compiler.dll"

-             />

-        <Reference Name="Microsoft.SpecSharp"

-             AssemblyName="Microsoft.SpecSharp"

-             Private="false"

-             HintPath="../../Binaries/Microsoft.SpecSharp.dll"

-             />

-        <Reference Name="System.Compiler.Framework"

-             AssemblyName="System.Compiler.Framework"

-             Private="false"

-             HintPath="../../Binaries/System.Compiler.Framework.dll"

-             />

-        <Reference Name="AbsInt"

-             Project="{11D06232-2039-4BCA-853B-C596E2A4EDB0}"

-             Private="true"

-             />

-        <Reference Name="AIFramework"

-             Project="{24B55172-AD8B-47D1-8952-5A95CFDB9B31}"

-             Private="true"

-             />

-        <Reference Name="Basetypes"

-             Project="{0C692837-77EC-415F-BF04-395E3ED06E9A}"

-             Private="true"

-             />

-        <Reference Name="Core"

-             Project="{47BC34F1-A173-40BE-84C2-9332B4418387}"

-             Private="true"

-             />

-        <Reference Name="Graph"

-             Project="{4C28FB90-630E-4B55-A937-11A011B79765}"

-             Private="true"

-             />

-        <Reference Name="Simplify"

-             Project="{F75666DE-FB56-457C-8782-09BE243450FC}"

-             Private="true"

-             />

-        <Reference Name="SMTLib"

-             Project="{13C3A68C-462A-4CDA-A480-738046E37C5A}"

-             Private="true"

-             />

-        <Reference Name="Z3"

-             Project="{F75666DE-CD56-457C-8782-09BE243450FC}"

-             Private="true"

-             />

-        <Reference Name="VCExpr"

-             Project="{CF42B700-10AA-4DA9-8992-48A800251C11}"

-             Private="true"

-             />

-        <Reference Name="VCGeneration"

-             Project="{F65666DE-FB56-457C-8782-09BE243450FC}"

-             Private="true"

-             />

-        <Reference Name="Isabelle"

-             Project="{C3C3BC4F-6AEB-41AB-A649-4A085DC6FB36}"

-             Private="true"

-             />

-      </References>

-    </Build>

-    <Files>

-      <Include>

-        <File RelPath="BoogieDriver.ssc"

-                 SubType="Code"

-                 BuildAction="Compile"

-                 />

-        <File BuildAction="Compile"

-                 SubType="Code"

-                 RelPath="..\version.ssc"

-                 />

-        <File BuildAction="Compile"

-                 SubType="Code"

-                 RelPath="AssemblyInfo.ssc"

-                 />

-      </Include>

-    </Files>

-  </XEN>

-</VisualStudioProject>

+<?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>{DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}</ProjectGuid>

+    <OutputType>Exe</OutputType>

+    <AppDesignerFolder>Properties</AppDesignerFolder>

+    <RootNamespace>BoogieDriver</RootNamespace>

+    <AssemblyName>Boogie</AssemblyName>

+    <TargetFrameworkVersion>v3.5</TargetFrameworkVersion>

+    <FileAlignment>512</FileAlignment>

+    <CodeContractsAssemblyMode>0</CodeContractsAssemblyMode>

+  </PropertyGroup>

+  <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Debug|AnyCPU' ">

+    <DebugSymbols>true</DebugSymbols>

+    <DebugType>full</DebugType>

+    <Optimize>false</Optimize>

+    <OutputPath>..\..\Binaries\</OutputPath>

+    <DefineConstants>DEBUG;TRACE</DefineConstants>

+    <ErrorReport>prompt</ErrorReport>

+    <WarningLevel>4</WarningLevel>

+    <CodeContractsEnableRuntimeChecking>True</CodeContractsEnableRuntimeChecking>

+    <CodeContractsRuntimeOnlyPublicSurface>False</CodeContractsRuntimeOnlyPublicSurface>

+    <CodeContractsRuntimeThrowOnFailure>True</CodeContractsRuntimeThrowOnFailure>

+    <CodeContractsRuntimeCallSiteRequires>False</CodeContractsRuntimeCallSiteRequires>

+    <CodeContractsRunCodeAnalysis>False</CodeContractsRunCodeAnalysis>

+    <CodeContractsNonNullObligations>False</CodeContractsNonNullObligations>

+    <CodeContractsBoundsObligations>False</CodeContractsBoundsObligations>

+    <CodeContractsArithmeticObligations>False</CodeContractsArithmeticObligations>

+    <CodeContractsPointerObligations>False</CodeContractsPointerObligations>

+    <CodeContractsContainerAnalysis>False</CodeContractsContainerAnalysis>

+    <CodeContractsRedundantAssumptions>False</CodeContractsRedundantAssumptions>

+    <CodeContractsRunInBackground>True</CodeContractsRunInBackground>

+    <CodeContractsShowSquigglies>False</CodeContractsShowSquigglies>

+    <CodeContractsUseBaseLine>False</CodeContractsUseBaseLine>

+    <CodeContractsEmitXMLDocs>False</CodeContractsEmitXMLDocs>

+    <CodeContractsCustomRewriterAssembly>

+    </CodeContractsCustomRewriterAssembly>

+    <CodeContractsCustomRewriterClass>

+    </CodeContractsCustomRewriterClass>

+    <CodeContractsLibPaths>

+    </CodeContractsLibPaths>

+    <CodeContractsExtraRewriteOptions>

+    </CodeContractsExtraRewriteOptions>

+    <CodeContractsExtraAnalysisOptions>

+    </CodeContractsExtraAnalysisOptions>

+    <CodeContractsBaseLineFile>

+    </CodeContractsBaseLineFile>

+    <CodeContractsRuntimeCheckingLevel>Full</CodeContractsRuntimeCheckingLevel>

+    <CodeContractsReferenceAssembly>%28none%29</CodeContractsReferenceAssembly>

+  </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="AbsInt, Version=2.0.0.0, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">

+      <SpecificVersion>False</SpecificVersion>

+      <HintPath>..\..\..\Binaries\AbsInt.dll</HintPath>

+    </Reference>

+    <Reference Include="AIFramework, Version=2.0.0.0, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">

+      <SpecificVersion>False</SpecificVersion>

+      <HintPath>..\..\..\Binaries\AIFramework.dll</HintPath>

+    </Reference>

+    <Reference Include="Basetypes, Version=2.0.0.0, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">

+      <SpecificVersion>False</SpecificVersion>

+      <HintPath>..\..\..\Binaries\Basetypes.dll</HintPath>

+    </Reference>

+    <Reference Include="Core, Version=2.0.0.0, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">

+      <SpecificVersion>False</SpecificVersion>

+      <HintPath>..\..\..\Binaries\Core.dll</HintPath>

+    </Reference>

+    <Reference Include="Graph, Version=2.0.0.0, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">

+      <SpecificVersion>False</SpecificVersion>

+      <HintPath>..\..\..\Binaries\Graph.dll</HintPath>

+    </Reference>

+    <Reference Include="Microsoft.Contracts, Version=1.0.0.0, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL" />

+    <Reference Include="Microsoft.SpecSharp, Version=1.0.21125.0, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">

+      <SpecificVersion>False</SpecificVersion>

+      <HintPath>..\..\..\Binaries\Microsoft.SpecSharp.dll</HintPath>

+    </Reference>

+    <Reference Include="Provers.Isabelle, Version=2.0.0.0, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">

+      <SpecificVersion>False</SpecificVersion>

+      <HintPath>..\..\..\Binaries\Provers.Isabelle.dll</HintPath>

+    </Reference>

+    <Reference Include="Provers.Simplify, Version=2.0.0.0, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">

+      <SpecificVersion>False</SpecificVersion>

+      <HintPath>..\..\..\Binaries\Provers.Simplify.dll</HintPath>

+    </Reference>

+    <Reference Include="Provers.SMTLib, Version=0.0.0.0, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">

+      <SpecificVersion>False</SpecificVersion>

+      <HintPath>..\..\..\Binaries\Provers.SMTLib.dll</HintPath>

+    </Reference>

+    <Reference Include="Provers.Z3, Version=2.0.0.0, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">

+      <SpecificVersion>False</SpecificVersion>

+      <HintPath>..\..\..\Binaries\Provers.Z3.dll</HintPath>

+    </Reference>

+    <Reference Include="System" />

+    <Reference Include="System.Compiler, Version=1.0.21125.0, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">

+      <SpecificVersion>False</SpecificVersion>

+      <HintPath>..\..\..\Binaries\System.Compiler.dll</HintPath>

+    </Reference>

+    <Reference Include="System.Compiler.Framework, Version=1.0.21125.0, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">

+      <SpecificVersion>False</SpecificVersion>

+      <HintPath>..\..\..\Binaries\System.Compiler.Framework.dll</HintPath>

+    </Reference>

+    <Reference Include="System.Compiler.Runtime, Version=1.0.21125.0, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">

+      <SpecificVersion>False</SpecificVersion>

+      <HintPath>..\..\..\Binaries\System.Compiler.Runtime.dll</HintPath>

+    </Reference>

+    <Reference Include="System.Data" />

+    <Reference Include="System.Xml" />

+    <Reference Include="VCExpr, Version=2.0.0.0, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">

+      <SpecificVersion>False</SpecificVersion>

+      <HintPath>..\..\..\Binaries\VCExpr.dll</HintPath>

+    </Reference>

+    <Reference Include="VCGeneration, Version=2.0.0.0, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">

+      <SpecificVersion>False</SpecificVersion>

+      <HintPath>..\..\..\Binaries\VCGeneration.dll</HintPath>

+    </Reference>

+  </ItemGroup>

+  <ItemGroup>

+    <Compile Include="Properties\AssemblyInfo.cs" />

+  </ItemGroup>

+  <ItemGroup>

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

+  </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