| Commit message (Expand) | Author | Age |
... | |
* | | | Fixed lots of bugs having to do with casts, conversions, and address-of | Mike Barnett | 2011-05-03 |
* | | | Merge | Mike Barnett | 2011-05-03 |
|\ \ \ |
|
| * | | | Ignored some new files. | Mike Barnett | 2011-05-03 |
| * | | | Fix creation of valid identifiers for methods with multi-dimensional | Mike Barnett | 2011-05-03 |
| * | | | Trying to fix "boxing", i.e., value type to ref conversions as done in the CLR. | Mike Barnett | 2011-05-03 |
* | | | | bug fixes related to handling of structs, arrays, and assignments | qadeer | 2011-05-02 |
|/ / / |
|
* | | | The decompilation is not guaranteed to get rid of all push statements and pop | Mike Barnett | 2011-04-29 |
* | | | fixed a bug in struct handling | qadeer | 2011-04-28 |
* | | | Use (get-model) Z3 command; quote skolem-ids | Michal Moskal | 2011-04-28 |
* | | | Merge | Mike Barnett | 2011-04-28 |
|\ \ \ |
|
* | | | | Add a method to the Sink that is responsible for creating a Boogie expression | Unknown | 2011-04-28 |
| * | | | Fix parsing of (labels) Z3 response; complain about unrecognized responses there | Michal Moskal | 2011-04-28 |
| * | | | Use :reason-unknown not :last-failure for Z3 in SMT mode; disable SORT_AND_OR... | Michal Moskal | 2011-04-28 |
* | | | | merge | Unknown | 2011-04-27 |
|\ \ \ \
| |/ / /
|/| | | |
|
| * | | | modeling struct creation by default value | Unknown | 2011-04-27 |
| |\ \ \ |
|
* | | | | | Boogie build succeeded, 1 test(s) failed | CodeplexBot | 2011-04-28 |
|/ / / / |
|
| * | | | Model newly constructed structs as a constant DefaultStruct that has axioms that | Unknown | 2011-04-27 |
* | | | | first check in | qadeer | 2011-04-27 |
| * | | | merge changes with shaz's checkin. | Unknown | 2011-04-27 |
|/| | | |
|
| * | | | Trying to get structs supported. | Unknown | 2011-04-27 |
* | | | | fixes to struct translation | qadeer | 2011-04-27 |
* | | | | fixed a bug in ComputeAllLabels | qadeer | 2011-04-27 |
* | | | | Merge | qadeer | 2011-04-27 |
|\| | | |
|
* | | | | fixing problems with struct translation | qadeer | 2011-04-27 |
| * | | | Add translation for conversion expressions, at least between bool and int. | Unknown | 2011-04-26 |
|/ / / |
|
* | | | Merge | qadeer | 2011-04-23 |
|\ \ \ |
|
* | | | | 0. Deleted other heap representations except SplitField and General | qadeer | 2011-04-23 |
| | | * | Dafny: include source location for array types supplied in input | Rustan Leino | 2011-04-22 |
| * | | | Boogie build succeeded, 25 test(s) failed | CodeplexBot | 2011-04-23 |
| | |/
| |/| |
|
* | | | Merge | qadeer | 2011-04-22 |
|\| | |
|
* | | | in the middle of trying to implement structs | qadeer | 2011-04-22 |
| * | | Merge with 1038 | Rustan Leino | 2011-04-22 |
| |\ \ |
|
| * | | | BVD: Smaller initial window (to better fit on a laptop screen) | Rustan Leino | 2011-04-22 |
| * | | | Jennisys: a (failed) attempt at getting a model from which one could generate... | Rustan Leino | 2011-04-22 |
| | * | | Updates for the latest changes in Z3's SMT2 parser | Michal Moskal | 2011-04-22 |
| |/ /
|/| | |
|
* | | | Changed label checking for goto targets in StmtList so that they can be any l... | qadeer | 2011-04-21 |
| * | | Dafny: Fix parsing of if-then-else expressions, and don't require parentheses... | Rustan Leino | 2011-04-21 |
* | | | Added translation for "x is T" expressions. | Unknown | 2011-04-21 |
| * | | Dafny: Alternative (and candidate replacement) syntax for declaring datatypes | Rustan Leino | 2011-04-20 |
|/ / |
|
* / | Dafny: added type "nat" | Rustan Leino | 2011-04-19 |
|/ |
|
* | Automated merge with https://hg01.codeplex.com/boogie | Rustan Leino | 2011-04-16 |
|\ |
|
* | | Boogie build succeeded, 1 test(s) failed | CodeplexBot | 2011-04-16 |
* | | Merge | qadeer | 2011-04-15 |
|\ \ |
|
* | | | modified letvc generation so that the use of control flow function and labels... | qadeer | 2011-04-15 |
| * | | Add "Large font" menu item (for demos) | Michal Moskal | 2011-04-15 |
|/ / |
|
* | | merge | Unknown | 2011-04-14 |
|\ \ |
|
* | | | added reachability information to the VC and used that to support arbitrary a... | Unknown | 2011-04-14 |
| * | | Stratified Inlining: minor bux fix with recording model values | Unknown | 2011-04-14 |
| * | | Dafny: added manual proofs for 5 theorems in Rippling.dfy | Rustan Leino | 2011-04-12 |
|/ / |
|
* | | merging in my changes i committed in 999. | Unknown | 2011-04-12 |
|\ \ |
|