summaryrefslogtreecommitdiff
path: root/Test
Commit message (Expand)AuthorAge
* Implement workarounds for some tests that fail with /autoTriggers.Gravatar Clément Pit--Claudel2015-08-28
* Suppress many warnings in the test suite.Gravatar Clément Pit--Claudel2015-08-28
* Clarify a commentGravatar Clément Pit--Claudel2015-08-28
* Implement {:nowarn}, clarify some messages, and add a few testsGravatar Clément Pit--Claudel2015-08-28
* Add a small test from the IronClad notebookGravatar Clément Pit--Claudel2015-08-27
* Further relax the loop detection conditionsGravatar Clément Pit--Claudel2015-08-27
* Small fix: there is no loop in (forall x :: Q(x) && Q(0))Gravatar Clément Pit--Claudel2015-08-27
* Improve the redundancy detection algorithm used while constructing sets of termsGravatar Clément Pit--Claudel2015-08-26
* Add change missing from bd47e3cdb79cGravatar Clément Pit--Claudel2015-08-23
* s/loops with/may loop with/Gravatar Clément Pit--Claudel2015-08-23
* Added /autoTriggers to two tests where it only makes a cosmetic differenceGravatar Clément Pit--Claudel2015-08-23
* Replace b || !b by true in Snapshots5.v1.dfyGravatar Clément Pit--Claudel2015-08-23
* Make quantifier splitting a two step processGravatar Clément Pit--Claudel2015-08-23
* Improve error reporting for split quantifiersGravatar Clément Pit--Claudel2015-08-23
* Allow MultiSelectExpr as quantifier headsGravatar Clément Pit--Claudel2015-08-23
* Fix: multi-dimensional OOB errors were sometimes reported on incorrect locati...Gravatar Clément Pit--Claudel2015-08-23
* Add one more wish: it would be nice to be able to prove exists b: bool :: bGravatar Clément Pit--Claudel2015-08-22
* Grant "wishlist/useless-casts-in-decreases-clauses.dfy"Gravatar Clément Pit--Claudel2015-08-22
* Add more wishes to the wishlistGravatar Clément Pit--Claudel2015-08-22
* Look at the full quantifier to find loops, not just the term.Gravatar Clément Pit--Claudel2015-08-22
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-24 21:15:08 +0000