index
:
debian-boogie
dfsg_free
master
Debian packaging for Boogie
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
Source
/
Core
Commit message (
Expand
)
Author
Age
*
deleted unused code
qadeer
2011-11-01
*
Merge
Rustan Leino
2011-10-29
|
\
*
|
Dafny induction:
Rustan Leino
2011-10-29
|
*
Boogie: Get rid of {:inline} attributes on axioms
Michal Moskal
2011-10-27
|
*
Boogie: Get rid of {:ignore} feature on axioms
Michal Moskal
2011-10-27
|
*
Boogie: removed unreachable or unused code
Rustan Leino
2011-10-27
|
*
Boogie: internal clean-up, removed BvHandling type, everything now behaves as...
Rustan Leino
2011-10-27
|
*
Boogie: Eliminated the /bv option. Only native bitvectors are supported now. ...
Rustan Leino
2011-10-27
|
*
Boogie: Changed default /prover to SMTLIB
Rustan Leino
2011-10-27
|
/
*
Added a push+pop+unsat-core interface to SMTLib (for stratified inlining only)
Unknown
2011-10-19
*
Merge
Rustan Leino
2011-09-28
|
\
|
*
bitvector fixes
qadeer
2011-09-24
|
*
Dafny: Fixed an assertion violation in the "Checked" configuration.
wuestholz
2011-09-20
*
|
Merge
Rustan Leino
2011-09-17
|
\
\
|
|
*
Dafny: Added support for attributes on methods and constructors.
wuestholz
2011-09-16
|
|
*
Fixed test failures in the "Checked" configuration.
wuestholz
2011-09-19
|
|
/
|
*
Added "free call" statements that don't check the precondition in the caller.
wuestholz
2011-09-14
*
|
Dafny: generate a compiler error upon encountering an assume statement
Rustan Leino
2011-09-11
|
/
*
further edits
qadeer
2011-09-01
*
improved bitvector analysis
qadeer
2011-09-01
*
Merge
qadeer
2011-08-29
|
\
*
|
more changes to bitvector analysis
qadeer
2011-08-29
|
*
Merge
Michal Moskal
2011-08-29
|
|
\
|
|
/
|
/
|
|
*
Add PROVER_PATH prover option (to base options, but currently only used by SM...
Michal Moskal
2011-08-29
*
|
Fixed a bug with "don't care" return value on an async call
Unknown
2011-08-24
|
/
*
Support for irreducible graphs (with extractLoops)
Unknown
2011-08-24
*
reverting irreducible handling temporarily
qadeer
2011-08-21
|
\
*
|
added code to handle irreducible graphs
qadeer
2011-08-20
*
|
deleted lazyinlining option 2 and 3
qadeer
2011-08-17
*
|
Added "procedure-copy bounding" for lazy inlining
Unknown
2011-08-10
*
|
further updates to bit vector analysis
qadeer
2011-08-09
*
|
more changes to bitvector analysis
qadeer
2011-08-09
*
|
another bug fix in bct
qadeer
2011-08-08
*
|
added a new file and fixed a bug in bct
qadeer
2011-08-08
*
|
various changes to boogie for bitvector analysis and bctprovider
qadeer
2011-08-08
*
|
cleaned up houdini options
qadeer
2011-08-04
*
|
Updated the Parser.cs and Scanner.cs files in Boogie and Dafny and removed so...
wuestholz
2011-07-15
*
|
async call return value is either int or bv32
qadeer
2011-07-09
*
|
ExtractLoops calls the same code for eliminating unreachable blocks that norm...
qadeer
2011-07-05
*
|
Merge
Michal Moskal
2011-07-05
|
\
\
|
*
|
Boogie: New cli option -z3exe:"path-to-z3.exe" allowing specifying path to th...
Unknown
2011-07-05
|
*
|
Added the /noCheating option. (treats assume as assert and drops free.)
Jason Koenig
2011-07-01
*
|
|
Allow : instead of = in options
Michal Moskal
2011-06-30
|
|
/
|
/
|
|
*
Added option to force Dafny compilation, even if verification fails.
Jason Koenig
2011-06-30
|
/
*
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 in live variable analysis
qadeer
2011-06-14
*
Boogie: white-space formating
Rustan Leino
2011-06-05
*
close the file stream opened by the parser
Unknown
2011-05-19
[next]