index
:
debian-dafny
master
Debian packaging for Dafny
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
Source
/
Dafny
Commit message (
Expand
)
Author
Age
*
New version number 1.9.7.30401, for binary release on Codeplex and Rise4fun.
leino
2016-04-01
*
Allow modifies clauses for a "Main" method annotated with {:main} attribute.
qunyanm
2016-03-31
*
Fix issue 143. The list that stores the function fuel constants was declared as
qunyanm
2016-03-31
*
Fix issue 75. Adjust the fuel for existentials to use more fuel in an assume
qunyanm
2016-03-31
*
Allow users to annontate a method as main with {:main} attribute. It’s an e...
qunyanm
2016-03-28
*
Make /autoTriggers:1 to be default. Add /autoTriggers:0 to tests that requires
qunyanm
2016-03-28
*
Update module export error messages. Also for "import Y" if there is at least
qunyanm
2016-03-21
*
Fix issue 93. Add per-function fuel setting that can be adjusted locally based
qunyanm
2016-03-18
*
Merge
Rustan Leino
2016-03-01
|
\
*
|
Revised the $Is and $IsAlloc axioms for arrow terms. It is now possible to
Rustan Leino
2016-03-01
*
|
Added a return-value contract
Rustan Leino
2016-02-29
|
*
Fix issue 139. Allow bound variables in nested case patterns to shadow variables
qunyanm
2016-02-26
|
/
*
Merge
Rustan Leino
2016-02-26
|
\
*
|
Changes to CanCall assumptions:
Rustan Leino
2016-02-26
|
*
Fix issue 138. Allow parenthese with the nullary constructor in
qunyanm
2016-02-26
|
*
Fix issue 140. Move the initializion of _this before the TAIL_CALL_START label.
qunyanm
2016-02-26
|
*
Fix issue 136. Less aggressive Lit wrap for assert/assume.
qunyanm
2016-02-26
|
/
*
Fix issue 132. The formal argument can't be assume to be allocated when a
qunyanm
2016-02-12
*
Fix issue 134. Wrong variable was used in the loop.
qunyanm
2016-02-11
*
Fix issue 133. The return type for some compare operators was wrongly typed
qunyanm
2016-02-11
*
Add /view:<view1, view2> option to filter module exports to be printed.
qunyanm
2016-02-11
*
Fix issue 131. Instead of crashing, report an error when an undefined member of
qunyanm
2016-02-09
*
Fix issue 120. Need to wrap operations that are "lit lifted" and turned into
qunyanm
2016-02-08
*
Fix issue 124. Consider math operators that later turned into function calls
qunyanm
2016-02-08
*
Fix issue 125. Add the missing case 2 and 3 with refinement and opened imports.
qunyanm
2016-02-05
*
Fix issue 128. Change the translation of CanCallAssumption for let-such-that
qunyanm
2016-02-04
*
Fix issue 129. When looking for a constructor for which Dafny knows how to
qunyanm
2016-02-02
*
Mark old "import A as B" syntax as deprecated. The new syntax is "import A : B"
qunyanm
2016-02-02
*
Implement module export so we can export a subset of items defined in the
qunyanm
2016-01-29
*
Revert Makefile to its prior settings
Richard L. Ford
2016-01-29
*
Fix build and test failures, cleanup grammar.
Richard L. Ford
2016-01-27
*
Implement 'extern' declaration modifier.
Richard L. Ford
2016-01-27
*
Fix issue 121. Don't split QuantifierExpr that are empty.
qunyanm
2016-01-25
*
Fix issue 122. Only generate autoTriggers for QuantifierExpr that are not
qunyanm
2016-01-25
*
Mark temps that are generated in the resolver as auto-generated identifiers so
qunyanm
2016-01-20
*
Fix issue 117. Generate an error when the "opened" of an import doesn't match
qunyanm
2016-01-08
*
Fix issue 118. When iteratively computing bounds, treat RefBoundedPool typed
qunyanm
2016-01-07
*
Removed Contract.Requires from method overrides (preconditions of overrides a...
Rustan Leino
2016-01-06
*
Fix issue 116. Add the missing @ for the generated c# code.
qunyanm
2016-01-05
*
Fix issue 114. Do not export private terms for ComprehensionExpr in trigger
qunyanm
2015-12-08
*
Fix printing for ForallStmt. Previously we traverse the resolved forall
qunyanm
2015-12-04
*
Fix issue 113. Make sure the tempVar name used in ToString() method doesn't
qunyanm
2015-12-03
*
Fix issue 110. Set useImport to true when trying to registerTopLevelDecls
qunyanm
2015-12-02
*
Fix issue 111. Create a new BoundVar for each CasePattern of MatchCaseExpr when
qunyanm
2015-11-30
*
Made an adjustment in the printing of resolved forall expressions (previous c...
leino
2015-11-28
*
Merge
leino
2015-11-27
|
\
*
|
Make cached results dependent on if a function is ghost or not
leino
2015-11-27
*
|
autocontracts: Don't add modifies clause to ghost methods
leino
2015-11-27
|
*
Fix issue 103. Emit the quantifiers for ForallStmt before AutoTrigger so that
qunyanm
2015-11-25
|
/
*
Add code that uses Z3's optimization features (currently disabled by default).
wuestholz
2015-11-19
[next]