diff options
| author |  rustanleino <unknown> | 2009-09-15 22:10:28 +0000 |
|---|---|---|
| committer | rustanleino <unknown> | 2009-09-15 22:10:28 +0000 |
| commit | 559ddc4cc1406cec4093bef5a842c2f42c148cfd (patch) | |
| tree | d62f46dacdc06def5ab207747f123f611e69cd78 | |
| parent | c58ad10e57f96f4b1e649adbcd78c7c14c75508c (diff) | |
* Boogie and Dafny: added /cev:<file> option
* SscBoogie: changed default setting for /modifiesOnLoop
(we really should move this SscBoogie-specific code to the Spec# codeplex)
| -rw-r--r-- | DafnyDriver/DafnyDriver.ssc | 14 |
1 files changed, 14 insertions, 0 deletions
diff --git a/DafnyDriver/DafnyDriver.ssc b/DafnyDriver/DafnyDriver.ssc index 06280e74..8817f761 100644 --- a/DafnyDriver/DafnyDriver.ssc +++ b/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();
+ }
}
}
|