Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Dafny: removed support for assigning to an array-range (that is, an ↵ | 2011-10-26 | |
| | | | | assignment statement where the LHS has the form a[lo..hi]) | ||
* | Merge | 2011-10-26 | |
|\ | |||
* | | Dafny: Commented out SnapshotableTrees.Node.FunctionalInsert while ↵ | 2011-10-26 | |
| | | | | | | | | performance issues with the prover and going into SMTLib2 mode are being investigated. | ||
| * | Added batch script to run tests for datatypes tests. | 2011-10-26 | |
| | | |||
* | | Dafny: implemented compilation of parallel statements | 2011-10-25 | |
| | | | | | | | | Dafny: beefed up resolution of parallel statements | ||
* | | Dafny: check subrange restriction in parallel Assign statement | 2011-10-24 | |
|/ | | | | | Dafny: verify parallel Call statement Dafny: fixed some bugs: handle all cases of comprehension expressions in resolver's UsesSpecFeatures, check target of method calls to be non-null (duh!) | ||
* | Dafny: continued translation of "parallel" statements (Assign and Proof ↵ | 2011-10-24 | |
| | | | | | | | forms are mostly there, Call is missing and so is compilation) Dafny: included some test cases for the "parallel" statement Dafny: starting changing old "foreach" statements to the new "parallel" statement | ||
* | Dafny: added translation of Assign case of the parallel statement | 2011-10-22 | |
| | | | | Dafny: discovered and fixed bug in no-overlap check of multi-dimensional array update, and changed previously incorrect MatrixFun.dfy test case (the new version is also a more efficient program) | ||
* | Dafny: changed triggers (which are never really used, anyhow) from having a ↵ | 2011-10-21 | |
| | | | | | | | special syntactic form to being just an attribute Dafny: added "parallel" statement (so far, only parsing and resolving) Dafny: allow types on bound variables in "match" expressions/statements (there's never any incentive to list them explicitly in the program text, but it nevertheless seemed silly to forbid them) | ||
* | Dafny: fixed performance-buggy translation of exists, and also added some ↵ | 2011-10-19 | |
| | | | | other features in SplitExpr (such as induction on existential quantifiers) | ||
* | Added a push+pop+unsat-core interface to SMTLib (for stratified inlining only) | 2011-10-19 | |
| | |||
* | added houdini to regression | 2011-10-17 | |
| | | | | changed houdini so that the initial worklist is created by queueing downstream Sccs first | ||
* | Dafny: added COST Verification Competition challenge programs to test suite | 2011-10-07 | |
| | |||
* | added membership tests | 2011-10-05 | |
| | |||
* | implementing datatypes | 2011-10-05 | |
| | |||
* | Merge | 2011-09-30 | |
|\ | |||
* | | Dafny: Updated snapshotable tree to remove IsReadonly precondition for ↵ | 2011-09-30 | |
| | | | | | | | | CreateIterator. | ||
* | | Dafny: fixed bug in translator when LHS of a call was an array element or a nat | 2011-09-30 | |
| | | |||
| * | Merge | 2011-09-30 | |
| |\ | |||
| * | | bug fix in houdini | 2011-09-30 | |
| | | | | | | | | | | | | also fixed runtest.bat and Answer | ||
| | * | Dafny: Fixed the 'Answer' file for test 'dafny2'. | 2011-09-30 | |
| |/ | |||
* / | Dafny: beautification in one test case, and fixed an Answer file | 2011-09-29 | |
|/ | |||
* | Dafny: Added TreeBarrier as a test case | 2011-09-29 | |
| | |||
* | Merge | 2011-09-28 | |
|\ | |||
| * | Updated the ANSWER file for 'test15'. | 2011-09-27 | |
| | | |||
* | | Merge | 2011-09-17 | |
|\ \ | |||
| | * | Dafny: Added support for attributes on methods and constructors. | 2011-09-16 | |
| |/ | |||
| * | Added "free call" statements that don't check the precondition in the caller. | 2011-09-14 | |
| | | |||
* | | Dafny: added Snapshotable Trees example | 2011-09-11 | |
| | | |||
* | | Dafny: added Flatten example to test suite | 2011-09-11 | |
|/ | |||
* | Merge | 2011-09-08 | |
|\ | |||
* | | Dafny: fixed parsing bug with "!in" | 2011-09-08 | |
| | | | | | | | | | | Dafny: fixed translation bug with missing match cases (where the constructor has some parameters) Dafny: fixed translation bug where the program had forward references to members of a datatype | ||
| * | Support for irreducible graphs (with extractLoops) | 2011-08-24 | |
|/ | |||
* | Dafny: updated Answer file from recent test additions | 2011-08-22 | |
| | |||
* | Dafny: updated test files (will soon update Answer files as well) | 2011-08-22 | |
| | |||
* | Merge | 2011-08-18 | |
|\ | |||
* | | Dafny: fixed bug in looking at the arguments of the :induction attribute | 2011-08-18 | |
| | | |||
| * | Dafny: Fixed a bug in the printer that led to a stack overflow. | 2011-08-11 | |
| | | |||
| * | Jennisys: started to work on synthesizing some methods. So far, only | 2011-08-10 | |
| | | | | | | | | | | | | infrastructural things have been implemented, like handling return parameters, generating different "fresh" spec for methods than for constructors, adding "Valid()" to method preconditions. | ||
| * | further changes for making houdini work | 2011-08-04 | |
|/ | |||
* | Dafny: added reverse*reverse=id example to test suite | 2011-08-04 | |
| | |||
* | Dafny: fix resolution crash (using multi-dimensional arrays in loop alternative) | 2011-08-03 | |
| | |||
* | Dafny: re-ran parser generator to include semicolon-less body-less ↵ | 2011-07-26 | |
| | | | | functions/methods, and updated some test files accordingly (compare with changesets 1429 and 1366) | ||
* | Merge | 2011-07-21 | |
|\ | |||
* | | Dafny: call previous lemma instead of restating it | 2011-07-21 | |
| | | |||
| * | Reverting accidental modification in changeset 58325a6e6ed3. | 2011-07-15 | |
| | | |||
| * | Fixed regression test failures due to removal of bodiless methods and functions. | 2011-07-15 | |
| | | |||
| * | Fixed failing regression tests. | 2011-07-14 | |
| | | |||
| * | Merge | 2011-07-14 | |
| |\ | |/ |/| | |||
| * | Added multiset from sequence axioms, removed array range RHSs. Fixed issue ↵ | 2011-07-13 | |
| | | | | | | | | with duplicate array.Length functions in generated Boogie file. |