summaryrefslogtreecommitdiff
Commit message (Expand)AuthorAge
* MergeGravatar Jason Koenig2011-07-06
|\
* | Dafny: Fixed bug in call statements where mutability of out parameters was no...Gravatar Jason Koenig2011-07-06
| * MergeGravatar Unknown2011-07-06
| |\ | |/ |/|
| * - implemented some sorts of symbolic evaluation of expressionsGravatar Unknown2011-07-06
| * - implemented synthesis of some simple constructors with parametersGravatar Unknown2011-07-05
* | Dafny: Updated regression tests to include chaining disjoint operators.Gravatar Jason Koenig2011-07-05
* | Dafny: Added chaining of disjoint (!!) using transitive chaining convention.Gravatar Jason Koenig2011-07-05
| * added some doc commentsGravatar Unknown2011-07-03
| * - when analyzing a constructor, repeated "assume <inv>" statement explicitlyGravatar Unknown2011-07-02
| * - generates "Valid()" for preconditionsGravatar Unknown2011-07-01
| * - removed the "Constructor" discriminator from type Member, and added aGravatar Unknown2011-07-01
* | Added the /noCheating option. (treats assume as assert and drops free.)Gravatar Jason Koenig2011-07-01
* | 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
* | 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
| |\ \
| * | | 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
* | | Added regression test file LoopModifies.dfy.Gravatar Jason Koenig2011-06-29
* | | 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
| | * fixed some minor bugs:Gravatar Unknown2011-06-24
| | * - implemented code generation from a synthesis solution (simple fieldGravatar Unknown2011-06-24
| | * - implemented reading models from a BVD model fileGravatar Unknown2011-06-24
* | | Added loop modifies clause syntax.Gravatar Jason Koenig2011-06-23
|/ /
* | 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
|\ \
| | * refactored the Analyzer code so that it generates a separate Dafny file for eachGravatar Unknown2011-06-20
* | | Dafny: removed deprecated "call" and "use" keywords from syntax highlightersGravatar Rustan Leino2011-06-20
| | * - changed the grammar to allow for arbitrary post-condition expressionsGravatar Unknown2011-06-19
| * | Dafny: fixed accidental omission of CaptureState after some assignmentsGravatar Rustan Leino2011-06-16
| |/
| * Dafny: added implicit datatype query fields and datatype destructor fieldsGravatar Rustan Leino2011-06-05
|/
* Dafny: fixed soundness problem with HeapSucc axiomGravatar Rustan Leino2011-06-01
* Dafny: compiler fixesGravatar Rustan Leino2011-05-31
* Dafny: compile multi-assignments, compile calls with more general LHSsGravatar Rustan Leino2011-05-31
* Dafny: translate call statements with fancy LHSsGravatar Rustan Leino2011-05-31
* Dafny: Translate general LHSs for var and := (not yet for call, no compilatio...Gravatar Rustan Leino2011-05-30
* Dafny: changed syntax of havoc statements from "havoc X;" to "X := *;"Gravatar Rustan Leino2011-05-28
* Dafny: added constructorsGravatar Rustan Leino2011-05-28
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-03 01:54:03 +0000