index
:
debian-boogie
dfsg_free
master
Debian packaging for Boogie
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
Test
Commit message (
Expand
)
Author
Age
...
*
Dafny: implemented thresholds for the new interval domain (/infer:j)
Rustan Leino
2011-12-12
*
Boogie: Changed Expr.Not to keep swap arguments rather change direction of op...
Rustan Leino
2011-12-12
*
Dafny: fix bug in translation of (the splitting of) if-then-else expressions ...
Rustan Leino
2011-12-10
*
Merge
Rustan Leino
2011-12-07
|
\
*
\
Merge
Rustan Leino
2011-12-07
|
\
\
|
*
\
Merge
Michal Moskal
2011-12-07
|
|
\
\
|
*
|
|
Make it work with mingw
Michal Moskal
2011-12-07
|
|
*
|
Dafny: Added a separate script to run all Dafny tests.
wuestholz
2011-12-07
*
|
|
|
Merge
Rustan Leino
2011-12-07
|
\
\
\
\
|
|
|
/
/
|
|
/
|
|
|
*
|
|
Dafny: Forward attributes on Dafny functions to Boogie (e.g., to disable well...
wuestholz
2011-12-07
*
|
|
|
Dafny tests: Disabled SnapshotableTrees.dfy for now while performance issues ...
Rustan Leino
2011-12-07
*
|
|
|
Merge
Rustan Leino
2011-12-06
|
\
|
|
|
|
*
|
|
first check in
qadeer
2011-12-05
*
|
|
|
Merge
Rustan Leino
2011-12-05
|
\
|
|
|
*
|
|
|
Boogie: Added new abstract interpretation harness, which uses native Boogie E...
Rustan Leino
2011-12-05
|
*
|
|
further fixes to houdini
qadeer
2011-12-05
|
|
/
/
|
*
|
Updated the 'Answer' file for test2.
wuestholz
2011-12-02
|
*
|
Boogie: Fixed a crash due to old expressions in lambda expressions that were ...
wuestholz
2011-12-02
|
/
/
*
|
added some more statistics to houdini
qadeer
2011-11-24
*
|
fixed bug in the inlineDepth option for houdini
qadeer
2011-11-23
|
*
Merge
Rustan Leino
2011-11-22
|
|
\
|
|
/
|
/
|
*
|
Dafny: call C# compiler directly from inside Dafny, and optionally produce a ...
Rustan Leino
2011-11-22
|
*
Dafny: Added "type" declaration (syntax: "type X;"), which introduces an arbi...
Rustan Leino
2011-11-21
*
|
changed the semantics of requires and ensures for inlined procedures
qadeer
2011-11-17
|
/
*
/contractInfer always prints the computed assignment now
qadeer
2011-11-16
*
Merge
Rustan Leino
2011-11-15
|
\
*
|
Added Dafny solutions to the VSTTE 2012 program verification competition
Rustan Leino
2011-11-15
*
|
Dafny: added let expressions (syntax: "var x := E0; E1")
Rustan Leino
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
|
/
*
Many, many bug fixes related to generics and some other random problems.
Mike Barnett
2011-11-10
*
Dafny: allow assert/assume expressions in more places
Rustan Leino
2011-11-09
*
Dafny: added assert/assume expressions
Rustan Leino
2011-11-09
*
Dafny: fixed part of a type-inference issue with datatypes and the < operator...
Rustan Leino
2011-11-09
*
Dafny: fixed bug in reads checking of array-to-sequence conversions
Rustan Leino
2011-11-08
*
Dafny: Cleaned up proof of RevConcat in test case
Rustan Leino
2011-11-08
*
Dafny: in test suite (Rippling.dfy), replaced an inline lemma with a call to ...
Rustan Leino
2011-11-04
*
Added some Dafny and Boogie test cases, including Turing's factorial program,...
Rustan Leino
2011-11-03
*
Merge
Rustan Leino
2011-10-31
|
\
|
*
File to experiment with type encoding for .NET.
Mike Barnett
2011-10-31
*
|
Merge
Rustan Leino
2011-10-31
|
\
\
|
|
/
|
/
|
*
|
Removed prover option from runtest.bat because smtlib is now the default
Mike Barnett
2011-10-30
|
*
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: Eliminated the /bv option. Only native bitvectors are supported now. ...
Rustan Leino
2011-10-27
|
/
*
Dafny: removed Dafny's "foreach" statements (replaced by the new "parallel" s...
Rustan Leino
2011-10-26
*
Dafny: removed support for assigning to an array-range (that is, an assignmen...
Rustan Leino
2011-10-26
*
Merge
Rustan Leino
2011-10-26
|
\
*
|
Dafny: Commented out SnapshotableTrees.Node.FunctionalInsert while performanc...
Rustan Leino
2011-10-26
[prev]
[next]