index
:
debian-dafny
master
Debian packaging for Dafny
summary
refs
log
tree
commit
diff
log msg
author
committer
range
Commit message (
Expand
)
Author
Age
*
Updated version to 1.9.2.11107 (which is going out on rise4fun)
Rustan Leino
2014-11-07
*
Resolved several more LL(1) warnings in the grammar
Rustan Leino
2014-11-06
*
Merge
leino
2014-11-06
|
\
*
|
Started fixing a number of LL(1) warnings
leino
2014-11-06
|
*
Now the parser parses "Type" rather than "IToken" for a trait
Reza Ahmadi
2014-11-05
|
*
Extracted a separate class to generate fresh variable names.
wuestholz
2014-11-06
|
*
Updated test.
chmaria
2014-11-06
|
*
Added computation of free variables in dirty while statements.
chmaria
2014-11-06
|
/
*
Merge
Rustan Leino
2014-11-05
|
\
*
|
Temporarily disabled one of the methods in NumberRepresentations.dfy -- this ...
leino
2014-11-05
*
|
Merge
leino
2014-11-05
|
\
\
|
*
|
Refactored the generation of unique IDs for temporary variable names.
wuestholz
2014-11-05
|
*
|
Did some refactoring.
wuestholz
2014-11-05
*
|
|
Merge
leino
2014-11-04
|
\
|
|
*
|
|
Merge
leino
2014-11-04
|
\
\
\
*
|
|
|
Refactored SnapshotableTrees a bit and made it verify in a reasonable amount ...
leino
2014-11-04
|
|
*
|
Made dirty statements ghost.
chmaria
2014-11-04
|
|
|
*
Merge
Rustan Leino
2014-11-03
|
|
|
|
\
|
|
|
|
/
|
|
|
/
|
|
|
|
*
Updated a test case for new syntax and convensions
Rustan Leino
2014-11-03
|
|
*
|
Fixed test output after refactoring in Boogie.
wuestholz
2014-11-03
|
|
*
|
Fixed test output after refactoring in Boogie.
wuestholz
2014-11-02
|
*
|
|
Merge
leino
2014-11-01
|
|
\
|
|
|
*
|
|
Various DafnyPrelude.bpl cleanup.
leino
2014-11-01
|
|
*
|
Minor fix in test dafny2/SnapshotableTrees.dfy.
chmaria
2014-11-01
|
|
*
|
Added initial support for dirty while statements.
chmaria
2014-11-01
|
*
|
|
Improved power of axioms Seq#FromArray
leino
2014-10-31
|
|
/
/
|
*
|
Allow assignment LHSs in a forall statement to be the same, so long as the th...
leino
2014-10-30
|
*
|
Resolve attributes of a forall statement only after bound variables have been...
leino
2014-10-29
|
|
/
|
*
Fix bug in translation of 'new' for arrays
Rustan Leino
2014-10-29
|
*
Merge
leino
2014-10-28
|
|
\
|
*
|
Fixed type-inference bug that could create cycles in proxy type graph
leino
2014-10-28
|
*
|
Disallow automatic completion of type arguments to the LHS of datatype declar...
leino
2014-10-28
|
|
*
Create large stack in DafnyDriver.cs, before calling main,
Bryan Parno
2014-10-28
|
|
/
|
*
Fixed a bug in the Substituter for datatype update expressions.
leino
2014-10-28
|
*
Add a DafnyCC option that disables some of Dafny's cleverness to better match...
Bryan Parno
2014-10-27
|
*
Fix datatype updates so chained updates don't explode performance
Bryan Parno
2014-10-27
|
*
Make autoreqs of free requires not free
Bryan Parno
2014-10-27
|
*
Allow autoReq in methods to generate auto-requirements on requires
Bryan Parno
2014-10-27
|
*
Fixed range bug that was causing extension to sometimes crash
Bryan Parno
2014-10-27
|
*
Don't process opaque functions more than once when generating auto-reqs
Bryan Parno
2014-10-27
|
*
Fix fixup to opaque-function revealer to deal with zero-argument lemmas
Bryan Parno
2014-10-27
|
*
Fix autoreq handling of quantifiers
Bryan Parno
2014-10-27
|
*
Ensure that no file is processed twice, even if one command-line file is incl...
Bryan Parno
2014-10-27
|
*
Added an attribute :timeLimitMultiplier for setting relative time outs.
Bryan Parno
2014-10-27
|
*
Push the translation of user-supplied triggers deeper
Bryan Parno
2014-10-27
|
*
Add support for counting spec/impl/proof lines by supressing, e.g., ghost sta...
Bryan Parno
2014-10-27
|
*
Add an option to allow automatically generated requirements to be printed
Bryan Parno
2014-10-27
|
*
Even with noCheating enabled, don't check included files or methods marked wi...
Bryan Parno
2014-10-27
|
*
Allow non-ghost axioms in order to model trusted external calls,
Bryan Parno
2014-10-27
|
*
Merge
leino
2014-10-25
|
|
\
[next]