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
...
*
|
Boogie: Eliminated the /bv option. Only native bitvectors are supported now. ...
Rustan Leino
2011-10-27
|
*
various refactorings
qadeer
2011-10-27
|
/
*
Added a push+pop+unsat-core interface to SMTLib (for stratified inlining only)
Unknown
2011-10-19
*
revised implementation of proc copy bounding
qadeer
2011-10-16
*
Bug fix to stratified inlining error trace values
Unknown
2011-09-28
*
Name the constant used in @MV_state function applications - otherwise we get ...
Michal Moskal
2011-09-26
*
fixed bug in data value generation
qadeer
2011-09-13
*
Added some extra functionality to Model code for corral
Unknown
2011-09-13
*
fixes to model value generation for stratified inlining
qadeer
2011-09-12
*
further fixes
qadeer
2011-09-08
*
minor fixes
qadeer
2011-09-07
*
Merge
qadeer
2011-09-07
|
\
|
*
Improvement for ProcCopyBounding
Unknown
2011-09-07
*
|
bug fix
qadeer
2011-09-06
*
|
further fixes
qadeer
2011-09-06
*
|
partial check in regarding getting states working with stratified inlining
qadeer
2011-09-06
|
/
*
Options.PostParse() is called by Parse(), so set command-line-derived options...
Michal Moskal
2011-08-30
*
Bug fix for Proc-Copy-Bounding
Unknown
2011-08-28
*
Procedure Copy Bounding for Stratified Inlinig
Unknown
2011-08-25
*
reverting irreducible handling temporarily
qadeer
2011-08-21
|
\
*
|
added code to handle irreducible graphs
qadeer
2011-08-20
*
|
minor refactoring
qadeer
2011-08-17
*
|
deleted lazyinlining option 2 and 3
qadeer
2011-08-17
*
|
Added "procedure-copy bounding" for lazy inlining
Unknown
2011-08-10
*
|
further changes for making houdini work
qadeer
2011-08-04
|
/
*
ported all the counterexample code to Michal's new Model class; the goal is t...
Unknown
2011-06-27
*
Fixed non-incremental option of stratified inlining
Unknown
2011-06-27
*
FindLeastToVerify: accept multiple procedures
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
*
implementation of iterative LetVC
qadeer
2011-06-23
*
Bug fix for trace generation with extractLoop option
Unknown
2011-06-23
*
Add a string for an uninterpreted value in errModel
Unknown
2011-06-06
*
LetVC can get null label2absy from lazy inlining. So, I weakened the precond...
qadeer
2011-05-03
*
modified letvc generation so that the use of control flow function and labels...
qadeer
2011-04-15
*
merge
Unknown
2011-04-14
|
\
*
|
added reachability information to the VC and used that to support arbitrary a...
Unknown
2011-04-14
|
*
Stratified Inlining: minor bux fix with recording model values
Unknown
2011-04-14
|
/
*
Minor fixes
schaef
2011-03-27
*
Boogie: fixed contract violation in stratified inlining
rustanleino
2011-03-23
*
Print recorded value of any type
akashlal
2011-03-21
*
Bug fix with model generation.
akashlal
2011-03-21
*
minor fix with loopy counterexample generation
akashlal
2011-03-18
*
Print out requested values in the counterexample trace
akashlal
2011-03-17
*
Re-enabled quantifier checking in the Checked configuration.
mikebarnett
2011-03-16
*
new algorithm for dead code detection (vc:doomed)
schaef
2011-03-15
*
Turn off quantifier checking in the runtime checking.
mikebarnett
2011-03-14
*
Replaced all dictionaries that mapped to bool (i.e., were being used to imple...
mikebarnett
2011-03-10
*
Renamed NonNullElements to NonNullDictionaryAndValues because the keys to dic...
mikebarnett
2011-03-10
*
Updated PrepareBoogieZip.bat to include BVD and smt2
rustanleino
2011-03-10
[prev]
[next]