summaryrefslogtreecommitdiff
path: root/Source/BoogieDriver
diff options
context:
space:
mode:
authorGravatar rustanleino <unknown>2009-09-15 22:10:28 +0000
committerGravatar rustanleino <unknown>2009-09-15 22:10:28 +0000
commit7d9a1e78eb07f592065a69db862d92014d5c1894 (patch)
tree5010573d6555ff09f90082271180894aed026b26 /Source/BoogieDriver
parent9e7c3594b662f1c3102d419104da453d83eddfcd (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)
Diffstat (limited to 'Source/BoogieDriver')
-rw-r--r--Source/BoogieDriver/BoogieDriver.ssc14
1 files changed, 14 insertions, 0 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();
+ }
}
}