Commit message (Collapse) | Author | Age | ||
---|---|---|---|---|
... | ||||
* | | fixed a small bug | 2015-09-27 | ||
| | | ||||
* | | added introduced and ghost local variables | 2015-09-25 | ||
| | | ||||
* | | 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. | |||
| * | | Added another test. | 2015-07-20 | ||
| | | | ||||
| * | | Added more tests. | 2015-07-20 | ||
| | | | ||||
| * | | Try to unbreak the tests added in | 2015-06-28 | ||
| | | | | | | | | | | | | 7f4e6b0fab58bb3028cd0f1734fc97b3feafefdf under Windows. | |||
| * | | 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. | |||
| * | | updated with Serdar's changes | 2015-06-25 | ||
| | | | ||||
| * | | 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 | ||
| | | | ||||
| * | | Fix issue with computation of statement checksums for lambda expressions. | 2015-06-12 | ||
| | | | ||||
| * | | Add a test case. | 2015-06-12 | ||
| | | | ||||
| * | | relaxed the check for created and hidden layers for skip actions | 2015-06-10 | ||
| | | | ||||
| * | | fixed crash | 2015-06-10 | ||
|/ / | ||||
* | | bug fix in pop | 2015-05-27 | ||
| | | ||||
* | | Merge branch 'master' of https://github.com/boogie-org/boogie | 2015-05-20 | ||
|\ \ | ||||
* | | | added more specifications | 2015-05-20 | ||
| | | | ||||
| * | | Make caching of verification results more fine-grained for changes that ↵ | 2015-05-17 | ||
| | | | | | | | | | | | | affect preconditions. | |||
| * | | SecureVC: example | 2015-05-07 | ||
| | | | ||||
| * | | Make it preserve the fact that the value of an assumption variable never ↵ | 2015-05-06 | ||
| | | | | | | | | | | | | becomes logically weaker after a havoc. | |||
| * | | Add support for 'verified_under' attributes on procedure calls and invariants. | 2015-04-29 | ||
| | | | ||||
| | * | Began adding the float type to VC expression | 2015-04-27 | ||
| | | | ||||
| * | | Try to fix the emission of invalid SMT-LIBv2 queries when Boogie has a | 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 | 2015-04-22 | ||
| | | ||||
* | | added more examples | 2015-04-18 | ||
| | | ||||
* | | patched ghost checking | 2015-04-18 | ||
| | | ||||
* | | changed aux attribute to ghost | 2015-04-18 | ||
| | | ||||
| * | Added the fp32 class, copied from the previously existing BigDec class. No ↵ | 2015-04-17 | ||
| | | | | | | | | significant changes from BigDec have been made | |||
* | | first check in | 2015-04-16 | ||
|/ | ||||
* | Disable test is ``Test/Secure``. They aren't set up properly. | 2015-04-05 | ||
| | ||||
* | Some test cases for SecureVCGen (disabled for lit currently) | 2015-04-05 | ||
| | ||||
* | Fix ``Test/test15/CaptureState.bpl`` test under Linux. | 2015-04-03 | ||
| | ||||
* | Fix ``livevars/daytona_bug2_ioctl_example_2.bpl`` test under Linux. | 2015-04-03 | ||
| | ||||
* | updated the example to include atomic specifications (sent by Suha) | 2015-03-29 | ||
| | ||||
* | fixed crash reported by Dan. | 2015-03-02 | ||
| | | | | DoModSetAnalysis needs to run before the linear and mover type checking. | |||
* | fix from Serdar and Suha | 2015-02-24 | ||
| | ||||
* | moved some things around | 2015-02-11 | ||
| | ||||
* | minor fix to the golden file | 2015-01-28 | ||
| | ||||
* | added lit stuff at the top of the file and the golden output | 2015-01-28 | ||
| | ||||
* | Work stealing queue (PLDI '12 Vechev et al.) | 2015-01-28 | ||
| | ||||
* | Merge | 2015-01-27 | ||
|\ | ||||
* | | removed unused functions and axioms to make the verification faster | 2015-01-27 | ||
| | | ||||
| * | Worked on the verification result caching (use weights for extracted functions). | 2015-01-24 | ||
| | | ||||
| * | Worked on the verification result caching (use native support for partially ↵ | 2015-01-16 | ||
|/ | | | | verified assertions). | |||
* | Added a test and a todo. | 2015-01-02 | ||
| | ||||
* | Minor change in verification result caching (extracted functions) | 2014-12-28 | ||
| |