index
:
debian-dafny
master
Debian packaging for Dafny
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
Test
/
dafny2
Commit message (
Expand
)
Author
Age
*
In method and iterator specifications, inline top-level predicates (except
leino
2015-10-24
*
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
*
Renamed "ghost method" to "lemma" whenever appropriate (which is most of the ...
Rustan Leino
2015-07-28
*
Fix: Unify column numbers in Dafny's errors
Clément Pit--Claudel
2015-07-23
*
Minor fixes in .expect files
Clément Pit--Claudel
2015-07-16
*
Fix multiple tests that relied on z3 triggering on $Box
Clément Pit--Claudel
2015-07-13
*
This changeset changes the default visibility of a function/predicate body ou...
leino
2015-03-09
*
Stop pretty-print from emitting deprecated semi-colons.
qunyanm
2015-03-05
*
Language change: All functions and methods declared lexically outside any cla...
leino
2014-12-12
*
Snapshot, to be continued
leino
2014-12-02
*
Refactored SnapshotableTrees a bit and made it verify in a reasonable amount ...
leino
2014-11-04
*
Added VC Splitting switch to dafny2/SnapshotableTrees.dfy to try to avoid som...
leino
2014-10-21
*
Enabled 'SnapshotableTrees.dfy' in the test suite.
wuestholz
2014-09-24
*
Made 'SnapshotableTrees.dfy' verify again.
wuestholz
2014-09-24
*
Disallow parentheses-less declarations of predicates and co-predicates, along...
leino
2014-08-27
*
Change behavior of 'decreases *', which can be applied to loops and methods. ...
Rustan Leino
2014-08-19
*
Add higher-order-functions and some other goodies
Dan Rosén
2014-08-11
*
Improved AnalyzeList encoding in a way that performs way better.
Rustan Leino
2014-07-09
*
Merge
Dan Rosén
2014-07-07
|
\
*
|
New logical encoding of types with Is and IsAlloc
Dan Rosén
2014-07-07
|
*
Removed the old test infrastructure.
wuestholz
2014-07-01
*
|
Made the snapshotable trees test "unsupported" instead of "unresolved".
wuestholz
2014-06-05
|
*
Made the snapshotable trees test "unsupported" instead of "unresolved".
wuestholz
2014-06-05
|
/
*
Set up the same test infrastructure as in Boogie.
wuestholz
2014-05-29
*
Renamed a constructor in a test file
Rustan Leino
2014-01-03
*
Add support for the /verifySeparately flag in Boogie and change most tests to...
wuestholz
2013-12-18
*
Update an 'Answer' file.
wuestholz
2013-12-10
*
Change a test program to verify faster (by a factor of 10-25).
wuestholz
2013-12-10
*
Moved resolution of BinaryExpr.ResolveOp until the CheckTypeInference phase, ...
Rustan Leino
2013-04-01
*
Renamed "parallel" statement to "forall" statement, and made the parentheses ...
Rustan Leino
2013-03-06
*
Added tests: parallel calc, better well-formedness checks, calc expression.
Nadia Polikarpova
2013-02-15
*
Updated a test in dafny2 with the new calc syntax.
Nadia Polikarpova
2013-02-14
*
Merge
Nadia Polikarpova
2013-02-14
|
\
|
*
Report error if type of a quantified variable cannot be inferred
Rustan Leino
2013-02-11
*
|
Changed calc syntax (custom operators are now written before the hint)
Nadia Polikarpova
2013-02-08
|
/
*
renamed "abstract module" to "module facade"
Rustan Leino
2012-10-22
*
added two "calc" proofs (by Nadia) of the MajorityVote example
Unknown
2012-10-19
*
improved and fixed compilation and resolution of assign-such-that statements
Rustan Leino
2012-10-05
*
Fixed some goof-ups in the test script edits
Rustan Leino
2012-10-04
*
Added Test/dafny3 and another test file for iterators (hey, you can even run ...
Rustan Leino
2012-10-04
*
Use expression splitting for checking calculation steps
Nadia Polikarpova
2012-09-23
*
Allow multiple calc/block statements in a hint. Removed the empty calc test f...
Nadia Polikarpova
2012-09-19
*
Allow empty calc statements
Nadia Polikarpova
2012-09-19
*
Dafny: some test cases for "calc" (very cool!)
Unknown
2012-09-17
*
Dafny: added MonotonicHeapstate refinement example
Unknown
2012-08-09
*
Dafny: updated test suite to new syntax
Jason Koenig
2012-07-30
*
Dafny: restored soundness for refinement by disallowing certain updates and m...
Jason Koenig
2012-07-11
*
Dafny: reinstated autocontracts
Jason Koenig
2012-07-02
*
Dafny: fixed up test suite (temporarily removed autocontract tests)
Jason Koenig
2012-06-28
[next]