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
...
*
Improved invariant inference.
Unknown
2012-03-28
*
Merge
Unknown
2012-03-26
|
\
*
|
Started adding another invariant generation analysis.
Unknown
2012-03-26
|
*
Switch bvd to MSIL (instead of x86) target architecture
stobies
2012-03-26
|
*
Emit of invariants now prints out the invariant attributes also
qadeer
2012-03-26
|
/
*
Started on live variable analysis in GPUVerify
Unknown
2012-03-26
*
Added "may be power of two" analysis.
Unknown
2012-03-25
*
Added "may be tid" analysis.
Unknown
2012-03-24
*
Fixed some bugs in uniformity analysis - now passes GPUVerify test suite.
Unknown
2012-03-24
*
Using uniform expression analysis in GPUVerify - also did some major refactor...
Unknown
2012-03-24
*
Merge
Unknown
2012-03-23
|
\
*
|
Added uniform expression analysis, and started using it to do less predication.
Unknown
2012-03-23
|
*
added attributes to loop invariants
qadeer
2012-03-23
*
|
Do not generate equality candidates for variables that are not in the mod set.
Unknown
2012-03-22
|
/
*
Cleaned up some GPUVerify code.
Unknown
2012-03-22
*
Added the option to let user determine whether or not GPUVerify should add in...
Unknown
2012-03-19
*
Merge
Unknown
2012-03-18
|
\
*
|
Support for arrays with arbitrary indices
Unknown
2012-03-18
|
*
more type checking for datatypes
qadeer
2012-03-18
|
/
*
Improved kernel precondition generation
Unknown
2012-03-17
*
Merge
Unknown
2012-03-16
|
\
*
|
Added support for further annotations
Unknown
2012-03-16
|
*
Dafny: support assign-such-that in var declarations in refinements
Unknown
2012-03-15
|
*
Dafny: fixed lack of assign-such-that restriction in parallel statement
Unknown
2012-03-15
|
*
Dafny: added assign-such-that statements; syntax: x,y,a[i],o.f :| Expr;
Unknown
2012-03-15
|
*
Boogie: Simplified (and liberalized) parsing of string literals as attribute ...
Unknown
2012-03-12
|
*
updated Boogie strings so that they can refer to \" (and more)
qadeer
2012-03-12
|
*
make the call to ProcessDataTypeConstructors in the right place
qadeer
2012-03-11
|
*
Merge
qadeer
2012-03-10
|
|
\
|
*
|
houdini cleanup continued
qadeer
2012-03-10
|
|
*
Dafny: fixed build error
Rustan Leino
2012-03-09
|
|
*
Merge
Unknown
2012-03-09
|
|
|
\
|
|
*
|
Boogie: map the given filename stdin.bpl to standard input
Unknown
2012-03-09
|
|
/
/
|
|
*
Dafny: fixed compilation problem with names in _default module
Rustan Leino
2012-03-08
|
|
/
|
*
Dafny: added ghost modules (the meaning is simply that such a module will not...
Rustan Leino
2012-03-07
|
*
Dafny: added experimental feature {:autocontracts} to de-clutter idiomatic sp...
Unknown
2012-03-05
|
/
*
Race checking assertions are now added as invariants and pre/post conditions ...
Unknown
2012-03-05
*
Support for __all and __at_most_one annotations
Unknown
2012-03-04
*
Merge
Unknown
2012-03-04
|
\
*
|
More annotation support
Unknown
2012-03-04
|
*
Merge
Unknown
2012-03-02
|
|
\
|
*
|
Dafny: allow more skeleton statements in refinements
Unknown
2012-03-02
|
|
*
small fix for a bug I introduced during the refactoring of InferAndVerify
qadeer
2012-03-02
|
|
*
Merge
qadeer
2012-03-02
|
|
|
\
|
|
_
|
/
|
/
|
|
|
|
*
various refactorings related to houdini
qadeer
2012-03-02
*
|
|
Merge
Unknown
2012-03-01
|
\
\
\
|
|
|
/
|
|
/
|
*
|
|
Support for access annotations.
Unknown
2012-03-01
|
|
/
|
/
|
|
*
Dafny: fixed well-formedness checking of LET expressions to allow the RHS to ...
Rustan Leino
2012-02-29
|
/
*
Added missing files.
Unknown
2012-02-29
*
Merge
Unknown
2012-02-29
|
\
[prev]
[next]