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: handle refinement of nested tokens that come from SpliExpr (still need...
Rustan Leino
2012-01-12
*
Dafny: make full predicate definitions available only inside a module (outsid...
Rustan Leino
2012-01-11
*
Dafny: allow class-member declarations at top level of any module (not just t...
Rustan Leino
2012-01-10
*
Dafny: added test case for refinement and predicates (and fixed a parsing bug)
Rustan Leino
2012-01-10
*
Dafny: allow definitions and uses of parameter-less predicates to go without ...
Rustan Leino
2012-01-10
*
Dafny: added predicates
Rustan Leino
2012-01-10
*
Dafny: added support for simple superposition refinements
Rustan Leino
2012-01-09
*
Merge
Rustan Leino
2012-01-05
|
\
*
|
Dafny: firmed up the module system
Rustan Leino
2012-01-05
|
*
Disable datatypes test until Z3 is updated.
Mike Barnett
2012-01-05
*
|
Dafny: disengaged old refinement test files
Rustan Leino
2012-01-04
|
/
*
Dafny: don't allow ghost expressions in print statements
Rustan Leino
2012-01-03
*
added a test for generalized array theory
qadeer
2011-12-30
*
added the datatypes test
qadeer
2011-12-29
*
fixed problems with datatypes
qadeer
2011-12-29
*
Dafny: Fixed a bug in the pretty printer.
wuestholz
2011-12-26
*
Dafny: Extended the support for attributes on method/constructor calls.
wuestholz
2011-12-23
*
Dafny: Added support for attributes on method/constructor calls.
wuestholz
2011-12-21
*
forgot to check it in
qadeer
2011-12-21
*
Dafny: for a datatype with just one constructor, don't check (but do assume) ...
Rustan Leino
2011-12-19
*
fixed a completeness problem in houdini with inlining
qadeer
2011-12-18
*
Dafny: Made sure that error locations refer to the Dafny program, even if the...
wuestholz
2011-12-15
*
Dafny: Added support for attributes on various specification constructs (asse...
wuestholz
2011-12-07
*
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
[next]