Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | (Honestly, I don't know what I'm doing. I'm trying to revert these changes, ↵ | 2016-02-12 | |
| | | | | but Git doesn't actually say what sort of commit I'm doing. Well, here goes.) | ||
* | bug fix | 2015-10-09 | |
| | |||
* | removed an extraneous warning | 2015-10-08 | |
| | |||
* | Merge branch 'master' of https://github.com/boogie-org/boogie | 2015-10-01 | |
|\ | |||
* | | 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 | |
| | |||
* | 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. | ||
| * | Merge branch 'master' of https://github.com/boogie-org/boogie | 2015-07-20 | |
| |\ | |||
| | * | Added another test. | 2015-07-20 | |
| | | | |||
| | * | Merge branch 'master' of https://github.com/boogie-org/boogie | 2015-07-20 | |
| | |\ | |||
| | * | | Minor additions to VC gen | 2015-07-20 | |
| | | | | |||
| | | * | Added more tests. | 2015-07-20 | |
| | |/ | |||
| * / | fix for /deterministicExtractLoops sed in SymDiff | 2015-07-19 | |
| |/ | |||
| * | Try to unbreak the tests added in | 2015-06-28 | |
| | | | | | | | | 7f4e6b0fab58bb3028cd0f1734fc97b3feafefdf under Windows. | ||
| * | 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. | ||
| * | Add travis file to gitattributes file. | 2015-06-28 | |
| | | |||
| * | 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. | ||
| * | updated with Serdar's changes | 2015-06-25 | |
| | | |||
| * | 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 | |
| | | | |||
| | * | added another sample | 2015-06-17 | |
| | | | |||
| | * | 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 | |
| | | |||
| * | Add a test case. | 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 | |
| | | | |||
| | * | Merge pull request #14 from cpitclaudel/clean-prover-exit | 2015-06-09 | |
| |/| |/| | | | | | Stop truncating the prover logs | ||
| * | | 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). |