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
*
[IronDafny] implemented workaround for "import opened" bug(s).
Michael Lowell Roberts
2015-07-13
*
Auto-merged heads.
Michael Lowell Roberts
2015-07-08
|
\
*
|
added unit tests for exclusive refinement.
Michael Lowell Roberts
2015-07-08
|
*
Fixed crashes in overrides checking of function decreases clauses, and improv...
Rustan Leino
2015-07-07
|
*
Report warnings only once. (This is the last step in fixing Issue #86.)
Rustan Leino
2015-07-06
|
*
Added command-line option /warnShadowing, which emits warnings if variables s...
Rustan Leino
2015-07-02
|
*
Type parameters in method/function signatures are no longer auto-declared. A...
Rustan Leino
2015-07-02
|
/
*
Added another lemma to a test file
Rustan Leino
2015-07-02
*
Merge
leino
2015-07-01
|
\
*
|
Fixed bug in BplImp!
leino
2015-07-01
|
*
Add the ability to specify how much "fuel" a function should have,
Bryan Parno
2015-07-01
*
|
Fixed bugs in encoding of preconditions of function values, Issue #84.
leino
2015-06-30
*
|
Additional test case for instance functions
leino
2015-06-30
|
/
*
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
[next]