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
...
*
Merge
leino
2015-09-29
|
\
|
*
Fix two test cases that failed if the path to "DafnySever.exe" contained spaces.
wuestholz
2015-09-30
*
|
Removed specContextOnly parameter from ResolveStatement.
leino
2015-09-28
*
|
Removed more traces of the previous resolution checks that happened during pa...
leino
2015-09-28
*
|
Additional tests
leino
2015-09-28
*
|
Whitespace changes in test file
leino
2015-09-28
*
|
Improvements in proofs
leino
2015-09-28
*
|
Changed computation of ghosts until pass 2 of resolution.
leino
2015-09-28
*
|
A test file with an example of least vs greatest fixpoints.
leino
2015-09-22
*
|
Added back in various ghost tests
leino
2015-09-20
*
|
Changes that only affect line numbers in test case
leino
2015-09-20
*
|
Removed tabs from test file
leino
2015-09-20
*
|
Adjusted (corrected, I think) test output
leino
2015-09-20
*
|
Preliminary refactoring of ghost-statement computations to after type checking
leino
2015-09-20
|
/
*
Proof that Ackermann can be curried and that it is monotonic in both arguments.
Rustan Leino
2015-09-08
*
Merge
Clément Pit--Claudel
2015-09-02
|
\
*
|
Fix some tests by locally disabling auto triggers
Clément Pit--Claudel
2015-08-28
*
|
Add a small test from a discussion with Bryan
Clément Pit--Claudel
2015-08-28
*
|
Implement workarounds for some tests that fail with /autoTriggers.
Clément Pit--Claudel
2015-08-28
*
|
Suppress many warnings in the test suite.
Clément Pit--Claudel
2015-08-28
*
|
Clarify a comment
Clément Pit--Claudel
2015-08-28
*
|
Implement {:nowarn}, clarify some messages, and add a few tests
Clément Pit--Claudel
2015-08-28
|
*
Merge
Rustan Leino
2015-08-28
|
|
\
|
|
/
|
/
|
|
*
Added tests for Boogie's new /verifySnapshots:3, which will be used by the Da...
Rustan Leino
2015-08-28
|
*
Fixed spelling mistake in test file
Rustan Leino
2015-08-28
*
|
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
[prev]
[next]