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
*
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
*
Dafny:
rustanleino
2010-03-10
*
Boogie: Added resolution and type checking for attributes on "call" and "call...
rustanleino
2010-03-09
*
added support for printing attributes on calls via Emit
qadeer
2010-03-08
*
added attributes to CallForallCmd as well
qadeer
2010-03-07
*
added the ability to annotate calls with attributes
qadeer
2010-03-06
*
Boogie:
rustanleino
2010-02-20
*
added an option /doModSetAnalysis specially for Zvonimir
qadeer
2010-02-20
[next]