summaryrefslogtreecommitdiff
path: root/Source
Commit message (Expand)AuthorAge
* Updated several project files.Gravatar wuestholz2013-05-21
* In Visual Studio interface, highlight variable definitions of let expressionsGravatar Rustan Leino2013-05-12
* Made the semi-colon after "type" and "module" declarations optional.Gravatar Rustan Leino2013-05-10
* Fix bug in substitution into let-such-that expressionsGravatar Rustan Leino2013-05-10
* When inlining the body of a predicate (in a proof obligation--via TrSplitExpr),Gravatar Rustan Leino2013-04-24
* Fixed (completeness) bug in translation of automatic induction--previously, t...Gravatar Rustan Leino2013-04-19
* Make semi-colon after datatype/codatatype declaration optional (in the future...Gravatar Rustan Leino2013-04-19
* Deleted a non-keywordGravatar Rustan Leino2013-04-04
* Refactored some resolution stages to make use of VisitorsGravatar Rustan Leino2013-04-02
* Moved resolution of BinaryExpr.ResolveOp until the CheckTypeInference phase, ...Gravatar Rustan Leino2013-04-01
* Fixed compilation of assign-such-that for the multi-variable case where some ...Gravatar Rustan Leino2013-03-29
* The "choose" statement, hacky and specialized as it was, is now gone. Use th...Gravatar Rustan Leino2013-03-27
* Replaced SuperSetBoundedPool by SubSetBoundedPool, which is much more useful ...Gravatar Rustan Leino2013-03-27
* Compilation of (many common) assign-such-that statements.Gravatar Rustan Leino2013-03-26
* Suppress compiler warnings about unreferenced labels (I hope all .NET platfor...Gravatar Rustan Leino2013-03-26
* Type-inference support for cardinality operatorGravatar Rustan Leino2013-03-26
* MergeGravatar Rustan Leino2013-03-25
|\
* | Beefed up assign/let-such-that to generate possible witnesses for set/multise...Gravatar Rustan Leino2013-03-25
| * First take on set, multiset and map cardinality.Gravatar Nadia Polikarpova2013-03-22
|/
* Minor code cleanup.Gravatar Nadia Polikarpova2013-03-21
* Bumped version to 1.6.3.00320, to appear on rise4funGravatar Rustan Leino2013-03-20
* MergeGravatar Nadia Polikarpova2013-03-20
|\
* | Finished support for ==# in calc, changed Paulson example to use it.Gravatar Nadia Polikarpova2013-03-20
| * Added multiset update.Gravatar Nadia Polikarpova2013-03-20
| * Added multiset indexing.Gravatar Nadia Polikarpova2013-03-20
|/
* Added some data structure to support ==# in calculations.Gravatar Nadia Polikarpova2013-03-20
* Updated version to 1.6.2.00318Gravatar Rustan Leino2013-03-18
* MergeGravatar Rustan Leino2013-03-15
|\
* | Fixed yield statement to process its arguments.Gravatar Rustan Leino2013-03-15
| * Added explies support to calculations.Gravatar Nadia Polikarpova2013-03-15
| * Added the <== operator.Gravatar Nadia Polikarpova2013-03-14
|/
* Bumped version to 1.6.1, to be released as a binary and on rise4fun.Gravatar Rustan Leino2013-03-10
* MergeGravatar Rustan Leino2013-03-06
|\
| * Disallow allocations in ghost contextsGravatar Rustan Leino2013-03-06
* | Set .Result field of calc even if there are 0 linesGravatar Rustan Leino2013-03-06
|/
* Renamed "parallel" statement to "forall" statement, and made the parentheses ...Gravatar Rustan Leino2013-03-06
* New well-formedness checks for calculations (no cascading).Gravatar Nadia Polikarpova2013-03-05
* Added side-effects and control-flow checks in hints.Gravatar Nadia Polikarpova2013-03-05
* Fixed crash in translator, having to do with recursive co-predicates.Gravatar Rustan Leino2013-03-04
* MergeGravatar Rustan Leino2013-02-21
|\
| * MergeGravatar Rustan Leino2013-02-21
| |\
* | | Pretty print the new parentheses-less "if" and "while" statements as such.Gravatar Rustan Leino2013-02-21
* | | Fixed let-such-that and if-then-else encodings so that they will pass the sub...Gravatar Rustan Leino2013-02-21
* | | Added Equals method on TypeGravatar Rustan Leino2013-02-20
| |/ |/|
* | Support for paren-free guards in if and while statements.Gravatar Nadia Polikarpova2013-02-15
| * Improved source location reported for two resolution errorsGravatar Rustan Leino2013-02-14
|/
* Solved some contract violation issues.Gravatar Nadia Polikarpova2013-02-14
* Manual merge.Gravatar Nadia Polikarpova2013-02-13
* MergeGravatar Nadia Polikarpova2013-02-13
|\
| * Frame expressions are now checked to be well formed.Gravatar Rustan Leino2013-02-13