Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Teach TravisCI to use Z3 4.4.1 from repositories that I'm currently | 2015-12-01 | |
| | | | | | | | | maintaining on the OpenSUSE build service. See https://build.opensuse.org/package/show/home:delcypher:z3/z3 | ||
* | Teach the TravisCI build to use the ``travis_retry`` command when | 2015-11-21 | |
| | | | | | | | | | using NuGet. The motivation here is that the ``nuget`` command is a little flakey (sometimes it times out) in the legacy TravisCI infrastructure. This command will retry the command passed to it a few times. Hopefully this will stop the random build failures we've been having. | ||
* | Add simplified may-unverified analysis and instrumentation. | 2015-11-20 | |
| | |||
* | Fix issue with partially-verified assertions. | 2015-11-19 | |
| | |||
* | Update test output after Nikolaj's enhancement in Z3. | 2015-11-19 | |
| | |||
* | Add a test. | 2015-11-19 | |
| | |||
* | Minor changes | 2015-11-19 | |
| | |||
* | Improve experimental support for optimization (requires Z3 changeset ↵ | 2015-11-18 | |
| | | | | 5948013b1b04d8529bce366c0c7b87e1d88a1827 or later). | ||
* | Add experimental support for optimization (requires Z3 build after changeset ↵ | 2015-11-18 | |
| | | | | 9cba63c31f6f1466dd4ef442bb840d1ab84539c7). | ||
* | Fix test output. | 2015-11-17 | |
| | |||
* | Fix issue #25. | 2015-11-17 | |
| | |||
* | Add a test. | 2015-11-16 | |
| | |||
* | Add a test. | 2015-11-16 | |
| | |||
* | Add support for identifying unnecessary assumes. | 2015-11-16 | |
| | |||
* | Merge pull request #22 from delcypher/proc_flag_fix | 2015-11-02 | |
|\ | | | | | Proc flag fix which addresses #16 | ||
| * | Document the new behaviour of the ``-proc:`` command line option | 2015-10-31 | |
| | | | | | | | | in the output of Boogie's help. | ||
| * | Added test cases for the new asterisk wildcard behaviour of the | 2015-10-31 | |
| | | | | | | | | ``-proc`` command line argument. | ||
| * | Added wild card matching for /proc flag | 2015-10-31 | |
|/ | |||
* | Add support for annotating implementations with k-ind. depth. | 2015-10-29 | |
| | |||
* | fix for deterministicExtractLoops for nested loops | 2015-10-27 | |
| | |||
* | fixed | 2015-10-26 | |
| | |||
* | Bug fix for deterministExtractLoops for Shaobo's example | 2015-10-26 | |
| | |||
* | bug fix in the type checking of calls to atomic procedures | 2015-10-16 | |
| | |||
* | 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 | |
| | |