index
:
debian-boogie
dfsg_free
master
Debian packaging for Boogie
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
Source
Commit message (
Expand
)
Author
Age
*
Unified the .frame files so that both Boogie and Dafny use exactly the same o...
mikebarnett
2010-06-25
*
Dafny:
rustanleino
2010-06-24
*
Dafny:
rustanleino
2010-06-24
*
Updated the frame files to work with the latest Coco/R. This entails *not* ha...
mikebarnett
2010-06-22
*
Boogie:
rustanleino
2010-06-22
*
Dafny:
rustanleino
2010-06-19
*
Dafny:
rustanleino
2010-06-18
*
Derive IsabelleContext from DeclFreeProverContext
stobies
2010-06-16
*
Improved error messages for doomed program points.
schaef
2010-06-15
*
Dafny: Added two additional heuristics for guessing missing loop decreases c...
rustanleino
2010-06-11
*
fixed a compiler warning about initialization of a non-null field inside the ...
qadeer
2010-06-10
*
Dafny: Another bug fix in SplitExpr, having to do with generic results of fu...
rustanleino
2010-06-09
*
Dafny: Fix type bug in SplitExpr translation.
rustanleino
2010-06-08
*
Dafny: For functions with an empty decreases clause that use the reads clause...
rustanleino
2010-06-08
*
Boogie:
rustanleino
2010-06-08
*
Dafny:
rustanleino
2010-06-05
*
Updated to find the latest version of Z3 (2.7) and made the algorithm slightl...
wuestholz
2010-05-28
*
changed the behavior of /loopUnroll:n so that the parameter n is applied per ...
qadeer
2010-05-26
*
Dafny: Allow < and > for comparisons of datatype values (which then compares ...
rustanleino
2010-05-21
*
Dafny:
rustanleino
2010-05-21
*
Dafny: Fixed crash in parser (that occurred when the Dafny input had a parti...
rustanleino
2010-05-18
*
Boogie:
rustanleino
2010-05-15
*
Dafny:
rustanleino
2010-05-13
*
BCT: Added prelude. Started test1 as a test of verification.
rustanleino
2010-05-12
*
Dafny:
rustanleino
2010-05-08
*
Dafny:
rustanleino
2010-05-06
*
Dafny:
rustanleino
2010-05-06
*
Added another option for lazy inlining based on macro expansion. This option...
qadeer
2010-05-03
*
Updated to find the latest version of Z3 (2.6).
wuestholz
2010-05-02
*
1. Fixed lazy inlining implementation so that inlined procedures use live var...
qadeer
2010-04-30
*
1. couple of bug fixes in interprocedural error trace generation
qadeer
2010-04-23
*
Added callee args information to calleeCounterexamples
qadeer
2010-04-21
*
Fixed bug in translation of select/store arguments that are Boolean
qadeer
2010-04-20
*
Fixed bug in interprocedural counterexample generation
qadeer
2010-04-19
*
1. Fixed an off-by-one error in parsing array partitions in Z3 models
qadeer
2010-04-19
*
Fixed a bug. Call RegisterType before the collection of Select and Store fun...
qadeer
2010-04-19
*
First cut of lazy inlining. The option can be turned on by the flag /lazyInl...
qadeer
2010-04-17
*
Dafny: Removed the previous optional curly braces in match expressions (use p...
rustanleino
2010-04-02
*
Dafny:
rustanleino
2010-03-31
*
Dafny: Ensures that function axioms are not being used while their consisten...
rustanleino
2010-03-19
*
Dafny:
rustanleino
2010-03-18
*
Dafny:
rustanleino
2010-03-16
*
Dafny:
rustanleino
2010-03-16
*
Dafny: Added definedness checks for all statements (previously, some were mi...
rustanleino
2010-03-13
*
Added wellformedness checks to method specifications
rustanleino
2010-03-12
*
Dafny:
rustanleino
2010-03-12
*
Call program-wide lambda desugaring on axioms only. Call it on procedures in ...
MichalMoskal
2010-03-12
*
Boogie: Clone a TypedIdent to get rid of 'where' clauses during the translati...
rustanleino
2010-03-12
*
Dafny:
rustanleino
2010-03-11
*
Dafny: Added stratosphere tests for datatypes--that is, it is now checked th...
rustanleino
2010-03-11
[next]