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
*
Dafny: fixed bug in which old locals were not properly forbidden from being m...
Jason Koenig
2012-07-12
*
Dafny: labeled (and unlabled) block statements are now matched during refinem...
Jason Koenig
2012-07-12
*
Dafny: check that resolution successfully resolved all types, where appropriate.
Jason Koenig
2012-07-12
*
Merge
Unknown
2012-07-12
|
\
|
*
Dafny: restored soundness for refinement by disallowing certain updates and m...
Jason Koenig
2012-07-11
|
*
Dafny: fixed translation bug in maps with objects in the domain, added test case
Jason Koenig
2012-07-11
*
|
Dafny: added a copredicate test case
Unknown
2012-07-11
|
/
*
Dafny: fixed ghost checking for labeled (i.e. named) expressions, changed to ...
Jason Koenig
2012-07-10
*
Add some Mono/MonoDevelop files to .hgignore
Peter Collingbourne
2012-07-09
*
Merge
Unknown
2012-07-10
|
\
*
|
Read and write logging variables are now only generated if they do not alread...
Unknown
2012-07-10
|
*
Boogie build succeeded
CodeplexBot
2012-07-10
|
*
Dafny: fixed bad merge
Rustan Leino
2012-07-09
|
*
Dafny: rebuilt parser/scanner after previous merge
Rustan Leino
2012-07-09
|
*
Merge
Rustan Leino
2012-07-09
|
|
\
|
*
|
Dafny: More work on the coinduction principle
Rustan Leino
2012-07-09
|
|
*
Merge
Jason Koenig
2012-07-09
|
|
|
\
|
|
*
|
Dafny: fixed test case
Jason Koenig
2012-07-09
|
|
*
|
Dafny: added verification that replaced expressions are the same as the original
Jason Koenig
2012-07-09
|
|
*
|
Dafny: added named expressions and replacement
Jason Koenig
2012-07-09
|
|
|
*
GPUVerify: add beginnings of a test suite
Peter Collingbourne
2012-07-04
|
|
|
*
GPUVerify: merge blocks into predecessors before and after predication
Peter Collingbourne
2012-07-09
|
|
|
*
VCGen: add MergeBlocksIntoPredecessors function
Peter Collingbourne
2012-07-09
|
|
|
/
|
|
*
Dafny: types can now be qualified with full module paths
Jason Koenig
2012-07-06
|
|
*
Dafny: datatype constructors can be accessed across module boundaries.
Jason Koenig
2012-07-06
|
|
*
Dafny: fixed a crash in datatype argument resolution
Jason Koenig
2012-07-05
|
|
*
Merge
Jason Koenig
2012-07-05
|
|
|
\
|
|
*
|
Dafny: Fixed bug in autocontracts where the post resolver was run even if the...
Jason Koenig
2012-07-05
|
|
*
|
Dafny: disallow importing ghost modules into physical ones.
Jason Koenig
2012-07-05
|
*
|
|
Merge
Rustan Leino
2012-07-04
|
|
\
\
\
|
|
|
|
/
|
|
|
/
|
|
|
*
|
Made error trace generation (without labels) more general for stratified
Unknown
2012-07-04
|
|
|
/
|
|
*
Dafny: added static members of _default to the module level scope, at low pri...
Jason Koenig
2012-07-03
|
|
*
Merge
Jason Koenig
2012-07-03
|
|
/
|
|
/
|
|
|
|
*
Dafny: added support for nested abstract modules, fixed some translation issues
Jason Koenig
2012-07-03
|
*
|
Dafny: removed old Substitute method (which has been replaced by a Substitute...
Rustan Leino
2012-07-03
*
|
|
Worked on cross-thread annotations.
Unknown
2012-07-03
|
*
|
Merge
Rustan Leino
2012-07-03
|
|
\
\
|
*
|
|
Dafny: added copredicates
Rustan Leino
2012-07-03
|
*
|
|
Changed copyright year range to include 2012
Rustan Leino
2012-07-03
|
|
|
*
Dafny: re-added field non-uniqueness (was accidentally reverted by a bad merge)
Jason Koenig
2012-07-02
|
|
|
/
*
|
|
Merge
Unknown
2012-07-02
|
\
\
\
|
|
|
/
|
|
/
|
|
*
|
Reinstate GPUVerify files
Peter Collingbourne
2012-07-02
|
*
|
Merge
Jason Koenig
2012-07-02
|
|
\
\
|
|
*
|
Dafny: reinstated autocontracts
Jason Koenig
2012-07-02
*
|
|
|
Added support for non-predicated assertions
Unknown
2012-07-02
|
/
/
/
*
|
|
Merge
Unknown
2012-07-02
|
\
\
\
*
|
|
|
Started adding support for annotation intrinsics for unstructured programs.
Unknown
2012-07-02
|
*
|
|
Boogie build succeeded
CodeplexBot
2012-07-01
|
*
|
|
Chalice build succeeded
CodeplexBot
2012-06-30
|
|
|
/
|
|
/
|
|
|
*
Merge
Jason Koenig
2012-06-29
|
|
/
|
[next]