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
*
Added functionality for race error reporting.
Egor Kyshtymov
2012-08-20
*
DafnyExtension: simplified display of type names and field names
Unknown
2012-08-17
*
DafnyExtension: various improvements
Unknown
2012-08-16
*
Fixed bug where source location attributes are not being attached to a CHECK
Unknown
2012-08-16
*
DafnyExtension: fixed more missing cases for hover texts
Unknown
2012-08-15
*
Dafny: fixed some bugs in the newly added DafnyExtension code
Unknown
2012-08-15
*
Dafny: added Statement.SubExpressions getter
Unknown
2012-08-15
*
Merge
Unknown
2012-08-14
|
\
*
|
Dafny: two bug fixes (resolution crashing on bad input, DafnyExtension crashi...
Unknown
2012-08-14
|
*
Added GPUVerifyBoogieDriver project.
Unknown
2012-08-14
|
*
Separated race checking into logging and checking calls. This simplifies
Unknown
2012-08-14
|
*
Removed some dud code for handling nested maps, which we no longer support.
Unknown
2012-08-13
|
*
Some more code cleanup related to removal of the "divided" option.
Unknown
2012-08-13
|
*
Removed code related to "divided" option.
Unknown
2012-08-13
|
/
*
Merge
Unknown
2012-08-13
|
\
*
|
Barrier divergence checking now achieved via precondition.
Unknown
2012-08-13
|
*
Dafny: internal renaming
Unknown
2012-08-10
|
*
Dafny: added heuristics for finding witnesses in assign-such-that checking
Unknown
2012-08-10
|
*
DafnyExtension: hide execution-trace output, show split-expr related error l...
Rustan Leino
2012-08-10
|
*
Dafny: fixed parser crash
Unknown
2012-08-09
|
/
*
Merge
Unknown
2012-08-09
|
\
*
|
Unstructured and smart predication are now default options for GPUVerify.
Unknown
2012-08-09
|
*
DafnyExtension: improvements
Rustan Leino
2012-08-08
|
*
Merge
Unknown
2012-08-08
|
|
\
|
*
|
Dafny: the DafnyExtension mode for Visual Studio now calls the verifier and v...
Unknown
2012-08-08
*
|
|
Merge
Unknown
2012-08-07
|
\
\
\
|
|
|
/
|
|
/
|
*
|
|
Revised candidate invariant generation for barrier divergence checking.
Unknown
2012-08-07
|
*
|
Houdini: recognise candidates of the form (p => (q => (... => (e => phi)))) w...
Peter Collingbourne
2012-08-07
|
/
/
*
|
Smart block predicator: track parents, and use to emit the invariant that if ...
Peter Collingbourne
2012-08-06
*
|
Smart block predicator: move *Map from parameters to fields
Peter Collingbourne
2012-08-06
*
|
Smart block predicator: drop the unused createCandidateInvariants parameter
Peter Collingbourne
2012-08-06
*
|
Dafny: corrected comment
Jason Koenig
2012-08-03
*
|
Core: attach :partition to assumes generated from structured ifs and whiles
Peter Collingbourne
2012-08-03
|
/
*
Dafny: fixed bug in reverifying allowing old locals to be modified.
Jason Koenig
2012-08-01
*
Dafny: reverify if the refining method modifies the heap.
Jason Koenig
2012-08-01
*
Dafny: fixed bug where expressions were not replaced.
Jason Koenig
2012-08-01
*
Dafny: support opening modules into the local scope
Jason Koenig
2012-07-30
*
Dafny: removed allocated keyword, changed module import syntax. "opened" keyw...
Jason Koenig
2012-07-30
*
GPUVerify: add an option which controls whether to use smart predication
Peter Collingbourne
2012-07-30
*
VCGeneration: implement smart predication
Peter Collingbourne
2012-07-30
*
Graph: make DomRelation and DominatorMap public
Peter Collingbourne
2012-07-11
*
BoogieDriver: correctly display time taken by prover if >60 seconds
Peter Collingbourne
2012-07-30
*
Dafny: removed allocated, changed semantics of fresh
Jason Koenig
2012-07-29
*
Dafny: added structural refinement check
Jason Koenig
2012-07-29
*
Merge
Unknown
2012-07-20
|
\
*
|
Implemented Houdini-based pointer analysis. Made inter-group race checking d...
Unknown
2012-07-20
|
*
Dafny: fixed datatype GetHashCode() to make it consistent with Equals()
Jason Koenig
2012-07-18
|
*
Dafny: allowed strictly finite datatypes in comprehensions, quantifiers, and ...
Jason Koenig
2012-07-17
|
*
Dafny: compilation of abstract modules, including local definitions (as in mo...
Jason Koenig
2012-07-17
|
*
Dafny: allow implict self (as in "`field") in frame declarations.
Jason Koenig
2012-07-16
|
/
[next]