index
:
debian-dafny
master
Debian packaging for Dafny
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
Test
Commit message (
Expand
)
Author
Age
*
Add a 'tutorial' folder to the distribution, with an initial example.
Clément Pit--Claudel
2015-08-22
*
Merge
Clément Pit--Claudel
2015-08-21
|
\
*
|
Make `old` a special case for trigger generation.
Clément Pit--Claudel
2015-08-21
*
|
Rephrase the message about triggers being rejected because they are too strong
Clément Pit--Claudel
2015-08-21
*
|
Add a few things to the wishlist
Clément Pit--Claudel
2015-08-21
*
|
Adjust WF checks to use unsplit quantifiers.
Clément Pit--Claudel
2015-08-21
|
*
Make use of new syntax in a test file
Rustan Leino
2015-08-21
*
|
Interleave stderr output with test results; this allows one to print stuff
Clément Pit--Claudel
2015-08-21
*
|
Ignore flycheck_* files in runTests
Clément Pit--Claudel
2015-08-21
*
|
Add tests for display expressions used as triggers
Clément Pit--Claudel
2015-08-21
*
|
Add /printTooltips to trigger tests
Clément Pit--Claudel
2015-08-21
|
*
Merge
Rustan Leino
2015-08-20
|
|
\
|
|
/
|
/
|
|
*
Fixed compilation that involve enumeration over native-type newtype values.
Rustan Leino
2015-08-20
*
|
Fix a typo
Clément Pit--Claudel
2015-08-20
*
|
Implement the SelectTrigger method, removing redundant triggers.
Clément Pit--Claudel
2015-08-20
*
|
Merge.
Clément Pit--Claudel
2015-08-20
|
\
|
|
*
Fixed bug in type unification
Rustan Leino
2015-08-20
|
*
Merge
Rustan Leino
2015-08-20
|
|
\
*
|
|
Add unit tests for trigger-related error messages
Clément Pit--Claudel
2015-08-20
*
|
|
Simplify error reporting in the trigger generator to get cleaner messages
Clément Pit--Claudel
2015-08-20
*
|
|
Add a test to show how trigger splitting balances the downsides of loop detec...
Clément Pit--Claudel
2015-08-20
*
|
|
Add a wishlist folder to the test suite, with things that we do not support (...
Clément Pit--Claudel
2015-08-19
*
|
|
Add a test to check that there are as many errors as failed preconditions
Clément Pit--Claudel
2015-08-19
*
|
|
Add tests for quantifier splitting and trigger generation
Clément Pit--Claudel
2015-08-19
|
|
/
|
/
|
|
*
Refactored and improved bounds discovery
Rustan Leino
2015-08-19
*
|
runTests: Accept tests one by one, even if they are given as a .lst file
Clément Pit--Claudel
2015-08-19
*
|
Use /tracePO instead of /trace in the server
Clément Pit--Claudel
2015-08-19
*
|
Merge.
Clément Pit--Claudel
2015-08-19
|
\
|
*
|
runTests: Include failed tests in mean completion time
Clément Pit--Claudel
2015-08-19
*
|
runTests: Report mean completion time of passed tests, excluding outliers
Clément Pit--Claudel
2015-08-18
*
|
Exclude folders named 'sandbox' from lit tests
Clément Pit--Claudel
2015-08-18
*
|
Cleanup indentation of trigger warnings
Clément Pit--Claudel
2015-08-19
*
|
Draft out a more advanced version of trigger generation
Clément Pit--Claudel
2015-08-19
|
*
Changed dafny3/Filter.dfy to use higher-order functions instead of the previo...
leino
2015-08-12
|
*
Change the induction heuristic for lemmas to also look in precondition for cl...
leino
2015-08-12
*
|
runTests.py: Pretty-print stderr output to TRACE upon test failure
Clément Pit--Claudel
2015-08-12
|
/
*
Merge
Rustan Leino
2015-07-31
|
\
|
*
Merge
leino
2015-07-31
|
|
\
|
*
\
Merge
leino
2015-07-31
|
|
\
\
*
|
|
|
Bug fix: check that assign-such-that constraint is of type boolean
Rustan Leino
2015-07-31
|
|
/
/
|
/
|
|
|
*
|
Allow forall statements in refinements
leino
2015-07-31
|
|
*
Add tests for the server
Clément Pit--Claudel
2015-07-31
|
|
/
|
/
|
*
|
Add quotes in snapshot tests.
Clément Pit--Claudel
2015-07-30
*
|
Fixed crash in resolution where, after reporting an error, the cases #type an...
Rustan Leino
2015-07-29
*
|
Merge
Clément Pit--Claudel
2015-07-28
|
\
\
*
|
|
Save failing tests to failing.lst, making it easy to re-run them
Clément Pit--Claudel
2015-07-28
|
*
|
Renamed "ghost method" to "lemma" whenever appropriate (which is most of the ...
Rustan Leino
2015-07-28
|
|
/
*
|
Clarify the inlining warning.
Clément Pit--Claudel
2015-07-27
|
*
Renamed "ghost method" to "lemma" in a couple of test files
Rustan Leino
2015-07-24
|
/
*
Bump up the time limit in runTests.py and save a bit of space in output
Clément Pit--Claudel
2015-07-23
[next]