summaryrefslogtreecommitdiff
path: root/Test
Commit message (Collapse)AuthorAge
...
* Fix issue in verification result caching for assertions without subsumption.Gravatar wuestholz2014-10-13
|
* Added a test for the issue that was fixed in changeset 'e972f163bb7c'.Gravatar wuestholz2014-09-23
|
* Add missing run lines (based off Test/doomed/runtest.bat) to doomedGravatar Dan Liew2014-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 /inlineDepthGravatar shuvendu2014-09-19
|
* a bug fix in Houdini (also AbsHoudini)Gravatar qadeer2014-09-19
|
* additional tests for houdini /inlineDepthGravatar shuvendu2014-09-18
|
* mergeGravatar qadeer2014-08-08
|\
* | fixed codexpr bug reported by Michael Emmi; removed special handling of ↵Gravatar qadeer2014-08-08
| | | | | | | | codexpr in InjectPostConditions
| * MergeGravatar Dan Rosén2014-08-01
| |\ | |/ |/|
| * Add alpha equivalence check for Expr, and use it when lambda liftingGravatar Dan Rosén2014-08-01
| |
* | deleted the free assume about gates after parallel callsGravatar qadeer2014-07-26
|/
* enabled merging of yield callsGravatar qadeer2014-07-20
|
* minor changeGravatar qadeer2014-07-19
|
* treiber stack fixedGravatar qadeer2014-07-18
|
* some clean upGravatar qadeer2014-07-16
|
* updated the linear type system based on Chris' design with linear, ↵Gravatar qadeer2014-07-15
| | | | linear_in, linear_out
* simplified yield type chcking and added treiber stack (not fully done)Gravatar qadeer2014-07-15
|
* added testsGravatar qadeer2014-07-12
|
* fixed some tests in ogGravatar qadeer2014-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.Gravatar wuestholz2014-07-10
|
* Worked on the more advanced verification result caching.Gravatar wuestholz2014-07-10
|
* Worked on the more advanced verification result caching.Gravatar wuestholz2014-07-09
|
* Added more tests and worked on adding support for "canned errors".Gravatar wuestholz2014-07-06
|
* Worked on adding support for "canned errors".Gravatar wuestholz2014-07-06
|
* Did some refactoring, fixed minor issues, and made it apply the more ↵Gravatar wuestholz2014-07-06
| | | | advanced verification result caching even for implementations with errors.
* Implemented an optimization for assignments to assumption variables that are ↵Gravatar wuestholz2014-07-04
| | | | injected by the verification result caching for calls within loops.
* Fixed issue involving axioms in the dependency analysis used for ↵Gravatar wuestholz2014-07-03
| | | | verification result caching.
* Optimized the way that assertions are marked as partially verified.Gravatar wuestholz2014-06-26
|
* Fixed issue in verification result caching.Gravatar wuestholz2014-06-26
|
* Add some pretty-printing, on by default. Turn off with the flag "/pretty:0"Gravatar Dan Rosén2014-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.Gravatar wuestholz2014-06-23
|
* Changed the 'verifySnapshots' command-line option to accept a numeric ↵Gravatar wuestholz2014-06-20
| | | | argument instead of a boolean one.
* Fixed crash in resolverGravatar Rustan Leino2014-06-19
|
* updated golden outputs and removed irrelevant testsGravatar qadeer2014-06-02
|
* Added more tests (snapshots).Gravatar wuestholz2014-05-30
|
* Documented the clean.py scriptGravatar Dan Liew2014-05-28
|
* Document lit's ``-s`` option.Gravatar Dan Liew2014-05-28
|
* Remove a few other old test infrastructure files. TheyGravatar Dan Liew2014-05-28
| | | | | probably aren't very useful anymore now that the old test infrastructure is gone.
* Removed old test infrastructure files except forGravatar Dan Liew2014-05-28
| | | | | | | | | ./AbsHoudini/ ./doomed/ ./z3api/ ./test17/ because their conversion to lit incomplete.
* MergeGravatar Dan Liew2014-05-28
|\
* | Report the python version being used when executing lit.Gravatar Dan Liew2014-05-28
| |
* | Fix running pydiff.py under Python 2.7Gravatar Dan Liew2014-05-28
| |
| * Updated an 'Answer' file (AbsHoudini).Gravatar wuestholz2014-05-28
|/
* MergeGravatar Dan Liew2014-05-27
|\
* | Fix lit test suite when running Boogie under a path that containsGravatar Dan Liew2014-05-27
| | | | | | | | spaces.
| * MergeGravatar Ally Donaldson2014-05-27
| |\ | |/ |/|
* | Convert the AbsHoudini tests to lit tests. They weren't being run by the oldGravatar Dan Liew2014-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 theGravatar Dan Liew2014-05-27
|/ | | | | ``fc`` tool on windows because it is buggy when tests are run concurrently.
* Implemented an additional type check for assumption variables.Gravatar wuestholz2014-05-27
|
* Added more tests (snapshots).Gravatar wuestholz2014-05-27
|