that pretty much says it all
Id #10247 | Release:
| Updated: Feb 25, 2015 at 8:53 PM by nimrodpar | Created: Feb 25, 2015 at 8:53 PM by nimrodpar
I'm currently using Boogie as a library and there is an issue that makes it incredibly painful to use. The issue is lots of the code refers to CommandLineOptions.Clo which is the global command lin...
Id #10244 | Release:
| Updated: Oct 21, 2014 at 11:40 AM by danliew | Created: Oct 21, 2014 at 11:40 AM by danliew
The tests in Test/doomed are really broken. If the lit.local.cfg is removed (this is preventing them from being executed) then they hang! Some .bpl files in that directory aren't use either.
Id #10243 | Release:
| Updated: Sep 21, 2014 at 9:21 PM by danliew | Created: Sep 21, 2014 at 9:21 PM by danliew
The tests in Test/AbsHoudini are currently disabled because some of them are broken. This is bad because we aren't tracking regressions introduced for this feature.
UNRESOLVED: Boogie :: AbsHoudini...
Id #10242 | Release:
| Updated: Sep 21, 2014 at 8:56 PM by danliew | Created: Sep 21, 2014 at 8:56 PM by danliew
The current version of Boogie ("version 2.2.30705.1126") from Codeplex without any command line flags falsely reports an error on the following program.
procedure p() returns ($r: int)
Id #10241 | Release:
| Updated: Aug 7, 2014 at 6:45 PM by mje | Created: Jul 31, 2014 at 3:24 PM by mje
I've generated a Boogie file that passes the type checker but crashes Boogie with a violated assertion. Certainly, there is a bug in the generated file, but maybe it should not crash Booige.
Id #10237 | Release:
| Updated: May 8, 2013 at 1:42 AM by schaef | Created: May 8, 2013 at 1:42 AM by schaef
The Boogie Verification Debugger (BVD) crashes with an example model file that was generated by Dafny. I've attached the input Dafny file. The version of Dafny I used was: Dafny program...
Id #10236 | Release:
| Updated: Apr 2, 2013 at 12:57 AM by jaltidor | Created: Apr 2, 2013 at 12:52 AM by jaltidor
Just started playing with Boogie after installing as oppose to using the rise4fun website.....
I ended up crashing it by removing an assert in the quicksort example on the website
Id #10235 | Release:
| Updated: Mar 5, 2013 at 10:19 PM by bmellow | Created: Mar 5, 2013 at 10:17 PM by bmellow
first of all thank you very much for adding support for real values to Boogie.
Unfortunately there are two bugs, when using reals in a Boogie file:
First: Boogie and BVD are not able to p...
Id #10234 | Release:
| Updated: Nov 21, 2012 at 5:16 PM by reicherdt | Created: Nov 21, 2012 at 5:16 PM by reicherdt
there is a small bug in the processing of command line arguments in BVD.
When using a full path of a model file including the drive letter, BVD splits the path on the ":" of "C:...".
Id #10233 | Release:
| Updated: Nov 21, 2012 at 4:53 PM by reicherdt | Created: Nov 21, 2012 at 4:53 PM by reicherdt