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
*
Boogie: output number of proof obligations (asserts) along with timing inform...
Rustan Leino
2012-01-09
*
made delegate a datatype
qadeer
2011-12-30
*
fixed problems with datatypes
qadeer
2011-12-29
*
fixed a completeness problem in houdini with inlining
qadeer
2011-12-18
*
Fixed the Boogie build.
wuestholz
2011-12-16
*
Dafny: Made sure that error locations refer to the Dafny program, even if the...
wuestholz
2011-12-15
*
Boogie: Changed Expr.Not to keep swap arguments rather change direction of op...
Rustan Leino
2011-12-12
*
Merge
Rustan Leino
2011-12-07
|
\
|
*
Merge
Michal Moskal
2011-12-07
|
|
\
|
*
|
Fix atg file and add comment about Set/*Variable*/
Michal Moskal
2011-12-07
|
*
|
Make set iteration order deterministic
Michal Moskal
2011-12-07
*
|
|
Merge
Rustan Leino
2011-12-05
|
\
\
\
|
|
|
/
|
|
/
|
*
|
|
Boogie: Added new abstract interpretation harness, which uses native Boogie E...
Rustan Leino
2011-12-05
|
|
/
|
/
|
|
*
Emit attribute on a requires
akashlal
2011-12-04
|
/
*
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
|
/
[next]