Commit message (Collapse) | Author | Age | ||
---|---|---|---|---|
... | ||||
* | | | added a fix to check all layers: created layer of actions or layers in | 2015-10-01 | ||
| | | | | | | | | | | | | requires, ensures, or asserts | |||
| * | | Improve output for diagnosing timeouts. | 2015-10-01 | ||
|/ / | ||||
* | | another fix requested by Chris | 2015-10-01 | ||
| | | | | | | | | verification is performed now for all created layers | |||
* | | Improve output for diagnosing timeouts. | 2015-09-30 | ||
| | | ||||
* | | update | 2015-09-28 | ||
| | | ||||
* | | cleaned up some names | 2015-09-28 | ||
| | | ||||
* | | a bug fix | 2015-09-27 | ||
| | | ||||
* | | fixed a small bug | 2015-09-27 | ||
| | | ||||
* | | removed a warning | 2015-09-26 | ||
| | | ||||
* | | added introduced and ghost local variables | 2015-09-25 | ||
| | | ||||
| * | Modified BigFloat to avoid evaluating the floating point value before ↵ | 2015-09-23 | ||
| | | | | | | | | sending it to z3 | |||
| * | Added initial support for float addition | 2015-09-17 | ||
| | | ||||
* | | fixed my earlier to make it nicer | 2015-09-03 | ||
| | | ||||
* | | fixed a crash when there is no collector | 2015-09-02 | ||
| | | ||||
* | | Merge branch 'master' of https://github.com/boogie-org/boogie | 2015-08-28 | ||
|\ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | Conflicts: Source/Core/CommandLineOptions.cs Source/ExecutionEngine/ExecutionEngine.cs Source/ExecutionEngine/VerificationResultCache.cs Source/VCGeneration/VC.cs Test/snapshots/runtest.snapshot Test/snapshots/runtest.snapshot.expect | |||
* | | | Added /verifySnapshots:3, which prints recycled errors messages with the ↵ | 2015-08-28 | ||
| | | | | | | | | | | | | source locations of the new code. | |||
| | * | Float type now works correctly for simple variable declaration and comparison. | 2015-07-20 | ||
| | | | ||||
| * | | Merge branch 'master' of https://github.com/boogie-org/boogie | 2015-07-20 | ||
| |\ \ | ||||
| | * | | Minor additions to VC gen | 2015-07-20 | ||
| | | | | ||||
| * | | | fix for /deterministicExtractLoops sed in SymDiff | 2015-07-19 | ||
| |/ / | ||||
| | * | Modified internal abstract float representation to allow user-defined ↵ | 2015-07-13 | ||
| | | | | | | | | | | | | mantissa and exponent | |||
| * | | Update URL to boogie-partners to its new location on GitHub. | 2015-06-28 | ||
| | | | ||||
| * | | Fix issue #16 reported by @crazykt | 2015-06-28 | ||
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Previously when Boogie was passed the ``-proc:<NAME>`` argument on the command line it would verify any procedure whose name contained ``<NAME>`` which doesn't seem like correct behaviour. Now Boogie only tries to verify a procedure only if its name matches ``<NAME>`` exactly. I've added several test cases to check Boogie behaves as expected. | |||
| * | | Normalise line endings using a .gitattributes file. Unfortunately | 2015-06-28 | ||
| | | | | | | | | | | | | | | | | | | this required that this commit globally modify most files. If you want to use git blame to see the real author of a line use the ``-w`` flag so that whitespace changes are ignored. | |||
| * | | Remove dead file. | 2015-06-28 | ||
| | | | ||||
| * | | removed a stray Console.WriteLine that Ken had earlier checked in by | 2015-06-25 | ||
| | | | | | | | | | | | | mistake. | |||
| * | | Merge branch 'master' of https://github.com/boogie-org/boogie | 2015-06-20 | ||
| |\ \ | ||||
| * | | | Fix for reading fixpoint back into boogie exprs | 2015-06-20 | ||
| | | | | ||||
| * | | | Missing braces | 2015-06-20 | ||
| | | | | ||||
| | * | | modified desugaring so that in commutatitivity checks copies of original | 2015-06-17 | ||
| | | | | | | | | | | | | | | | | codeexpr is made. | |||
| | * | | fixed bug reported by Chris | 2015-06-15 | ||
| | | | | ||||
| | * | | adding z3name option | 2015-06-15 | ||
| |/ / | ||||
| * | | Minor changes | 2015-06-12 | ||
| | | | ||||
| * | | Fix issue with computation of statement checksums for lambda expressions. | 2015-06-12 | ||
| | | | ||||
| * | | Fix issue in checksum computation for lambda expressions. | 2015-06-12 | ||
| | | | ||||
| * | | Fix minor issue with diagnosing timeouts. | 2015-06-12 | ||
| | | | ||||
| * | | Merge branch 'master' of https://github.com/boogie-org/boogie | 2015-06-11 | ||
| |\ \ | ||||
| | * | | relaxed the check for created and hidden layers for skip actions | 2015-06-10 | ||
| | | | | ||||
| | * | | fixed crash | 2015-06-10 | ||
| | | | | ||||
| * | | | various changes for duality from dead codeplex repo | 2015-06-09 | ||
|/ / / | ||||
| * / | Stop truncating the prover logs | 2015-06-09 | ||
|/ / | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | As it stands, Boogie abruptly aborts the prover by calling Kill() on the associated process after receiving responses to all of its queries. In most cases this is fine, but in general this is pretty bad: it yields to all sorts of output corruption when user-supplied options require z3 to write output to an auxiliary file (say, using /z3opt:TRACE=true). This explains why VCC's Axiom Profiler often complains about a missing [eof] after running Boogie with /z3opt:TRACE=true. This patch fixes it by only falling back to Kill if the process seems to have become unresponsive. That is, it starts by cleanly closing the process input, which signals the end of the interactive session. It then waits for a clean exit for 2s, and only after that does it resort to calling Kill(). I've striven for minimal modifications to the logic, so the patch still universally swallows errors that might occur while closing the underlying stream, and still calls Kill() (I wouldn't be against Boogie just hanging if z3 hangs too). On my tests, z3 exits cleanly pretty much instantly after input is closed anyway, so I don't expect the timeout to fire often (which would be one more reason to actually remove that timeout, and condition Boogie's exit on that of z3 IMO). | |||
* | | Improve support for diagnosing timeouts. | 2015-06-08 | ||
| | | ||||
* | | Fix minor issue. | 2015-06-05 | ||
| | | ||||
* | | Improve support for diagnosing timeouts. | 2015-06-05 | ||
| | | ||||
* | | Fix for SI: initialize extraRecBound | 2015-06-05 | ||
| | | ||||
* | | Merge branch 'master' of https://github.com/boogie-org/boogie | 2015-06-01 | ||
|\ \ | ||||
* | | | Simplified StratifiedVC interface | 2015-06-01 | ||
| | | | ||||
| * | | Merge branch 'master' of https://github.com/boogie-org/boogie | 2015-05-31 | ||
| |\ \ | |/ / |/| | | ||||
| * | | added assume about gate after calls and parallel calls | 2015-05-31 | ||
| | | | ||||
* | | | Improve heuristics for diagnosing timeouts. | 2015-05-31 | ||
|/ / |