index
:
debian-boogie
dfsg_free
master
Debian packaging for Boogie
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
Source
/
VCGeneration
Commit message (
Expand
)
Author
Age
*
Added functionality for race error reporting.
Egor Kyshtymov
2012-08-20
*
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
*
VCGeneration: implement smart predication
Peter Collingbourne
2012-07-30
*
VCGen: add MergeBlocksIntoPredecessors function
Peter Collingbourne
2012-07-09
*
Made error trace generation (without labels) more general for stratified
Unknown
2012-07-04
*
Worked on cross-thread annotations.
Unknown
2012-07-03
*
Added support for non-predicated assertions
Unknown
2012-07-02
*
Started adding support for annotation intrinsics for unstructured programs.
Unknown
2012-07-02
*
Merge
Unknown
2012-06-25
|
\
*
\
Merge
Unknown
2012-06-21
|
\
\
|
|
*
merge with Peter's changes
qadeer
2012-06-20
|
|
*
Merge
qadeer
2012-06-20
|
|
|
\
|
|
|
/
|
|
/
|
|
*
|
Block predicator: handle StateCmd
Peter Collingbourne
2012-06-20
|
|
*
a bug fix
qadeer
2012-06-19
|
|
*
another edit for predication
qadeer
2012-06-19
|
|
*
integrating predication
qadeer
2012-06-19
|
|
/
|
*
Merge
qadeer
2012-06-18
|
|
\
|
|
/
|
/
|
|
*
Fix line endings
Peter Collingbourne
2012-06-18
|
*
Move block predicator to VCGeneration
Peter Collingbourne
2012-06-18
|
/
*
deleted an unused class
qadeer
2012-06-12
*
refactoring in SI
qadeer
2012-06-12
*
Merge
qadeer
2012-06-10
|
\
*
|
1. changed new SI implemnetation so that it performs substitution for call sites
qadeer
2012-06-10
|
*
Dafny/Boogie/BVD: made Dafny plug-in for BVD work again
Rustan Leino
2012-06-08
|
/
*
final (hopefully) fix to new SI
qadeer
2012-06-07
*
testing a fix in SI
qadeer
2012-06-07
*
Merging again
Ken McMillan
2012-06-07
|
\
|
*
Trying to merge with recent changes, failing.
Ken McMillan
2012-06-05
|
|
\
|
|
*
Some changes to support expanded use of z3api.
Ken McMillan
2012-06-05
*
|
|
Bug fix with mvInfo during VCGen
akashlal
2012-06-06
*
|
|
update to SI
qadeer
2012-06-04
|
/
/
*
|
moved class Macro to Absy
qadeer
2012-06-04
*
|
added FindLeastToVerify to StratfiedVCGenBase as an abstract method
qadeer
2012-05-30
*
|
moved a couple of overrides from StratifiedVCGen to StratifiedVCGenBase
qadeer
2012-05-30
*
|
added support for recordProcCallSites to new SI
qadeer
2012-05-30
*
|
extra recursion bound
akashlal
2012-05-30
*
|
further refactoring of SI;
qadeer
2012-05-29
*
|
Removed program argument from VerifyImplementation. It is redundant since th...
qadeer
2012-05-29
*
|
further refactoring
qadeer
2012-05-28
*
|
more refactoring
qadeer
2012-05-28
*
|
Merge
qadeer
2012-05-28
|
\
\
*
|
|
removed call site simplification from the old SI flow
qadeer
2012-05-28
|
*
|
No need for extra attributes in ExtractLoops
akashlal
2012-05-28
|
*
|
updating FindLeastToVerify to the new flow
akashlal
2012-05-28
|
/
/
*
|
Better interface for adding skipped calls, and
akashlal
2012-05-26
*
|
new stratified inlining (initial prototype)
qadeer
2012-05-25
*
|
more refactoring in stratified inlining
qadeer
2012-05-24
*
|
small fix
qadeer
2012-05-21
[next]