Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Improve precision of abstract interpreter for modulo operations. | Valentin Wüstholz | 2015-12-28 |
| | |||
* | 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. | ||
* | Update test output for Z3 4.4.1. | Valentin Wüstholz | 2015-12-01 |
| | |||
* | Fix issue with partially-verified assertions. | Valentin Wüstholz | 2015-11-19 |
| | |||
* | Update test output after Nikolaj's enhancement in Z3. | Valentin Wüstholz | 2015-11-19 |
| | |||
* | Add a test. | Valentin Wüstholz | 2015-11-19 |
| | |||
* | Minor changes | Valentin Wüstholz | 2015-11-19 |
| | |||
* | Improve experimental support for optimization (requires Z3 changeset ↵ | Valentin Wüstholz | 2015-11-18 |
| | | | | 5948013b1b04d8529bce366c0c7b87e1d88a1827 or later). | ||
* | Add experimental support for optimization (requires Z3 build after changeset ↵ | Valentin Wüstholz | 2015-11-18 |
| | | | | 9cba63c31f6f1466dd4ef442bb840d1ab84539c7). | ||
* | Fix test output. | Valentin Wüstholz | 2015-11-17 |
| | |||
* | Fix issue #25. | Valentin Wüstholz | 2015-11-17 |
| | |||
* | Add a test. | Valentin Wüstholz | 2015-11-16 |
| | |||
* | Add a test. | Valentin Wüstholz | 2015-11-16 |
| | |||
* | Add support for identifying unnecessary assumes. | Valentin Wüstholz | 2015-11-16 |
| | |||
* | Added test cases for the new asterisk wildcard behaviour of the | Dan Liew | 2015-10-31 |
| | | | | ``-proc`` command line argument. | ||
* | fix for deterministicExtractLoops for nested loops | Shuvendu Lahiri | 2015-10-27 |
| | |||
* | fixed | Shaz Qadeer | 2015-10-26 |
| | |||
* | 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 |
| | |||
* | another fix requested by Chris | Shaz Qadeer | 2015-10-01 |
| | | | | verification is performed now for all created layers | ||
* | fixed a small bug | Shaz Qadeer | 2015-09-27 |
| | |||
* | added introduced and ghost local variables | Shaz Qadeer | 2015-09-25 |
| | |||
* | 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. | ||
| * | Added another test. | Valentin Wüstholz | 2015-07-20 |
| | | |||
| * | Added more tests. | Valentin Wüstholz | 2015-07-20 |
| | | |||
| * | Try to unbreak the tests added in | Dan Liew | 2015-06-28 |
| | | | | | | | | 7f4e6b0fab58bb3028cd0f1734fc97b3feafefdf under Windows. | ||
| * | 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. | ||
| * | updated with Serdar's changes | qadeer | 2015-06-25 |
| | | |||
| * | added another sample | qadeer | 2015-06-17 |
| | | |||
| * | 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 |
| | | |||
| * | Fix issue with computation of statement checksums for lambda expressions. | Valentin Wüstholz | 2015-06-12 |
| | | |||
| * | Add a test case. | Valentin Wüstholz | 2015-06-12 |
| | | |||
| * | relaxed the check for created and hidden layers for skip actions | qadeer | 2015-06-10 |
| | | |||
| * | fixed crash | qadeer | 2015-06-10 |
|/ | |||
* | bug fix in pop | qadeer | 2015-05-27 |
| | |||
* | Merge branch 'master' of https://github.com/boogie-org/boogie | qadeer | 2015-05-20 |
|\ | |||
* | | added more specifications | qadeer | 2015-05-20 |
| | | |||
| * | Make caching of verification results more fine-grained for changes that ↵ | Valentin Wüstholz | 2015-05-17 |
| | | | | | | | | affect preconditions. | ||
| * | SecureVC: example | Akash Lal | 2015-05-07 |
| | | |||
| * | Make it preserve the fact that the value of an assumption variable never ↵ | Valentin Wüstholz | 2015-05-06 |
| | | | | | | | | becomes logically weaker after a havoc. | ||
| * | Add support for 'verified_under' attributes on procedure calls and invariants. | Valentin Wüstholz | 2015-04-29 |
| | | |||
| * | Try to fix the emission of invalid SMT-LIBv2 queries when Boogie has a | Dan Liew | 2015-04-26 |
|/ | | | | | variable that begins with a ``.``. This was't an issue for Z3 which ignores this but CVC4 is stricter and will emit an error | ||
* | renamed og to civl | qadeer | 2015-04-22 |
| | |||
* | added more examples | qadeer | 2015-04-18 |
| | |||
* | patched ghost checking | qadeer | 2015-04-18 |
| |