Boogie: Cannot show error messages in VS2010

Mar 30, 2012 at 7:09 PM

Mimicing Dafny, I renamed a copy of "StartDafny.bat" as "StartBoogie.bat" and made some changes as below:

@echo offecho ---------- Starting ------------ < nul >> c:\tmp\boo.outtime < nul >> c:\tmp\boo.outecho. < nul >> c:\tmp\boo.out
"c:\boogie\Binaries\Boogie.exe" -nologo stdin.bpl -timeLimit:10 %* 2>> c:\tmp\boo.out
time < nul >> c:\tmp\boo.outecho. < nul >> c:\tmp\boo.outecho ---------- Done ------------ < nul >> c:\tmp\boo.out


The errors of a boogie file with some errors cannot be shown in VS2010. It seems the StandardOutput is not redirected. 

I am wondering if you have any solution.



Apr 5, 2012 at 12:17 AM

Strange.  What you did works for me.  I presume you have built (using the regular VS 2010) Util\VS2010\Boogie\BoogieLanguageService.sln and then you're opening the Boogie programs (for example, Test\textbook\Find.bpl) in the Experimental Instance of VS 2010 (just like you would for Dafny)?  You should then be able to see in the c:\tmp\boo.out file that Boogie has indeed been run on the file in VS.

When you say StandardOutput is not redirected, are you referring to the output that Boogie is producing?