diff options
| author |  tabarbe <unknown> | 2010-07-01 15:46:16 +0000 |
|---|---|---|
| committer | tabarbe <unknown> | 2010-07-01 15:46:16 +0000 |
| commit | 6b7471ded8b47da80273bef3c6a9e307c9640d90 (patch) | |
| tree | b09401c8945f18f6635240e782eb3a506761f672 | |
| parent | c5402514fbc8193b7f4a2f9ccec537e71bb1b0aa (diff) | |
As it turns out, the C# Intellisense compiler takes precedence over the Spec# Intellisense compiler during editing of a .cs file. So, in order to allow continued editing of Boogie, during my porting project I will not be renaming the .ssc files to .cs, but rather creating copies of, for example, the BoogieDriver project's files, naming them as .cs versions, and porting them the rest of the way into C#. I will build these projects and run the regression tests on them, and once (and only once) the reg tests are passed, I will commit the compiled C# output as the replacement for the Spec# component.
| -rw-r--r-- | Source/BoogieDriver/AssemblyInfo.ssc | 4 | ||||
| -rw-r--r-- | Source/BoogieDriver/BoogieDriver.ssc | 714 |
2 files changed, 718 insertions, 0 deletions
diff --git a/Source/BoogieDriver/AssemblyInfo.ssc b/Source/BoogieDriver/AssemblyInfo.ssc new file mode 100644 index 00000000..6ed99a25 --- /dev/null +++ b/Source/BoogieDriver/AssemblyInfo.ssc @@ -0,0 +1,4 @@ +using System.Reflection;
+using System.Runtime.CompilerServices;
+
+[assembly: AssemblyKeyFile("..\\InterimKey.snk")]
diff --git a/Source/BoogieDriver/BoogieDriver.ssc b/Source/BoogieDriver/BoogieDriver.ssc new file mode 100644 index 00000000..c1bf358e --- /dev/null +++ b/Source/BoogieDriver/BoogieDriver.ssc @@ -0,0 +1,714 @@ +//-----------------------------------------------------------------------------
+//
+// Copyright (C) Microsoft Corporation. All Rights Reserved.
+//
+//-----------------------------------------------------------------------------
+//---------------------------------------------------------------------------------------------
+// OnlyBoogie OnlyBoogie.ssc
+// - main program for taking a BPL program and verifying it
+//---------------------------------------------------------------------------------------------
+
+namespace Microsoft.Boogie
+{
+ using System;
+ using System.IO;
+ using System.Collections;
+ using System.Collections.Generic;
+ using PureCollections;
+ using Microsoft.Boogie;
+ using Microsoft.Boogie.AbstractInterpretation;
+ 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
+*/
+
+ public class OnlyBoogie
+ {
+ // ------------------------------------------------------------------------
+ // Main
+
+ public static void Main (string[]! args)
+ {
+ assert forall{int i in (0:args.Length); args[i] != null};
+ CommandLineOptions.Clo.RunningBoogieFromCommandLine = true;
+ if (CommandLineOptions.Clo.Parse(args) != 1)
+ {
+ goto END;
+ }
+ if (CommandLineOptions.Clo.Files.Count == 0)
+ {
+ ErrorWriteLine("*** Error: No input files were specified.");
+ goto END;
+ }
+ if (CommandLineOptions.Clo.XmlSink != null) {
+ string errMsg = CommandLineOptions.Clo.XmlSink.Open();
+ if (errMsg != null) {
+ ErrorWriteLine("*** Error: " + errMsg);
+ goto END;
+ }
+ }
+ if (!CommandLineOptions.Clo.DontShowLogo)
+ {
+ Console.WriteLine(CommandLineOptions.Clo.Version);
+ }
+ if (CommandLineOptions.Clo.ShowEnv == CommandLineOptions.ShowEnvironment.Always)
+ {
+ Console.WriteLine("---Command arguments");
+ foreach (string! arg in args)
+ {
+ Console.WriteLine(arg);
+ }
+ Console.WriteLine("--------------------");
+ }
+
+ SelectPlatform(CommandLineOptions.Clo);
+
+ Helpers.ExtraTraceInformation("Becoming sentient");
+
+ // Make sure the Spec# runtime is initialized.
+ // This happens when the static constructor for the Runtime type is executed.
+ // Otherwise, if a reference happens to get chased to it, it is loaded twice
+ // 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;
+ }
+
+ foreach (string! file in CommandLineOptions.Clo.Files)
+ {
+ 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;
+ }
+ }
+ 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();
+ }
+ }
+
+ public static void ErrorWriteLine(string! s) {
+ 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);
+ 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) {
+ string s = string.Format(format, args);
+ ErrorWriteLine(s);
+ }
+
+ public static void AdvisoryWriteLine(string! format, params object[] args) {
+ 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;
+ {
+ string message = node.GetMessage(System.Threading.Thread.CurrentThread.CurrentUICulture);
+ string kind;
+ if (message.Contains("(trace position)")) {
+ kind = "Related information";
+ } else {
+ 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);
+ } 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));
+ }
+ }
+ }
+
+ static void ProcessFiles (List<string!>! 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 (CommandLineOptions.Clo.PrintFile != null) {
+ PrintBplFile(CommandLineOptions.Clo.PrintFile, program, false);
+ }
+
+ 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) {
+ case PipelineOutcome.Done:
+ case PipelineOutcome.VerificationCompleted:
+ WriteTrailer(verified, errorCount, inconclusives, timeOuts, outOfMemories);
+ break;
+ default:
+ break;
+ }
+ }
+ }
+
+
+ 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);
+ }
+ 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;
+ }
+
+
+ /// <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; }
+ 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;
+ {
+ 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");
+ } else {
+ 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");
+ }
+ if (timeOuts != 0) {
+ Console.Write(", {0} time out{1}", timeOuts, timeOuts == 1 ? "" : "s");
+ }
+ if (outOfMemories != 0) {
+ Console.Write(", {0} out of memory", outOfMemories);
+ }
+ Console.WriteLine();
+ Console.Out.Flush();
+ }
+
+
+
+ static void ReportBplError(Absy! node, string! message, bool error, bool showBplLocation)
+ {
+ IToken tok = node.tok;
+ string s;
+ if (tok != null && showBplLocation) {
+ s = string.Format("{0}({1},{2}): {3}", tok.filename, tok.line, tok.col, message);
+ } else {
+ s = message;
+ }
+ if (error) {
+ ErrorWriteLine(s);
+ if (CommandLineOptions.Clo.CEVPrint) {
+ TextWriter mw = VC.VCGen.ErrorReporter.ModelWriter;
+ mw.WriteLine("BEGINNING_OF_ERROR");
+ mw.WriteLine(s);
+ mw.WriteLine("END_OF_ERROR");
+ mw.Flush();
+ }
+ } else {
+ Console.WriteLine(s);
+ if (CommandLineOptions.Clo.CEVPrint) {
+ TextWriter mw = VC.VCGen.ErrorReporter.ModelWriter;
+ mw.WriteLine("BEGINNING_OF_RELATED_INFO");
+ mw.WriteLine(s);
+ mw.WriteLine("END_OF_RELATED_INFO");
+ mw.Flush();
+ }
+ }
+ }
+
+ /// <summary>
+ /// 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)
+ {
+ //BoogiePL.Errors.count = 0;
+ Program program = null;
+ bool okay = true;
+ foreach (string bplFileName in fileNames) {
+ if (!suppressTraceOutput) {
+ if (CommandLineOptions.Clo.XmlSink != null) {
+ CommandLineOptions.Clo.XmlSink.WriteFileFragment(bplFileName);
+ }
+ if (CommandLineOptions.Clo.Trace) {
+ Console.WriteLine("Parsing " + bplFileName);
+ }
+ }
+
+ Program programSnippet;
+ int errorCount;
+ try {
+ errorCount = BoogiePL.Parser.Parse(bplFileName, out programSnippet);
+ if (programSnippet == null || errorCount != 0) {
+ Console.WriteLine("{0} parse errors detected in {1}", errorCount, bplFileName);
+ okay = false;
+ continue;
+ }
+ } catch (IOException e) {
+ ErrorWriteLine("Error opening file \"{0}\": {1}", bplFileName, e.Message);
+ okay = false;
+ continue;
+ }
+ if (program == null) {
+ program = programSnippet;
+ } else if (programSnippet != null) {
+ program.TopLevelDeclarations.AddRange(programSnippet.TopLevelDeclarations);
+ }
+ }
+ if (!okay) {
+ return null;
+ } else if (program == null) {
+ return new Program();
+ } else {
+ return program;
+ }
+ }
+
+
+ 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:
+ /// - Done if no errors occurred, and command line specified no resolution or no type checking.
+ /// - ResolutionError if a resolution error occurred
+ /// - TypeCheckingError if a type checking error occurred
+ /// - ResolvedAndTypeChecked if both resolution and type checking succeeded
+ /// </summary>
+ static PipelineOutcome ResolveAndTypecheck (Program! program, string! bplFileName)
+ {
+ // ---------- Resolve ------------------------------------------------------------
+
+ if (CommandLineOptions.Clo.NoResolve) { return PipelineOutcome.Done; }
+
+ int errorCount = program.Resolve();
+ if (errorCount != 0) {
+ Console.WriteLine("{0} name resolution errors detected in {1}", errorCount, bplFileName);
+ return PipelineOutcome.ResolutionError;
+ }
+
+ // ---------- Type check ------------------------------------------------------------
+
+ 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 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) {
+ // 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;
+ if (CommandLineOptions.Clo.ProcedureInlining != CommandLineOptions.Inlining.None) {
+ bool inline = false;
+ foreach (Declaration d in TopLevelDeclarations) {
+ if (d.FindExprAttribute("inline") != null) {
+ inline = true;
+ }
+ }
+ if (inline && CommandLineOptions.Clo.LazyInlining == 0) {
+ foreach (Declaration d in TopLevelDeclarations) {
+ Implementation impl = d as Implementation;
+ if (impl != null) {
+ impl.OriginalBlocks = impl.Blocks;
+ impl.OriginalLocVars = impl.LocVars;
+ }
+ }
+ foreach (Declaration d in TopLevelDeclarations) {
+ Implementation impl = d as Implementation;
+ if (impl != null && !impl.SkipVerification) {
+ Inliner.ProcessImplementation(program, impl);
+ }
+ }
+ foreach (Declaration d in TopLevelDeclarations) {
+ Implementation impl = d as Implementation;
+ if (impl != null) {
+ impl.OriginalBlocks = null;
+ impl.OriginalLocVars = null;
+ }
+ }
+ }
+ }
+ return PipelineOutcome.Done;
+ }
+
+ /// <summary>
+ /// Given a resolved and type checked Boogie program, infers invariants for the program
+ /// and then attempts to verify it. Returns:
+ /// - Done if command line specified no verification
+ /// - FatalError if a fatal error occurred, in which case an error has been printed to console
+ /// - VerificationCompleted if inference and verification completed, in which the out
+ /// parameters contain meaningful values
+ /// </summary>
+ 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;
+ {
+ 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.PrintInstrumented) {
+ program.Emit(new TokenTextWriter(Console.Out));
+ }
+
+ if (CommandLineOptions.Clo.ExpandLambdas) {
+ LambdaHelper.ExpandLambdas(program);
+ //PrintBplFile ("-", program, true);
+ }
+
+ // ---------- Verify ------------------------------------------------------------
+
+ 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");
+ program.Emit(new TokenTextWriter(w));
+ w.Close();
+#endif
+
+ ConditionGeneration vcgen = null;
+ try
+ {
+ if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Doomed)
+ {
+ vcgen = new DCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend);
+ } else
+ {
+ vcgen = new VCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend);
+ }
+ }
+ catch (ProverException e)
+ {
+ ErrorWriteLine("Fatal Error: ProverException: {0}", e);
+ return PipelineOutcome.FatalError;
+ }
+
+ foreach ( Declaration! decl in program.TopLevelDeclarations )
+ {
+ Implementation impl = decl as Implementation;
+ if (impl != null && CommandLineOptions.Clo.UserWantsToCheckRoutine((!)impl.Name) && !impl.SkipVerification) {
+ List<Counterexample!>? errors;
+
+ DateTime start = new DateTime(); // to please compiler's definite assignment rules
+ if (CommandLineOptions.Clo.Trace || CommandLineOptions.Clo.XmlSink != null) {
+ start = DateTime.Now;
+ if (CommandLineOptions.Clo.Trace) {
+ Console.WriteLine();
+ Console.WriteLine("Verifying {0} ...", impl.Name);
+ }
+ if (CommandLineOptions.Clo.XmlSink != null) {
+ CommandLineOptions.Clo.XmlSink.WriteStartMethod(impl.Name, start);
+ }
+ }
+
+ VCGen.Outcome outcome;
+ try
+ {
+ outcome = vcgen.VerifyImplementation(impl, program, out errors);
+ }
+ 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)
+ {
+ 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) {
+ if (CommandLineOptions.Clo.Trace) {
+ timeIndication = string.Format(" [{0} s] ", elapsed.TotalSeconds);
+ }
+ }
+
+
+ switch (outcome) {
+ default:
+ assert false; // unexpected outcome
+ case VCGen.Outcome.Correct:
+ if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Doomed) {
+ Inform(String.Format("{0}credible", timeIndication));
+ verified++;
+ } else {
+ Inform(String.Format("{0}verified", timeIndication));
+ verified++;
+ }
+ break;
+ case VCGen.Outcome.TimedOut:
+ timeOuts++;
+ Inform(String.Format("{0}timed out", timeIndication));
+ break;
+ case VCGen.Outcome.OutOfMemory:
+ outOfMemories++;
+ Inform(String.Format("{0}out of memory", timeIndication));
+ break;
+ case VCGen.Outcome.Inconclusive:
+ inconclusives++;
+ Inform(String.Format("{0}inconclusive", timeIndication));
+ break;
+ case VCGen.Outcome.Errors:
+ if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Doomed) {
+ Inform(String.Format("{0}doomed", timeIndication));
+ 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)
+ {
+ 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
+ {
+ 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++;
+ }
+ //}
+ Inform(String.Format("{0}error{1}", timeIndication, errors.Count == 1 ? "" : "s"));
+ }
+ break;
+ }
+ if (CommandLineOptions.Clo.XmlSink != null) {
+ CommandLineOptions.Clo.XmlSink.WriteEndMethod(outcome.ToString().ToLowerInvariant(), end, elapsed);
+ }
+ if (outcome == VCGen.Outcome.Errors || CommandLineOptions.Clo.Trace) {
+ Console.Out.Flush();
+ }
+ }
+ }
+ vcgen.Close();
+ ((!)CommandLineOptions.Clo.TheProverFactory).Close();
+
+ #endregion
+
+ return PipelineOutcome.VerificationCompleted;
+ }
+
+ }
+}
|