Commit message (Collapse) | Author | Age | ||
---|---|---|---|---|
... | ||||
* | Fix issue in verification result caching for assertions without subsumption. | wuestholz | 2014-10-13 | |
| | ||||
* | Added a test for the issue that was fixed in changeset 'e972f163bb7c'. | wuestholz | 2014-09-23 | |
| | ||||
* | Add missing run lines (based off Test/doomed/runtest.bat) to doomed | Dan Liew | 2014-09-21 | |
| | | | | | | | | tests. These are really broken because Boogie just seems to hang when they are executed. So they aren't executed right now. I'm not sure what to do with the other .bpl files. ``schaef`` left them lying around. | |||
* | more tests for houdini /inlineDepth | shuvendu | 2014-09-19 | |
| | ||||
* | a bug fix in Houdini (also AbsHoudini) | qadeer | 2014-09-19 | |
| | ||||
* | additional tests for houdini /inlineDepth | shuvendu | 2014-09-18 | |
| | ||||
* | merge | qadeer | 2014-08-08 | |
|\ | ||||
* | | fixed codexpr bug reported by Michael Emmi; removed special handling of ↵ | qadeer | 2014-08-08 | |
| | | | | | | | | codexpr in InjectPostConditions | |||
| * | Merge | Dan Rosén | 2014-08-01 | |
| |\ | |/ |/| | ||||
| * | Add alpha equivalence check for Expr, and use it when lambda lifting | Dan Rosén | 2014-08-01 | |
| | | ||||
* | | deleted the free assume about gates after parallel calls | qadeer | 2014-07-26 | |
|/ | ||||
* | enabled merging of yield calls | qadeer | 2014-07-20 | |
| | ||||
* | minor change | qadeer | 2014-07-19 | |
| | ||||
* | treiber stack fixed | qadeer | 2014-07-18 | |
| | ||||
* | some clean up | qadeer | 2014-07-16 | |
| | ||||
* | updated the linear type system based on Chris' design with linear, ↵ | qadeer | 2014-07-15 | |
| | | | | linear_in, linear_out | |||
* | simplified yield type chcking and added treiber stack (not fully done) | qadeer | 2014-07-15 | |
| | ||||
* | added tests | qadeer | 2014-07-12 | |
| | ||||
* | fixed some tests in og | qadeer | 2014-07-11 | |
| | | | | | added another test in linear (based on bug reported by Chris) removed the QED build configuration | |||
* | Worked on the more advanced verification result caching. | wuestholz | 2014-07-10 | |
| | ||||
* | Worked on the more advanced verification result caching. | wuestholz | 2014-07-10 | |
| | ||||
* | Worked on the more advanced verification result caching. | wuestholz | 2014-07-09 | |
| | ||||
* | Added more tests and worked on adding support for "canned errors". | wuestholz | 2014-07-06 | |
| | ||||
* | Worked on adding support for "canned errors". | wuestholz | 2014-07-06 | |
| | ||||
* | Did some refactoring, fixed minor issues, and made it apply the more ↵ | wuestholz | 2014-07-06 | |
| | | | | advanced verification result caching even for implementations with errors. | |||
* | Implemented an optimization for assignments to assumption variables that are ↵ | wuestholz | 2014-07-04 | |
| | | | | injected by the verification result caching for calls within loops. | |||
* | Fixed issue involving axioms in the dependency analysis used for ↵ | wuestholz | 2014-07-03 | |
| | | | | verification result caching. | |||
* | Optimized the way that assertions are marked as partially verified. | wuestholz | 2014-06-26 | |
| | ||||
* | Fixed issue in verification result caching. | wuestholz | 2014-06-26 | |
| | ||||
* | Add some pretty-printing, on by default. Turn off with the flag "/pretty:0" | Dan Rosén | 2014-06-24 | |
| | | | | | | When running boogie form the command line, this should be on by default. On the other hand, the TokenTextWriter constructors and PrintBplFile now have an argument for this, but by default it is off. | |||
* | Worked on an extension of the existing verification result caching. | wuestholz | 2014-06-23 | |
| | ||||
* | Changed the 'verifySnapshots' command-line option to accept a numeric ↵ | wuestholz | 2014-06-20 | |
| | | | | argument instead of a boolean one. | |||
* | Fixed crash in resolver | Rustan Leino | 2014-06-19 | |
| | ||||
* | updated golden outputs and removed irrelevant tests | qadeer | 2014-06-02 | |
| | ||||
* | Added more tests (snapshots). | wuestholz | 2014-05-30 | |
| | ||||
* | Documented the clean.py script | Dan Liew | 2014-05-28 | |
| | ||||
* | Document lit's ``-s`` option. | Dan Liew | 2014-05-28 | |
| | ||||
* | Remove a few other old test infrastructure files. They | Dan Liew | 2014-05-28 | |
| | | | | | probably aren't very useful anymore now that the old test infrastructure is gone. | |||
* | Removed old test infrastructure files except for | Dan Liew | 2014-05-28 | |
| | | | | | | | | | ./AbsHoudini/ ./doomed/ ./z3api/ ./test17/ because their conversion to lit incomplete. | |||
* | Merge | Dan Liew | 2014-05-28 | |
|\ | ||||
* | | Report the python version being used when executing lit. | Dan Liew | 2014-05-28 | |
| | | ||||
* | | Fix running pydiff.py under Python 2.7 | Dan Liew | 2014-05-28 | |
| | | ||||
| * | Updated an 'Answer' file (AbsHoudini). | wuestholz | 2014-05-28 | |
|/ | ||||
* | Merge | Dan Liew | 2014-05-27 | |
|\ | ||||
* | | Fix lit test suite when running Boogie under a path that contains | Dan Liew | 2014-05-27 | |
| | | | | | | | | spaces. | |||
| * | Merge | Ally Donaldson | 2014-05-27 | |
| |\ | |/ |/| | ||||
* | | Convert the AbsHoudini tests to lit tests. They weren't being run by the old | Dan Liew | 2014-05-27 | |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | infrastructure so I have not bothered to update the Answer file. These tests are still disabled by the lit.local.cfg file in the AbsHoudini folder because the following tests fail or weren't even being run previously (these are left unresolved because I do not know how these tests are meant to be run) UNRESOLVED: Boogie :: AbsHoudini/f1.bpl (1 of 32) UNRESOLVED: Boogie :: AbsHoudini/imp1.bpl (7 of 32) UNRESOLVED: Boogie :: AbsHoudini/int1.bpl (8 of 32) UNRESOLVED: Boogie :: AbsHoudini/multi.bpl (9 of 32) FAIL: Boogie :: AbsHoudini/quant3.bpl (22 of 32) FAIL: Boogie :: AbsHoudini/quant5.bpl (28 of 32) | |||
* | | Added simple python implementation of diff to replace using the | Dan Liew | 2014-05-27 | |
|/ | | | | | ``fc`` tool on windows because it is buggy when tests are run concurrently. | |||
* | Implemented an additional type check for assumption variables. | wuestholz | 2014-05-27 | |
| | ||||
* | Added more tests (snapshots). | wuestholz | 2014-05-27 | |
| |