summaryrefslogtreecommitdiff
Commit message (Expand)AuthorAge
* Added option to force Dafny compilation, even if verification fails.Gravatar Jason Koenig2011-06-30
* Refactored update statement resolution to its own method.Gravatar Jason Koenig2011-06-30
* MergeGravatar Jason Koenig2011-06-30
|\
* | Refactor. Renamed update statement field and removed unused field in AST.Gravatar Jason Koenig2011-06-30
| * Boogie build succeededGravatar CodeplexBot2011-06-30
* | Added additional test case to modifies on loops tests.Gravatar Jason Koenig2011-06-29
|/
* Removed tab characters.Gravatar Jason Koenig2011-06-29
* MergeGravatar Jason Koenig2011-06-29
|\
* | Added returns with parameters to printer.Gravatar Jason Koenig2011-06-29
* | Fixed bug in compiler relating to returns with parameters.Gravatar Jason Koenig2011-06-29
* | Added regression tests for new return statements with parameters.Gravatar Jason Koenig2011-06-29
* | Stable implementation of return statements with parameters.Gravatar Jason Koenig2011-06-29
* | Made Receiver mutable, as this cannot be linked properly by the parser.Gravatar Jason Koenig2011-06-29
| * MergeGravatar Rustan Leino2011-06-29
| |\
| * | Boogie: use (WEIGHT 0) with the select-of-store axiomsGravatar Rustan Leino2011-06-29
| * | Dafny: Fixed axioms for Seq#Contains vs. the sequence building functionsGravatar Rustan Leino2011-06-29
* | | Initial implementation of return statments with parameters.Gravatar Jason Koenig2011-06-29
| |/ |/|
* | Removed development comments.Gravatar Jason Koenig2011-06-29
* | MergeGravatar Jason Koenig2011-06-29
|\ \
* | | Added regression test file LoopModifies.dfy.Gravatar Jason Koenig2011-06-29
| * | Boogie build succeeded, 1 test(s) failedGravatar CodeplexBot2011-06-29
|/ /
* | MergeGravatar Jason Koenig2011-06-28
|\ \
* | | Added regression test for loop modifies clauses.Gravatar Jason Koenig2011-06-28
* | | Changed regression test answer for dafny0 to reflect new error messages.Gravatar Jason Koenig2011-06-28
* | | Initial modifies on loops implementation. Still some errors remaining.Gravatar Jason Koenig2011-06-28
| * | ported all the counterexample code to Michal's new Model class; the goal is t...Gravatar Unknown2011-06-27
|/ /
* | Boogie build succeededGravatar CodeplexBot2011-06-27
* | Fixed non-incremental option of stratified inliningGravatar Unknown2011-06-27
* | FindLeastToVerify: accept multiple proceduresGravatar Unknown2011-06-26
* | Call PostOrderVisitIterative by defaultGravatar Unknown2011-06-26
* | Added an iterative version of PostOrderVisit (but it is not called)Gravatar Unknown2011-06-26
* | Avoid restarting the theorem prover for stratified inlining because itGravatar Unknown2011-06-25
* | early clearing of live variables and incarnation mapsGravatar qadeer2011-06-24
* | further refactoringGravatar qadeer2011-06-24
* | MergeGravatar qadeer2011-06-24
|\ \
* | | extra test filesGravatar qadeer2011-06-24
* | | fixes to z3apiGravatar qadeer2011-06-24
| * | Boogie build succeededGravatar CodeplexBot2011-06-24
|/ /
* | MergeGravatar qadeer2011-06-23
|\ \
* | | implementation of iterative LetVCGravatar qadeer2011-06-23
| * | MergeGravatar Jason Koenig2011-06-23
| |\ \
| * | | Added loop modifies clause syntax.Gravatar Jason Koenig2011-06-23
| | |/ | |/|
* | | MergeGravatar qadeer2011-06-23
|\ \ \ | | |/ | |/|
* | | bug fix in translation of dispatch continuationGravatar qadeer2011-06-23
| * | Didn't intend to include Z3api by defaultGravatar Unknown2011-06-23
| * | Bug fix for trace generation with extractLoop optionGravatar Unknown2011-06-23
| |\ \ | |/ / |/| |
| * | Bug fix for trace generation with extractLoop optionGravatar Unknown2011-06-23
* | | clean up in z3apiGravatar qadeer2011-06-22
|/ /
* | MergeGravatar qadeer2011-06-22
|\|
* | partial fixes to these regressionsGravatar qadeer2011-06-22