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: re-ran parser generator to include semicolon-less body-less functions/...
Rustan Leino
2011-07-26
*
Merge
Rustan Leino
2011-07-21
|
\
*
|
Dafny: call previous lemma instead of restating it
Rustan Leino
2011-07-21
|
*
Reverting accidental modification in changeset 58325a6e6ed3.
Jason Koenig
2011-07-15
|
*
Fixed regression test failures due to removal of bodiless methods and functions.
Jason Koenig
2011-07-15
|
*
Fixed failing regression tests.
Jason Koenig
2011-07-14
|
*
Merge
Jason Koenig
2011-07-14
|
|
\
|
|
/
|
/
|
|
*
Added multiset from sequence axioms, removed array range RHSs. Fixed issue wi...
Jason Koenig
2011-07-13
*
|
Merge
Rustan Leino
2011-07-11
|
\
\
*
|
|
Dafny: allow constructors only inside classes, removed semi-colons at end of ...
Rustan Leino
2011-07-11
|
|
*
Merge
Jason Koenig
2011-07-11
|
|
|
\
|
|
|
/
|
|
/
|
|
|
*
Added s[..] syntax in anticipation of sequence forming operation. (also updat...
Jason Koenig
2011-07-11
|
*
|
added a new regression
qadeer
2011-07-09
|
*
|
Merge
qadeer
2011-07-09
|
|
\
|
|
*
|
fixed bug in vcgen for bitvectors
qadeer
2011-07-09
|
/
/
|
*
Dafny: Added Euclidean regression test (Verifier only).
Jason Koenig
2011-07-08
|
/
*
Dafny: Fixed bug in call statements where mutability of out parameters was no...
Jason Koenig
2011-07-06
*
Merge
Jason Koenig
2011-07-05
|
\
*
|
Dafny: Updated regression tests to include chaining disjoint operators.
Jason Koenig
2011-07-05
|
*
Merge
Michal Moskal
2011-07-05
|
|
\
|
|
/
|
/
|
|
*
Let = in options be passed down to the runtest.bat
Michal Moskal
2011-06-30
*
|
Added additional test case to modifies on loops tests.
Jason Koenig
2011-06-29
|
/
*
Removed tab characters.
Jason Koenig
2011-06-29
*
Merge
Jason Koenig
2011-06-29
|
\
*
|
Added regression tests for new return statements with parameters.
Jason Koenig
2011-06-29
|
*
Merge
Rustan Leino
2011-06-29
|
|
\
|
|
/
|
/
|
|
*
Dafny: Fixed axioms for Seq#Contains vs. the sequence building functions
Rustan Leino
2011-06-29
*
|
Added regression test file LoopModifies.dfy.
Jason Koenig
2011-06-29
*
|
Added regression test for loop modifies clauses.
Jason Koenig
2011-06-28
*
|
Changed regression test answer for dafny0 to reflect new error messages.
Jason Koenig
2011-06-28
*
|
extra test files
qadeer
2011-06-24
*
|
fixes to z3api
qadeer
2011-06-24
*
|
clean up in z3api
qadeer
2011-06-22
*
|
partial fixes to these regressions
qadeer
2011-06-22
|
/
*
added more regressions to livevars
qadeer
2011-06-14
*
Dafny: added implicit datatype query fields and datatype destructor fields
Rustan Leino
2011-06-05
*
Dafny: translate call statements with fancy LHSs
Rustan Leino
2011-05-31
*
Dafny: Translate general LHSs for var and := (not yet for call, no compilatio...
Rustan Leino
2011-05-30
*
Dafny: changed syntax of havoc statements from "havoc X;" to "X := *;"
Rustan Leino
2011-05-28
*
Dafny: added constructors
Rustan Leino
2011-05-28
*
Merge
Rustan Leino
2011-05-27
|
\
*
|
Dafny:
Rustan Leino
2011-05-27
|
*
Merge
Rustan Leino
2011-05-27
|
|
\
|
|
/
|
/
|
*
|
Dafny: permanently changed the syntax of "datatype" declarations to what prev...
Rustan Leino
2011-05-27
*
|
Dafny: retired "use" statements
Rustan Leino
2011-05-27
*
|
Dafny: added chaining operators
Rustan Leino
2011-05-27
*
|
Dafny:
Rustan Leino
2011-05-26
|
*
Dafny: fixed bug in induction-tactic heuristic (should never pick values whos...
Rustan Leino
2011-05-26
|
*
Dafny: fixed bug (ill-formed Boogie) in translation of "foreach" for sequences
Rustan Leino
2011-05-26
*
|
Dafny: retired the "call" keyword
Rustan Leino
2011-05-26
[next]