index
:
debian-boogie
dfsg_free
master
Debian packaging for Boogie
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
Source
Commit message (
Expand
)
Author
Age
*
added support for handling duplicate axioms
qadeer
2011-11-22
*
Merge
Unknown
2011-11-21
|
\
*
|
Generating useful, and guarateed by construction, postconditions and loop inv...
Unknown
2011-11-21
|
*
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
|
*
Dafny: fixed bad Code Contracts
Rustan Leino
2011-11-16
|
*
Merge
qadeer
2011-11-16
|
|
\
|
*
|
/contractInfer always prints the computed assignment now
qadeer
2011-11-16
|
*
|
refactoring houdini so that it creates only a single instance of z3
qadeer
2011-11-16
|
|
*
Boogie: fixed build error (incorrect type in Contract.Result)
Rustan Leino
2011-11-16
|
*
|
Eliminated unused argument in the constructor for Checker
qadeer
2011-11-16
|
|
*
Merge
Michal Moskal
2011-11-16
|
|
|
\
|
|
_
|
/
|
/
|
|
|
*
|
Merge
qadeer
2011-11-16
|
|
\
\
|
|
/
/
|
/
|
|
|
*
|
simple fix in houdini
qadeer
2011-11-16
*
|
|
Small fix.
Unknown
2011-11-16
*
|
|
Merge
Unknown
2011-11-16
|
\
\
\
*
|
|
|
Better support for race-checking contracts
Unknown
2011-11-16
|
*
|
|
Merge
akashlal
2011-11-16
|
|
\
\
\
|
|
*
|
|
Debugging output for stratified inlining. Emit attribute on Ensures while
Unknown
2011-11-16
|
|
|
/
/
|
|
|
*
BVD: Fix display bug
Michal Moskal
2011-11-15
|
|
|
*
VCC: Further data type improvements
Michal Moskal
2011-11-15
|
|
|
*
VCC: Better display of data type values
Michal Moskal
2011-11-15
|
*
|
|
DafnyExtension: fixed build problems
Rustan Leino
2011-11-15
|
*
|
|
Boogie (and Dafny, with effects also on SscBoogie): I refactored CommandLine...
Rustan Leino
2011-11-15
|
|
|
*
VCC: Recognize $result
Michal Moskal
2011-11-15
|
|
|
/
|
*
|
Merge
Rustan Leino
2011-11-15
|
|
\
|
|
|
*
Merge
qadeer
2011-11-15
|
|
|
\
|
|
_
|
/
|
/
|
|
|
|
*
changed inlining code so that candidate preconditions and postconditions are ...
qadeer
2011-11-15
*
|
|
Some fixes for race checking contracts
Unknown
2011-11-15
*
|
|
Modified solution to build on all platforms.
Unknown
2011-11-15
|
|
/
|
/
|
|
*
Dafny: added let expressions (syntax: "var x := E0; E1")
Rustan Leino
2011-11-14
*
|
fixed another bug in model parser related to datatype values
qadeer
2011-11-14
*
|
added the option /inlineDepth:n. This option defaults to -1. If the user prov...
qadeer
2011-11-13
|
*
Dafny: implemented the wellformedness check that datatype destructors are onl...
Rustan Leino
2011-11-11
|
/
*
Merge
qadeer
2011-11-11
|
\
|
*
moved the addition of selectors and testers to program.Resolve
qadeer
2011-11-11
*
|
Produce unsat cores only when enabled (in stratified inlining)
Unknown
2011-11-11
|
/
*
Dafny: allow assert/assume expressions in more places
Rustan Leino
2011-11-09
*
Dafny: added assert/assume expressions
Rustan Leino
2011-11-09
*
Merge
qadeer
2011-11-09
|
\
*
|
copied all attributes of the constructor (except for :constructor) to the sel...
qadeer
2011-11-09
|
*
VCC: remove _vcc_math_type_ from type names
Michal Moskal
2011-11-09
|
*
VCC: hide #limited# functions
Michal Moskal
2011-11-09
|
*
Merge
Rustan Leino
2011-11-09
|
|
\
|
*
|
Dafny: moved definition of class.array into prelude, anticipating writing axi...
Rustan Leino
2011-11-09
|
|
*
Refactoring, and work on race checking contracts
Unknown
2011-11-09
|
|
/
|
*
Merge
Rustan Leino
2011-11-09
|
|
\
|
*
|
Dafny: fixed part of a type-inference issue with datatypes and the < operator...
Rustan Leino
2011-11-09
|
|
*
BVD: don't do the "Duplicate entry exception"; uncomment for debugging
Michal Moskal
2011-11-08
[next]