Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Use SMT2 syntax for sign_extend | 2011-08-22 | |
| | |||
* | reverting irreducible handling temporarily | 2011-08-21 | |
|\ | |||
* \ | Merge | 2011-08-20 | |
|\ \ | |||
* | | | added code to handle irreducible graphs | 2011-08-20 | |
| | | | |||
| * | | Merge | 2011-08-18 | |
| |\ \ | |/ / |/| | | |||
| * | | Dafny: fixed bug in looking at the arguments of the :induction attribute | 2011-08-18 | |
| | | | |||
* | | | minor refactoring | 2011-08-17 | |
| | | | |||
* | | | deleted lazyinlining option 2 and 3 | 2011-08-17 | |
| | | | | | | | | | | | | fixed proc copy bounding | ||
* | | | Merge | 2011-08-16 | |
|\ \ \ | |||
| * | | | Dafny: Fixed a bug in the printer that led to a stack overflow. | 2011-08-11 | |
| | | | | |||
| * | | | Added "procedure-copy bounding" for lazy inlining | 2011-08-10 | |
| | | | | |||
| * | | | further updates to bit vector analysis | 2011-08-09 | |
| | | | | |||
| * | | | more changes to bitvector analysis | 2011-08-09 | |
| | | | | |||
| * | | | another bug fix in bct | 2011-08-08 | |
| | | | | |||
| * | | | added a new file and fixed a bug in bct | 2011-08-08 | |
| | | | | |||
| * | | | various changes to boogie for bitvector analysis and bctprovider | 2011-08-08 | |
| | | | | |||
* | | | | Fix null-ref | 2011-08-07 | |
| | | | | |||
| * | | | further updates to bctprovider | 2011-08-05 | |
| | | | | |||
| * | | | first add | 2011-08-05 | |
| | | | | |||
| * | | | fixed the key signing problem with houdini | 2011-08-05 | |
| | | | | | | | | | | | | | | | | started adding bct provider | ||
| * | | | further changes for making houdini work | 2011-08-04 | |
| | | | | |||
| * | | | Merge | 2011-08-04 | |
| |\| | | |||
| * | | | cleaned up houdini options | 2011-08-04 | |
| | | | | |||
| | * | | Merge | 2011-08-04 | |
| | |\ \ | | |/ / | |/| | | |||
| * | | | full port of houdini project | 2011-08-04 | |
| | | | | |||
| * | | | Merge | 2011-08-03 | |
| |\ \ \ | |/ / / |/| | | | |||
| * | | | ported Houdini to C#, added Houdini project to the Boogie solution | 2011-08-03 | |
|/ / / | |||
| * / | Dafny: fix resolution crash (using multi-dimensional arrays in loop alternative) | 2011-08-03 | |
|/ / | |||
* | | release build should not have z3api being built | 2011-07-28 | |
| | | |||
* | | 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-15 | |
|\ \ | |||
* | | | Added compilation support for multisets and sequences from arrays. | 2011-07-15 | |
| | | | |||
| * | | Updated the Parser.cs and Scanner.cs files in Boogie and Dafny and removed ↵ | 2011-07-15 | |
| | | | | | | | | | | | | some trailing whitespace. | ||
* | | | Merge | 2011-07-14 | |
|\| | | |||
* | | | Fixed bug where wellformedness for E in multiset(E) was checked in the "old" ↵ | 2011-07-14 | |
| | | | | | | | | | | | | context. | ||
* | | | Added multiset from sequence axioms, removed array range RHSs. Fixed issue ↵ | 2011-07-13 | |
| | | | | | | | | | | | | with duplicate array.Length functions in generated Boogie file. | ||
| * | | Another test checkin | 2011-07-12 | |
| | | | |||
* | | | Fixed printing of multisets. | 2011-07-11 | |
| | | | |||
* | | | Multiset forming operators added. | 2011-07-11 | |
| | | | |||
| * | | Merge | 2011-07-11 | |
| |\ \ | |||
| * | | | Dafny: allow constructors only inside classes, removed semi-colons at end of ↵ | 2011-07-11 | |
| | | | | | | | | | | | | | | | | body-less functions/methods | ||
* | | | | Merge | 2011-07-11 | |
|\ \ \ \ | |||
* \ \ \ \ | Merge | 2011-07-11 | |
|\ \ \ \ \ | |||
* | | | | | | Added s[..] syntax in anticipation of sequence forming operation. (also ↵ | 2011-07-11 | |
| | | | | | | | | | | | | | | | | | | | | | | | | updated regression tests.) | ||
| | | | * | | - fixed a bug in DafnyModelUtils.fs (reading set values from models) | 2011-07-11 | |
| | |_|/ / | |/| | | | | | | | | | | | | | | | | | | - changed Dafny so that it returns an exit code - changed CheckDafnyProgram so that it checks Dafny exit code as well | ||
| | * | | | Partial implementation of multisets. | 2011-07-11 | |
| |/ / / |/| | | | |||
| * | | | async call return value is either int or bv32 | 2011-07-09 | |
| | | | | |||
| * | | | Merge | 2011-07-09 | |
| |\ \ \ | |/ / / |/| | | | |||
| * | | | fixed bug in vcgen for bitvectors | 2011-07-09 | |
| |/ / | |||
* / / | Dafny: Dafny now uses the Euclidean definition of division. (Verifier and ↵ | 2011-07-08 | |
|/ / | | | | | | | runtime.) |