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
*
Added tests for extractloops
akashlal
2010-09-04
*
Dafny: Added Dafny solutions to the VSComp 2010 problems
rustanleino
2010-09-01
*
Change Synonym type printing to what it was, use a workaround in TypeToString...
MichalMoskal
2010-08-18
*
Boogie: Fixed test 'bitvectors'.
wuestholz
2010-08-14
*
Updated answer to this regression to reflect the fact that it is now verified.
tabarbe
2010-08-12
*
Boogie: This reg test was not running verification.
tabarbe
2010-08-12
*
Added the option /extractLoops to extract loops as procedure calls. If eithe...
qadeer
2010-08-11
*
Fix the test to use new name for /z3bv option.
MichalMoskal
2010-08-10
*
Boogie: Added boolean code expressions (sans well-formedness checks on the in...
rustanleino
2010-08-10
*
Boogie: That file should not have been in the depot, but rather be created lo...
tabarbe
2010-08-09
*
Boogie: added /z3bv option that overrides the current setting of Z3 options f...
stobies
2010-08-06
*
Boogie: Added a new simple regression test, "sanity", which runs a single tes...
tabarbe
2010-07-29
*
Dafny: better error reporting on resolution of refinements. Replace assertion...
kyessenov
2010-07-14
*
Dafny: Axiom about inverting a set union operation, similar to the recent on...
rustanleino
2010-07-09
*
Boogie: Added stratified inlining. It is enabled using the flag /stratifiedIn...
akashlal
2010-07-07
*
Dafny:
rustanleino
2010-07-06
*
Added a comment noting that this test fails with Z3 2.4.
mschwerhoff
2010-07-06
*
Dafny: added assertions in the refinement obligation necessitating that the r...
kyessenov
2010-07-03
*
Dafny: Support class type parameters in refinements. Added another regression...
kyessenov
2010-07-02
*
Dafny: added Carrol Morgan's calculator regression test.
kyessenov
2010-07-02
*
Dafny: support input/output parameters in refined methods.
kyessenov
2010-07-02
*
Dafny: added a regression test for the refinement extension.
kyessenov
2010-07-02
*
Dafny:
rustanleino
2010-06-24
*
Updated the frame files to work with the latest Coco/R. This entails *not* ha...
mikebarnett
2010-06-22
*
Boogie:
rustanleino
2010-06-22
*
Dafny:
rustanleino
2010-06-19
*
Dafny:
rustanleino
2010-06-14
*
Dafny: Added two additional heuristics for guessing missing loop decreases c...
rustanleino
2010-06-11
*
Dafny: Another bug fix in SplitExpr, having to do with generic results of fu...
rustanleino
2010-06-09
*
Dafny: Fix type bug in SplitExpr translation.
rustanleino
2010-06-08
*
Boogie:
rustanleino
2010-06-08
*
Dafny:
rustanleino
2010-06-05
*
added lazyinline to the regressions
qadeer
2010-05-28
*
Dafny: Allow < and > for comparisons of datatype values (which then compares ...
rustanleino
2010-05-21
*
Dafny:
rustanleino
2010-05-21
*
Boogie:
rustanleino
2010-05-15
*
Dafny:
rustanleino
2010-05-13
*
Dafny:
rustanleino
2010-05-08
*
Dafny:
rustanleino
2010-05-06
*
Dafny:
rustanleino
2010-05-06
*
First cut of lazy inlining. The option can be turned on by the flag /lazyInl...
qadeer
2010-04-17
*
Dafny: Removed the previous optional curly braces in match expressions (use p...
rustanleino
2010-04-02
*
Dafny:
rustanleino
2010-03-31
*
Dafny: Ensures that function axioms are not being used while their consisten...
rustanleino
2010-03-19
*
Dafny:
rustanleino
2010-03-18
*
Dafny:
rustanleino
2010-03-16
*
Dafny:
rustanleino
2010-03-16
*
Dafny: Added definedness checks for all statements (previously, some were mi...
rustanleino
2010-03-13
*
Added wellformedness checks to method specifications
rustanleino
2010-03-12
*
Dafny:
rustanleino
2010-03-12
[next]