Commit message (Collapse) | Author | Age | ||
---|---|---|---|---|
... | ||||
* | | 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 | |
| | | | ||||
| | * | Began adding the float type to VC expression | Dietrich | 2015-04-27 | |
| | | | ||||
| * | | 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 | |
| | | ||||
* | | changed aux attribute to ghost | qadeer | 2015-04-18 | |
| | | ||||
| * | Added the fp32 class, copied from the previously existing BigDec class. No ↵ | Dietrich | 2015-04-17 | |
| | | | | | | | | significant changes from BigDec have been made | |||
* | | first check in | qadeer | 2015-04-16 | |
|/ | ||||
* | Disable test is ``Test/Secure``. They aren't set up properly. | Dan Liew | 2015-04-05 | |
| | ||||
* | Some test cases for SecureVCGen (disabled for lit currently) | akashlal | 2015-04-05 | |
| | ||||
* | Fix ``Test/test15/CaptureState.bpl`` test under Linux. | Dan Liew | 2015-04-03 | |
| | ||||
* | Fix ``livevars/daytona_bug2_ioctl_example_2.bpl`` test under Linux. | Dan Liew | 2015-04-03 | |
| | ||||
* | updated the example to include atomic specifications (sent by Suha) | qadeer | 2015-03-29 | |
| | ||||
* | fixed crash reported by Dan. | qadeer | 2015-03-02 | |
| | | | | DoModSetAnalysis needs to run before the linear and mover type checking. | |||
* | fix from Serdar and Suha | qadeer | 2015-02-24 | |
| | ||||
* | moved some things around | qadeer | 2015-02-11 | |
| | ||||
* | minor fix to the golden file | qadeer | 2015-01-28 | |
| | ||||
* | added lit stuff at the top of the file and the golden output | qadeer | 2015-01-28 | |
| | ||||
* | Work stealing queue (PLDI '12 Vechev et al.) | Unknown | 2015-01-28 | |
| | ||||
* | Merge | qadeer | 2015-01-27 | |
|\ | ||||
* | | removed unused functions and axioms to make the verification faster | qadeer | 2015-01-27 | |
| | | ||||
| * | Worked on the verification result caching (use weights for extracted functions). | wuestholz | 2015-01-24 | |
| | | ||||
| * | Worked on the verification result caching (use native support for partially ↵ | wuestholz | 2015-01-16 | |
|/ | | | | verified assertions). | |||
* | Added a test and a todo. | wuestholz | 2015-01-02 | |
| | ||||
* | Minor change in verification result caching (extracted functions) | wuestholz | 2014-12-28 | |
| |