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 small test from the IronClad notebook
Clément Pit--Claudel
2015-08-27
*
|
Further relax the loop detection conditions
Clément Pit--Claudel
2015-08-27
*
|
Small fix: there is no loop in (forall x :: Q(x) && Q(0))
Clément Pit--Claudel
2015-08-27
*
|
Improve the redundancy detection algorithm used while constructing sets of terms
Clément Pit--Claudel
2015-08-26
|
/
*
Add change missing from bd47e3cdb79c
Clément Pit--Claudel
2015-08-23
*
s/loops with/may loop with/
Clément Pit--Claudel
2015-08-23
*
Added /autoTriggers to two tests where it only makes a cosmetic difference
Clément Pit--Claudel
2015-08-23
*
Replace b || !b by true in Snapshots5.v1.dfy
Clément Pit--Claudel
2015-08-23
*
Make quantifier splitting a two step process
Clément Pit--Claudel
2015-08-23
*
Improve error reporting for split quantifiers
Clément Pit--Claudel
2015-08-23
*
Allow MultiSelectExpr as quantifier heads
Clément Pit--Claudel
2015-08-23
*
Fix: multi-dimensional OOB errors were sometimes reported on incorrect locati...
Clément Pit--Claudel
2015-08-23
*
Add one more wish: it would be nice to be able to prove exists b: bool :: b
Clément Pit--Claudel
2015-08-22
*
Grant "wishlist/useless-casts-in-decreases-clauses.dfy"
Clément Pit--Claudel
2015-08-22
*
Add more wishes to the wishlist
Clément Pit--Claudel
2015-08-22
*
Look at the full quantifier to find loops, not just the term.
Clément Pit--Claudel
2015-08-22
*
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
[prev]
[next]