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
*
Added option of turning off model generation in SI. Can be very expensive som...
akashlal
2011-11-26
*
fixed bug in the inlineDepth option for houdini
qadeer
2011-11-23
*
Merge
qadeer
2011-11-22
|
\
|
*
Boogie: don't resolve ignored types (that is, "extern" types that have been t...
Rustan Leino
2011-11-22
*
|
added support for handling duplicate axioms
qadeer
2011-11-22
|
/
*
Added lazy summary computation to stratified inlining (not finished yet)
akashlal
2011-11-20
*
commented calls to GC.Collect()
qadeer
2011-11-18
*
changed the semantics of requires and ensures for inlined procedures
qadeer
2011-11-17
*
Boogie: fixed build error (incorrect type in Contract.Result)
Rustan Leino
2011-11-16
*
Merge
akashlal
2011-11-16
|
\
|
*
Debugging output for stratified inlining. Emit attribute on Ensures while
Unknown
2011-11-16
*
|
Boogie (and Dafny, with effects also on SscBoogie): I refactored CommandLine...
Rustan Leino
2011-11-15
|
/
*
changed inlining code so that candidate preconditions and postconditions are ...
qadeer
2011-11-15
*
added the option /inlineDepth:n. This option defaults to -1. If the user prov...
qadeer
2011-11-13
*
moved the addition of selectors and testers to program.Resolve
qadeer
2011-11-11
*
Merge
qadeer
2011-11-07
|
\
|
*
Dafny: added a new /inductionHeuristic option
Rustan Leino
2011-11-04
|
*
Dafny: added options to make Induction Heuristic apply to array index express...
Rustan Leino
2011-11-04
*
|
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
[next]