summaryrefslogtreecommitdiff
path: root/Source
Commit message (Expand)AuthorAge
...
* | Dafny: Fixed bug in call statements where mutability of out parameters was no...Gravatar Jason Koenig2011-07-06
* | MergeGravatar Jason Koenig2011-07-05
|\ \
* | | Dafny: Added chaining of disjoint (!!) using transitive chaining convention.Gravatar Jason Koenig2011-07-05
| * | ExtractLoops calls the same code for eliminating unreachable blocks that norm...Gravatar qadeer2011-07-05
| * | Don't send (check-sat) after error limit is reachedGravatar Michal Moskal2011-07-05
| * | MergeGravatar Michal Moskal2011-07-05
| |\ \ | |/ / |/| |
* | | Boogie: New cli option -z3exe:"path-to-z3.exe" allowing specifying path to th...Gravatar Unknown2011-07-05
* | | Added the /noCheating option. (treats assume as assert and drops free.)Gravatar Jason Koenig2011-07-01
| * | Update the RECENT_Z3 #define to include SORT_AND_ORGravatar Michal Moskal2011-06-30
| * | Add /T: option to Z3 to kill it if it exceeds soft timeout by more than 1sGravatar Michal Moskal2011-06-30
| * | Allow : instead of = in optionsGravatar Michal Moskal2011-06-30
| * | SMTLib: Only use (set-logic ...) when requested; quote some more symbolsGravatar Michal Moskal2011-06-30
* | | 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
* | | Refactor. Renamed update statement field and removed unused field in AST.Gravatar Jason Koenig2011-06-30
|/ /
* | 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
* | | 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
* | | | Initial implementation of return statments with parameters.Gravatar Jason Koenig2011-06-29
| |/ / |/| |
* | | Removed development comments.Gravatar Jason Koenig2011-06-29
| |/ |/|
* | MergeGravatar 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
|/ /
* | 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
* | fixes to z3apiGravatar qadeer2011-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
| |/
* | 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
|\|
* | various fixes to port to latest version of Microsoft.Z3.dllGravatar qadeer2011-06-22
| * Dafny: bug fix in generating IsCanonicalBoolBox predicatesGravatar Rustan Leino2011-06-21
|/
* Dafny: better error message when "decreases *" is attempted on a function or ...Gravatar Rustan Leino2011-06-20
* MergeGravatar Rustan Leino2011-06-20
|\
* | Dafny: fixed accidental omission of CaptureState after some assignmentsGravatar Rustan Leino2011-06-16