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-06-25
|
\
*
|
Tried to reduce frame-axiom instantiations by saying the earlier heap must be...
leino
2015-06-25
*
|
Removed unneeded :heapQuantifier from test case (rendinging this attribute cu...
leino
2015-06-25
|
*
Fix various bugs in nested match patterns listed in issue #83
qunyanm
2015-06-19
|
/
*
Changed logical order of requires and reads clauses on functions. Reads clauses
Rustan Leino
2015-06-15
*
Do postponsed reads checking also for the body of functions -- see Test/dafny...
Rustan Leino
2015-06-15
*
Some more reads tests
Rustan Leino
2015-06-15
*
More reads tests
Rustan Leino
2015-06-15
*
Postpone reads checks of function preconditions until after the entire precon...
leino
2015-06-15
*
More tests of reads-clause checking
Rustan Leino
2015-06-15
*
Merge
leino
2015-06-12
|
\
*
|
Added /vcs... cop-out to test case to make it go through
leino
2015-06-12
|
*
Fix a bug spotted by Chris in my BigInteger patch; thanks!
Clément Pit--Claudel
2015-06-12
*
|
Merge
leino
2015-06-12
|
\
|
*
|
Combined some common routines into CheckWellformedAndAssume, which also allow...
leino
2015-06-12
|
*
Merge
Clément Pit--Claudel
2015-06-12
|
|
\
|
*
|
Small fix in runTests.py
Clément Pit--Claudel
2015-06-12
|
|
*
merge
Michael Lowell Roberts
2015-06-12
|
|
|
\
|
|
|
/
|
|
/
|
|
|
*
added -optimize option to compiler.
Michael Lowell Roberts
2015-06-12
|
|
/
|
/
|
|
*
Add missing default parameter in runTests.py
Clément Pit--Claudel
2015-06-11
|
*
A few more improvements to runTests.py
Clément Pit--Claudel
2015-06-11
|
*
Small improvements to runTests.py
Clément Pit--Claudel
2015-06-10
|
/
*
Fix the UseBaseNameForFileName flag; it shouldn't set the return code to zero.
Clément Pit--Claudel
2015-06-07
*
Fix lit headers implicitly relying on bash-style constructs
Clément Pit--Claudel
2015-06-08
*
Add the beginning of a new testing infrastructure
Clément Pit--Claudel
2015-06-08
*
Generate #requires function for OpaqueFunction.
qunyanm
2015-06-04
*
Merge
leino
2015-05-29
|
\
|
*
Add an infinite set collection type.
qunyanm
2015-05-29
*
|
Improvements in traits test case
leino
2015-05-29
*
|
Improvements to Nipkow and Klein test cases: Changed imap to map, removed ne...
leino
2015-05-29
|
/
*
Fix issue #81. Pass a call's TypeArgumentSubstitution to CheckCallTermination.
qunyanm
2015-05-18
*
Updated test output after change in Boogie.
wuestholz
2015-05-17
*
Fix issue #79. Allow tuple pattern matching with parenthesis only.
qunyanm
2015-05-15
*
Allow MatchExpr and MatchStmt to have nested patterns. Such as
qunyanm
2015-05-14
*
Don't include arrow types among ordered types.
leino
2015-05-11
*
Added to the test suite a Dafny encoding of Chapter 7 from the Nipkow and Kle...
leino
2015-05-10
*
Additional test case for inductive predicates
leino
2015-05-07
*
Added "inductive lemma" methods
leino
2015-05-07
*
Added inductive predicates
leino
2015-05-06
*
Improved generation of .reads axioms (correcting an incorrect answer and corr...
leino
2015-05-01
*
Answer file
leino
2015-05-01
*
Improved encoding of a property of reads clauses to make things more easily p...
leino
2015-05-01
*
Added to the test suite a Dafny encoding of Chapter 3 from the Nipkow and Kle...
leino
2015-04-29
*
Added a test where Dafny verifies something that the Juggernaut tool can infer
leino
2015-04-28
*
Merge
leino
2015-04-28
|
\
*
|
Changes to the VerifyThis2015 test programs
leino
2015-04-28
|
*
Fix issue #72. Add the constructor questionmark to a function's axiom if the
qunyanm
2015-04-24
*
|
Fixed bug in tuples
leino
2015-04-24
|
*
Fix issue #70. Check the ctors for equality before marking them as duplicates.
qunyanm
2015-04-21
|
*
Fix issue #73. Pass in expr.tok when creating Bpl.Expr for InMap and NotInMap.
qunyanm
2015-04-20
[next]