Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | 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 |
| | |||
* | changed aux attribute to ghost | qadeer | 2015-04-18 |
| | |||
* | 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 |
| | |||
* | strengthened type checking | qadeer | 2014-12-26 |
| | | | | | cleaned up the generation of mover checks (based on example from Chris) added two examples from Chris to regressions | ||
* | changed type checking of yield procedures so that they can only call other ↵ | qadeer | 2014-12-18 |
| | | | | yielding procedures | ||
* | 1. made variable introduction layer explicit in the test cases | qadeer | 2014-12-15 |
| | | | | 2. if a single layer is specified for a global variable, that layer is the introduction layer | ||
* | patched an expected output | qadeer | 2014-12-15 |
| | |||
* | Worked on the verification result caching (extracted functions). | wuestholz | 2014-11-25 |
| | |||
* | Fixed issues in the verification result caching (old expressions). | wuestholz | 2014-11-24 |
| | |||
* | Fixed issue in the verification result caching. | wuestholz | 2014-11-10 |
| | |||
* | Worked on the verification result caching. | wuestholz | 2014-11-10 |
| | |||
* | Made it never include the statement checksum when printing assert statements. | wuestholz | 2014-11-16 |
| |