From 7d9a1e78eb07f592065a69db862d92014d5c1894 Mon Sep 17 00:00:00 2001 From: rustanleino Date: Tue, 15 Sep 2009 22:10:28 +0000 Subject: * Boogie and Dafny: added /cev: option * SscBoogie: changed default setting for /modifiesOnLoop (we really should move this SscBoogie-specific code to the Spec# codeplex) --- Source/BoogieDriver/BoogieDriver.ssc | 14 +++++++++++++ Source/Core/CommandLineOptions.ssc | 40 +++++++++++++++++++++++++----------- Source/DafnyDriver/DafnyDriver.ssc | 14 +++++++++++++ Source/VCGeneration/VC.ssc | 4 ++-- 4 files changed, 58 insertions(+), 14 deletions(-) diff --git a/Source/BoogieDriver/BoogieDriver.ssc b/Source/BoogieDriver/BoogieDriver.ssc index 0254c3ef..6eb16fa4 100644 --- a/Source/BoogieDriver/BoogieDriver.ssc +++ b/Source/BoogieDriver/BoogieDriver.ssc @@ -299,8 +299,22 @@ namespace Microsoft.Boogie } 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(); + } } } diff --git a/Source/Core/CommandLineOptions.ssc b/Source/Core/CommandLineOptions.ssc index d215de0d..244dc640 100644 --- a/Source/Core/CommandLineOptions.ssc +++ b/Source/Core/CommandLineOptions.ssc @@ -143,6 +143,7 @@ namespace Microsoft.Boogie public int PrintErrorModel = 0; public string PrintErrorModelFile = null; invariant (0 <= PrintErrorModel && PrintErrorModel <= 2) || PrintErrorModel == 4; + public bool CEVPrint = false; public int EnhancedErrorMessages = 0; invariant 0 <= EnhancedErrorMessages && EnhancedErrorMessages < 2; public bool ForceBplErrors = false; // if true, boogie error is shown even if "msg" attribute is present @@ -654,7 +655,7 @@ namespace Microsoft.Boogie case "/localModifiesChecks": { int localChecks = 0; - ps.GetNumericArgument(ref localChecks, 7); + ps.GetNumericArgument(ref localChecks, 2); LocalModifiesChecks = (localChecks != 0); } break; @@ -730,6 +731,15 @@ namespace Microsoft.Boogie break; + case "-cev": + case "/cev": + if (ps.ConfirmArgumentCount(1)) + { + PrintErrorModelFile = args[ps.i]; + } + CEVPrint = true; + break; + case "-printModelToFile": case "/printModelToFile": if (ps.ConfirmArgumentCount(1)) @@ -1191,14 +1201,18 @@ namespace Microsoft.Boogie } if (LoopFrameConditions == -1) { - // /modifiesOnLoop not specified. Set its default depending on /level - if (CheckingLevel == 2) { - LoopFrameConditions = 2; - } else { + // /modifiesOnLoop not specified. Set its default depending on /localModifiesChecks + if (LocalModifiesChecks) { LoopFrameConditions = 1; + } else { + LoopFrameConditions = 2; } } + if (CEVPrint && PrintErrorModel == 0) { + PrintErrorModel = 1; + } + switch (InductiveMinMax) { case 1: case 2: case 4: case 5: ReflectAdd = true; // these InductiveMinMax modes imply ReflectAdd @@ -1649,7 +1663,7 @@ namespace Microsoft.Boogie ---- Spec# options --------------------------------------------------------- If any of the following switches is included, only those methods specified - by some switch are translated into BoogiePL. Furthermore, a method is + by some switch are translated into Boogie. Furthermore, a method is not translated if a [Verify(false)] attribute applies to it or if the flag /trExclude applies (see below). /translate: : include method if its full name contains substring @@ -1685,12 +1699,13 @@ namespace Microsoft.Boogie occurring at the top-level of modifies clause as p.f, p.*, p.**, p[i], p[*], or p.0 6 - (5) but for every parameter p - /modifiesOnLoop: : 0 - never, 1 - assume only (usual default), - 2 - assume and check (default with /level:2) + /modifiesOnLoop: : 0 - never, 1 - assume only (default), + 2 - assume and check (default with + /localModifiesChecks:0) /localModifiesChecks: 0 - check modifies-clause as post-condition of a procedure 1 - check violations of modifies-clause at each - assignment and procedure call (default) + assignment and method call (default) /loopUnroll: : unroll loops, following up to n back edges (and then some) /noVerifyByDefault : change the default to [Verify(false)] /orderStrength: : 0 (default) - only few properties of subtyping @@ -1716,10 +1731,11 @@ namespace Microsoft.Boogie e = experimental t = trivial (implied by /methodology:vs) /printModel: : 0 (default) - do not print Z3's error model - 1 - print Z3's error model + 1 - print Z3's error model (default with /cev) 2 - print Z3's error model plus reverse mappings 4 - print Z3's error model in a more human readable way /printModelToFile: : print model to instead of console + /cev: Print Z3's error model to and include error message /enhancedErrorMessages: : 0 (default) - no enhanced error messages 1 - Z3 error model enhanced error messages @@ -1740,7 +1756,7 @@ namespace Microsoft.Boogie /noResolve : parse only /noTypecheck : parse and resolve only - /print: : print BoogiePL program after parsing it + /print: : print Boogie program after parsing it (use - as to print to console) /printWithUniqueIds : print augmented information that uniquely identifies variables @@ -1774,7 +1790,7 @@ namespace Microsoft.Boogie /interprocInfer : perform interprocedural inference /contractInfer : perform procedure contract inference /logInfer : print debug output during inference - /printInstrumented : print BoogiePL program after it has been + /printInstrumented : print Boogie program after it has been instrumented with invariants /Houdini[:] : perform procedure Houdini c = continue when an error found diff --git a/Source/DafnyDriver/DafnyDriver.ssc b/Source/DafnyDriver/DafnyDriver.ssc index 06280e74..8817f761 100644 --- a/Source/DafnyDriver/DafnyDriver.ssc +++ b/Source/DafnyDriver/DafnyDriver.ssc @@ -308,8 +308,22 @@ namespace Microsoft.Boogie } 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(); + } } } diff --git a/Source/VCGeneration/VC.ssc b/Source/VCGeneration/VC.ssc index a79e63eb..a5590b2c 100644 --- a/Source/VCGeneration/VC.ssc +++ b/Source/VCGeneration/VC.ssc @@ -1635,9 +1635,9 @@ namespace VC protected Dictionary! incarnationOriginMap; protected VerifierCallback! callback; internal string? resourceExceededMessage; - static private System.IO.TextWriter? modelWriter; + static System.IO.TextWriter? modelWriter; - static protected TextWriter! ModelWriter { + public static TextWriter! ModelWriter { get { if (ErrorReporter.modelWriter == null) ErrorReporter.modelWriter = CommandLineOptions.Clo.PrintErrorModelFile == null ? Console.Out : new StreamWriter(CommandLineOptions.Clo.PrintErrorModelFile, false); -- cgit v1.2.3