index
:
debian-boogie
dfsg_free
master
Debian packaging for Boogie
summary
refs
log
tree
commit
diff
log msg
author
committer
range
Commit message (
Expand
)
Author
Age
...
|
*
|
Merge
Rustan Leino
2011-06-29
|
|
\
\
|
*
|
|
Boogie: use (WEIGHT 0) with the select-of-store axioms
Rustan Leino
2011-06-29
|
*
|
|
Dafny: Fixed axioms for Seq#Contains vs. the sequence building functions
Rustan Leino
2011-06-29
*
|
|
|
Initial implementation of return statments with parameters.
Jason Koenig
2011-06-29
|
|
/
/
|
/
|
|
*
|
|
Removed development comments.
Jason Koenig
2011-06-29
*
|
|
Merge
Jason Koenig
2011-06-29
|
\
\
\
*
|
|
|
Added regression test file LoopModifies.dfy.
Jason Koenig
2011-06-29
|
*
|
|
Boogie build succeeded, 1 test(s) failed
CodeplexBot
2011-06-29
|
/
/
/
*
|
|
Merge
Jason Koenig
2011-06-28
|
\
\
\
*
|
|
|
Added regression test for loop modifies clauses.
Jason Koenig
2011-06-28
*
|
|
|
Changed regression test answer for dafny0 to reflect new error messages.
Jason Koenig
2011-06-28
*
|
|
|
Initial modifies on loops implementation. Still some errors remaining.
Jason Koenig
2011-06-28
|
*
|
|
ported all the counterexample code to Michal's new Model class; the goal is t...
Unknown
2011-06-27
|
/
/
/
*
|
|
Boogie build succeeded
CodeplexBot
2011-06-27
*
|
|
Fixed non-incremental option of stratified inlining
Unknown
2011-06-27
*
|
|
FindLeastToVerify: accept multiple procedures
Unknown
2011-06-26
*
|
|
Call PostOrderVisitIterative by default
Unknown
2011-06-26
*
|
|
Added an iterative version of PostOrderVisit (but it is not called)
Unknown
2011-06-26
*
|
|
Avoid restarting the theorem prover for stratified inlining because it
Unknown
2011-06-25
*
|
|
early clearing of live variables and incarnation maps
qadeer
2011-06-24
|
|
*
fixed some minor bugs:
Unknown
2011-06-24
|
|
*
- implemented code generation from a synthesis solution (simple field
Unknown
2011-06-24
*
|
|
further refactoring
qadeer
2011-06-24
|
|
*
- implemented reading models from a BVD model file
Unknown
2011-06-24
*
|
|
Merge
qadeer
2011-06-24
|
\
\
\
*
|
|
|
extra test files
qadeer
2011-06-24
*
|
|
|
fixes to z3api
qadeer
2011-06-24
|
*
|
|
Boogie build succeeded
CodeplexBot
2011-06-24
|
/
/
/
*
|
|
Merge
qadeer
2011-06-23
|
\
\
\
*
|
|
|
implementation of iterative LetVC
qadeer
2011-06-23
|
*
|
|
Merge
Jason Koenig
2011-06-23
|
|
\
\
\
|
*
|
|
|
Added loop modifies clause syntax.
Jason Koenig
2011-06-23
|
|
|
/
/
|
|
/
|
|
*
|
|
|
Merge
qadeer
2011-06-23
|
\
\
\
\
|
|
|
/
/
|
|
/
|
|
*
|
|
|
bug fix in translation of dispatch continuation
qadeer
2011-06-23
|
*
|
|
Didn't intend to include Z3api by default
Unknown
2011-06-23
|
*
|
|
Bug fix for trace generation with extractLoop option
Unknown
2011-06-23
|
|
\
\
\
|
|
/
/
/
|
/
|
|
|
|
*
|
|
Bug fix for trace generation with extractLoop option
Unknown
2011-06-23
*
|
|
|
clean up in z3api
qadeer
2011-06-22
|
/
/
/
*
|
|
Merge
qadeer
2011-06-22
|
\
|
|
*
|
|
partial fixes to these regressions
qadeer
2011-06-22
*
|
|
various fixes to port to latest version of Microsoft.Z3.dll
qadeer
2011-06-22
|
*
|
Merge
Rustan Leino
2011-06-21
|
|
\
\
|
|
/
/
|
/
|
|
|
*
|
Dafny: bug fix in generating IsCanonicalBoolBox predicates
Rustan Leino
2011-06-21
*
|
|
Merge
qadeer
2011-06-20
|
\
|
|
*
|
|
Translate IConditional exactly the same way as IConditionalStatement to accou...
qadeer
2011-06-20
|
*
|
Merge
Rustan Leino
2011-06-20
|
|
\
\
|
|
/
/
|
/
|
|
|
*
|
Dafny: better error message when "decreases *" is attempted on a function or ...
Rustan Leino
2011-06-20
*
|
|
Merge
qadeer
2011-06-20
|
\
|
|
*
|
|
whole bunch of bug fixes
qadeer
2011-06-20
|
*
|
Merge
Rustan Leino
2011-06-20
|
|
\
\
[prev]
[next]