Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Remove unused file. | Valentin Wüstholz | 2015-12-03 |
| | |||
* | Remove workaround for older versions of Z3. | Valentin Wüstholz | 2015-12-02 |
| | |||
* | Use the EndCurly token when creating the ReturnCmd for unifiedExit | qunyanm | 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. | Valentin Wüstholz | 2015-11-20 |
| | |||
* | Fix issue with partially-verified assertions. | Valentin Wüstholz | 2015-11-19 |
| | |||
* | Minor changes | Valentin Wüstholz | 2015-11-19 |
| | |||
* | Add experimental support for optimization (requires Z3 build after changeset ↵ | Valentin Wüstholz | 2015-11-18 |
| | | | | 9cba63c31f6f1466dd4ef442bb840d1ab84539c7). | ||
* | Fix issue #25. | Valentin Wüstholz | 2015-11-17 |
| | |||
* | Add support for identifying unnecessary assumes. | Valentin Wüstholz | 2015-11-16 |
| | |||
* | Document the new behaviour of the ``-proc:`` command line option | Dan Liew | 2015-10-31 |
| | | | | in the output of Boogie's help. | ||
* | Added wild card matching for /proc flag | Shaobo | 2015-10-31 |
| | |||
* | Add support for annotating implementations with k-ind. depth. | Valentin Wüstholz | 2015-10-29 |
| | |||
* | fix for deterministicExtractLoops for nested loops | Shuvendu Lahiri | 2015-10-27 |
| | |||
* | Bug fix for deterministExtractLoops for Shaobo's example | Shuvendu Lahiri | 2015-10-26 |
| | |||
* | bug fix in the type checking of calls to atomic procedures | Shaz Qadeer | 2015-10-16 |
| | |||
* | bug fix | Shaz Qadeer | 2015-10-09 |
| | |||
* | removed an extraneous warning | Shaz Qadeer | 2015-10-08 |
| | |||
* | Merge branch 'master' of https://github.com/boogie-org/boogie | Shaz Qadeer | 2015-10-01 |
|\ | |||
* | | added a fix to check all layers: created layer of actions or layers in | Shaz Qadeer | 2015-10-01 |
| | | | | | | | | requires, ensures, or asserts | ||
| * | Improve output for diagnosing timeouts. | Valentin Wüstholz | 2015-10-01 |
|/ | |||
* | another fix requested by Chris | Shaz Qadeer | 2015-10-01 |
| | | | | verification is performed now for all created layers | ||
* | Improve output for diagnosing timeouts. | Valentin Wüstholz | 2015-09-30 |
| | |||
* | update | Shaz Qadeer | 2015-09-28 |
| | |||
* | cleaned up some names | Shaz Qadeer | 2015-09-28 |
| | |||
* | a bug fix | Shaz Qadeer | 2015-09-27 |
| | |||
* | fixed a small bug | Shaz Qadeer | 2015-09-27 |
| | |||
* | removed a warning | Shaz Qadeer | 2015-09-26 |
| | |||
* | added introduced and ghost local variables | Shaz Qadeer | 2015-09-25 |
| | |||
* | fixed my earlier to make it nicer | Shaz Qadeer | 2015-09-03 |
| | |||
* | fixed a crash when there is no collector | Shaz Qadeer | 2015-09-02 |
| | |||
* | Merge branch 'master' of https://github.com/boogie-org/boogie | Rustan Leino | 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 ↵ | Rustan Leino | 2015-08-28 |
| | | | | | | | | source locations of the new code. | ||
| * | Merge branch 'master' of https://github.com/boogie-org/boogie | Shuvendu Lahiri | 2015-07-20 |
| |\ | |||
| | * | Minor additions to VC gen | Akash Lal | 2015-07-20 |
| | | | |||
| * | | fix for /deterministicExtractLoops sed in SymDiff | Shuvendu Lahiri | 2015-07-19 |
| |/ | |||
| * | Update URL to boogie-partners to its new location on GitHub. | Dan Liew | 2015-06-28 |
| | | |||
| * | Fix issue #16 reported by @crazykt | Dan Liew | 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 | Dan Liew | 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. | Dan Liew | 2015-06-28 |
| | | |||
| * | removed a stray Console.WriteLine that Ken had earlier checked in by | qadeer | 2015-06-25 |
| | | | | | | | | mistake. | ||
| * | Merge branch 'master' of https://github.com/boogie-org/boogie | akashlal | 2015-06-20 |
| |\ | |||
| * | | Fix for reading fixpoint back into boogie exprs | akashlal | 2015-06-20 |
| | | | |||
| * | | Missing braces | akashlal | 2015-06-20 |
| | | | |||
| | * | modified desugaring so that in commutatitivity checks copies of original | qadeer | 2015-06-17 |
| | | | | | | | | | | | | codeexpr is made. | ||
| | * | fixed bug reported by Chris | qadeer | 2015-06-15 |
| | | | |||
| | * | adding z3name option | Ken McMillan | 2015-06-15 |
| |/ | |||
| * | Minor changes | Valentin Wüstholz | 2015-06-12 |
| | | |||
| * | Fix issue with computation of statement checksums for lambda expressions. | Valentin Wüstholz | 2015-06-12 |
| | | |||
| * | Fix issue in checksum computation for lambda expressions. | Valentin Wüstholz | 2015-06-12 |
| | | |||
| * | Fix minor issue with diagnosing timeouts. | Valentin Wüstholz | 2015-06-12 |
| | |