Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Fix deadlock in the new thread scheduler | 2016-08-12 | |
| | | | | | | | | Fix deadlock where a Boogie task schedules a task and waits on it. The .NET threadpool creates more threads than cores, up to a limit, which hides the issue. The new policy did not account for recursion and caused the newly-created tasks to wait forever for the earlier ones to complete. | ||
* | Run Boogie code on threads with large stacks | 2016-07-22 | |
| | | | | | | | Replace TaskScheduler.Default by a custom TaskScheduler. The .Default uses threadpool threads whose stack size is controlled by the host EXE header. The new ThreadTaskScheduler give Boogie control over the stack size, and defaults to 16mb. | ||
* | Rename DLLs to non-generic names by prefixing "Boogie". Project names and | 2016-04-15 | |
| | | | | namespaces remain the same. | ||
* | Improve support for identifying unnecessary assumes. | 2016-03-09 | |
| | |||
* | Add support for weights on soft assumes. | 2016-03-07 | |
| | |||
* | Improve support for optimization and identifying unnecessary assumes. | 2016-03-03 | |
| | |||
* | Bug fix in determining whether a type parameter is bounded | 2016-01-19 | |
| | | | | | | When checking whether a type parameter could be determined from the bound variable types, we mistakenly compare equality between a TypeVarable and a VCExprVar, instead of between two VCExprVars. | ||
* | Minor change | 2015-12-29 | |
| | |||
* | Fix issue with ids for assume-statements. | 2015-12-28 | |
| | |||
* | Improve precision of abstract interpreter for modulo operations. | 2015-12-28 | |
| | |||
* | Enable optimization for more prover queries. | 2015-12-27 | |
| | |||
* | Remove unused file. | 2015-12-03 | |
| | |||
* | Remove workaround for older versions of Z3. | 2015-12-02 | |
| | |||
* | Use the EndCurly token when creating the ReturnCmd for unifiedExit | 2015-12-02 | |
| | | | | | | | | When there are more than one exit blocks, an unified exit block is created which includes a ReturnCmd. However, the ReturnCmd is created with NoToken. This causes the line/column number reported for a failed postcondition to be (0,0). The right token should be the EndCurly since the ReturnCmd is in the exit block. | ||
* | Add simplified may-unverified analysis and instrumentation. | 2015-11-20 | |
| | |||
* | Fix issue with partially-verified assertions. | 2015-11-19 | |
| | |||
* | Minor changes | 2015-11-19 | |
| | |||
* | Add experimental support for optimization (requires Z3 build after changeset ↵ | 2015-11-18 | |
| | | | | 9cba63c31f6f1466dd4ef442bb840d1ab84539c7). | ||
* | Fix issue #25. | 2015-11-17 | |
| | |||
* | Add support for identifying unnecessary assumes. | 2015-11-16 | |
| | |||
* | Document the new behaviour of the ``-proc:`` command line option | 2015-10-31 | |
| | | | | in the output of Boogie's help. | ||
* | 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 | |
| | |||
* | 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 | |
| |\ | |||
| | * | Minor additions to VC gen | 2015-07-20 | |
| | | | |||
| * | | fix for /deterministicExtractLoops sed in SymDiff | 2015-07-19 | |
| |/ | |||
| * | 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 | |
| | |