index
:
debian-dafny
master
Debian packaging for Dafny
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
Source
/
Dafny
/
Translator.cs
Commit message (
Expand
)
Author
Age
...
*
|
Clean up new trigger declarations in Translator.cs
Clément Pit--Claudel
2015-07-17
*
|
Strip literals from triggers
Clément Pit--Claudel
2015-07-16
*
|
Fix broken interaction between triggers and inlining of function calls
Clément Pit--Claudel
2015-07-14
*
|
Start adding missing triggers to the translator
Clément Pit--Claudel
2015-07-13
*
|
Make attributes enumerable.
Clément Pit--Claudel
2015-07-13
|
*
Fixed crashes in overrides checking of function decreases clauses, and improv...
Rustan Leino
2015-07-07
*
|
Small refactoring of Printer.cs
Clément Pit--Claudel
2015-07-06
|
*
multiple changes...
Michael Lowell Roberts
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
|
/
*
Tried to reduce frame-axiom instantiations by saying the earlier heap must be...
leino
2015-06-25
*
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
*
Postpone reads checks of function preconditions until after the entire precon...
leino
2015-06-15
*
Little edits in new CheckWellformedAndAssume code
leino
2015-06-12
*
Combined some common routines into CheckWellformedAndAssume, which also allow...
leino
2015-06-12
*
Generate #requires function for OpaqueFunction.
qunyanm
2015-06-04
*
Merge
leino
2015-05-29
|
\
|
*
Add an infinite set collection type.
qunyanm
2015-05-29
*
|
Merge
leino
2015-05-29
|
\
|
*
|
Bug fix in type-antecedent for traits in allocation axioms
leino
2015-05-29
|
*
Merge
Rustan Leino
2015-05-29
|
|
\
|
*
|
Changes to ComputeFreeVariables--bug fix as well as beautification
Rustan Leino
2015-05-29
|
|
*
Fix build break. Part of the change was not checked in last check-in somehow.
qunyanm
2015-05-19
|
|
*
Fix issue #81. Pass a call's TypeArgumentSubstitution to CheckCallTermination.
qunyanm
2015-05-18
|
|
/
|
/
|
*
|
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
*
|
Improved encoding of a property of reads clauses to make things more easily p...
leino
2015-05-01
|
/
*
Fix issue #72. Add the constructor questionmark to a function's axiom if the
qunyanm
2015-04-24
*
Fix issue #73. Pass in expr.tok when creating Bpl.Expr for InMap and NotInMap.
qunyanm
2015-04-20
*
Include axioms about $Is and $IsAlloc for traits
leino
2015-04-07
*
Fixed some bugs in override axioms (but still missing support for classes wit...
leino
2015-04-05
*
Merge
leino
2015-04-03
|
\
*
|
Added test cases and fixes for overrides termination checks
leino
2015-04-03
|
*
Eliminate redundant checks of newtype and opaque function well-formedness fro...
chrishaw
2015-04-02
|
/
*
Fix issue #56. Convert parametered opaque type parameters into an IdentifierExpr
qunyanm
2015-03-27
*
Fix issue #58. In TrSplitExpr(), add allocatedness for arguments to the inlined
qunyanm
2015-03-26
*
Fix issue #63. ForceSubstitutionOfQuantifiedVars for SetComprehesion.
qunyanm
2015-03-17
*
Merge
leino
2015-03-13
|
\
*
|
Allow let-such-that expression to be compiled, provided that they provably ha...
leino
2015-03-13
|
*
Allow trigger annotations in more statements and expressions
chrishaw
2015-03-11
|
*
Merge
qunyanm
2015-03-11
|
|
\
|
|
/
|
/
|
|
*
Fix issue #54 and #57. Resolve a formal's type before creating a substitute.
qunyanm
2015-03-11
*
|
Removed some old and unused functions
leino
2015-03-09
*
|
This changeset changes the default visibility of a function/predicate body ou...
leino
2015-03-09
|
/
*
Add imap display/update expressions
chrishaw
2015-02-27
*
Add imap type, which is like map but may have have infinite size
chrishaw
2015-02-26
[prev]
[next]