summaryrefslogtreecommitdiff
path: root/Test
Commit message (Expand)AuthorAge
* Add a 'tutorial' folder to the distribution, with an initial example.Gravatar Clément Pit--Claudel2015-08-22
* MergeGravatar Clément Pit--Claudel2015-08-21
|\
* | Make `old` a special case for trigger generation.Gravatar Clément Pit--Claudel2015-08-21
* | Rephrase the message about triggers being rejected because they are too strongGravatar Clément Pit--Claudel2015-08-21
* | Add a few things to the wishlistGravatar Clément Pit--Claudel2015-08-21
* | Adjust WF checks to use unsplit quantifiers.Gravatar Clément Pit--Claudel2015-08-21
| * Make use of new syntax in a test fileGravatar Rustan Leino2015-08-21
* | Interleave stderr output with test results; this allows one to print stuffGravatar Clément Pit--Claudel2015-08-21
* | Ignore flycheck_* files in runTestsGravatar Clément Pit--Claudel2015-08-21
* | Add tests for display expressions used as triggersGravatar Clément Pit--Claudel2015-08-21
* | Add /printTooltips to trigger testsGravatar Clément Pit--Claudel2015-08-21
| * MergeGravatar Rustan Leino2015-08-20
| |\ | |/ |/|
| * Fixed compilation that involve enumeration over native-type newtype values.Gravatar Rustan Leino2015-08-20
* | Fix a typoGravatar Clément Pit--Claudel2015-08-20
* | Implement the SelectTrigger method, removing redundant triggers.Gravatar Clément Pit--Claudel2015-08-20
* | Merge.Gravatar Clément Pit--Claudel2015-08-20
|\|
| * Fixed bug in type unificationGravatar Rustan Leino2015-08-20
| * MergeGravatar Rustan Leino2015-08-20
| |\
* | | Add unit tests for trigger-related error messagesGravatar Clément Pit--Claudel2015-08-20
* | | Simplify error reporting in the trigger generator to get cleaner messagesGravatar Clément Pit--Claudel2015-08-20
* | | Add a test to show how trigger splitting balances the downsides of loop detec...Gravatar Clément Pit--Claudel2015-08-20
* | | Add a wishlist folder to the test suite, with things that we do not support (...Gravatar Clément Pit--Claudel2015-08-19
* | | Add a test to check that there are as many errors as failed preconditionsGravatar Clément Pit--Claudel2015-08-19
* | | Add tests for quantifier splitting and trigger generationGravatar Clément Pit--Claudel2015-08-19
| |/ |/|
| * Refactored and improved bounds discoveryGravatar Rustan Leino2015-08-19
* | runTests: Accept tests one by one, even if they are given as a .lst fileGravatar Clément Pit--Claudel2015-08-19
* | Use /tracePO instead of /trace in the serverGravatar Clément Pit--Claudel2015-08-19
* | Merge.Gravatar Clément Pit--Claudel2015-08-19
|\|
* | runTests: Include failed tests in mean completion timeGravatar Clément Pit--Claudel2015-08-19
* | runTests: Report mean completion time of passed tests, excluding outliersGravatar Clément Pit--Claudel2015-08-18
* | Exclude folders named 'sandbox' from lit testsGravatar Clément Pit--Claudel2015-08-18
* | Cleanup indentation of trigger warningsGravatar Clément Pit--Claudel2015-08-19
* | Draft out a more advanced version of trigger generationGravatar Clément Pit--Claudel2015-08-19
| * Changed dafny3/Filter.dfy to use higher-order functions instead of the previo...Gravatar leino2015-08-12
| * Change the induction heuristic for lemmas to also look in precondition for cl...Gravatar leino2015-08-12
* | runTests.py: Pretty-print stderr output to TRACE upon test failureGravatar Clément Pit--Claudel2015-08-12
|/
* MergeGravatar Rustan Leino2015-07-31
|\
| * MergeGravatar leino2015-07-31
| |\
| * \ MergeGravatar leino2015-07-31
| |\ \
* | | | Bug fix: check that assign-such-that constraint is of type booleanGravatar Rustan Leino2015-07-31
| |/ / |/| |
| * | Allow forall statements in refinementsGravatar leino2015-07-31
| | * Add tests for the serverGravatar Clément Pit--Claudel2015-07-31
| |/ |/|
* | Add quotes in snapshot tests.Gravatar Clément Pit--Claudel2015-07-30
* | Fixed crash in resolution where, after reporting an error, the cases #type an...Gravatar Rustan Leino2015-07-29
* | MergeGravatar Clément Pit--Claudel2015-07-28
|\ \
* | | Save failing tests to failing.lst, making it easy to re-run themGravatar Clément Pit--Claudel2015-07-28
| * | Renamed "ghost method" to "lemma" whenever appropriate (which is most of the ...Gravatar Rustan Leino2015-07-28
| |/
* | Clarify the inlining warning.Gravatar Clément Pit--Claudel2015-07-27
| * Renamed "ghost method" to "lemma" in a couple of test filesGravatar Rustan Leino2015-07-24
|/
* Bump up the time limit in runTests.py and save a bit of space in outputGravatar Clément Pit--Claudel2015-07-23
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-01 16:20:13 +0000