| Commit message (Expand) | Author | Age |
* | fix for apparent typo in Rewriter.cs | Michael Lowell Roberts | 2015-07-20 |
* | Merge my autoTriggers work into the master branch | Clément Pit--Claudel | 2015-07-17 |
|\ |
|
* | | Register the trigger generator as a a rewriter in the Resolver. | Clément Pit--Claudel | 2015-07-13 |
* | | Make attributes enumerable. | Clément Pit--Claudel | 2015-07-13 |
| * | Fix identifiers in nested match patterns not showing in the IDE bug. Remember | qunyanm | 2015-06-29 |
|/ |
|
* | Fix various bugs in nested match patterns listed in issue #83 | qunyanm | 2015-06-19 |
* | Added {:auto_generated} trigger, which indicates that a declaration was not e... | Rustan Leino | 2015-06-02 |
* | Add an infinite set collection type. | qunyanm | 2015-05-29 |
* | Allow MatchExpr and MatchStmt to have nested patterns. Such as | qunyanm | 2015-05-14 |
* | Fix issue #71. When substitute the forall's variables for those of the | qunyanm | 2015-04-16 |
* | Eliminate redundant checks of newtype and opaque function well-formedness fro... | chrishaw | 2015-04-02 |
* | Fix issue #55 and #64. When performing type argument substitution for function | qunyanm | 2015-03-16 |
* | This changeset changes the default visibility of a function/predicate body ou... | leino | 2015-03-09 |
* | Fixed an encoding bug for newtypes (this fixes Issue #50) | Rustan Leino | 2015-01-27 |
* | Switched use of List(IToken) in UserDefinedType to NameSegment/ExprDotName, s... | leino | 2015-01-23 |
* | Fixed bug in opaque functions with type parameters | leino | 2015-01-07 |
* | Language change: All functions and methods declared lexically outside any cla... | leino | 2014-12-12 |
* | Finished up refactoring of the new name segment parsing, AST, and resolution. | leino | 2014-12-07 |
* | Snapshot, to be continued | leino | 2014-12-02 |
* | Make autoreqs of free requires not free | Bryan Parno | 2014-10-27 |
* | Allow autoReq in methods to generate auto-requirements on requires | Bryan Parno | 2014-10-27 |
* | Don't process opaque functions more than once when generating auto-reqs | Bryan Parno | 2014-10-27 |
* | Fix fixup to opaque-function revealer to deal with zero-argument lemmas | Bryan Parno | 2014-10-27 |
* | Fix autoreq handling of quantifiers | Bryan Parno | 2014-10-27 |
* | Added an attribute :timeLimitMultiplier for setting relative time outs. | Bryan Parno | 2014-10-27 |
* | Add an option to allow automatically generated requirements to be printed | Bryan Parno | 2014-10-27 |
* | Added types "char" and "string" (the latter being a synonym for "seq<char>"). | leino | 2014-10-20 |
* | Merge | Dan Rosén | 2014-08-11 |
|\ |
|
* | | Add higher-order-functions and some other goodies | Dan Rosén | 2014-08-11 |
| * | Fixed bug Issue 37: expand type synonyms in more (hopefully all) places in th... | leino | 2014-08-02 |
|/ |
|
* | Make reveal axioms from opaque functions quantify over layers | Dan Rosén | 2014-07-10 |
* | Merge | Rustan Leino | 2014-07-08 |
|\ |
|
* | | Implemented compilation of the int<->real conversions, and changed the resolu... | Rustan Leino | 2014-07-08 |
| * | New logical encoding of types with Is and IsAlloc | Dan Rosén | 2014-07-07 |
|/ |
|
* | Refactored code for dealing with SCCs in the call graph. | Rustan Leino | 2014-02-24 |
* | Removed some blank lines at the end of hover texts. | Rustan Leino | 2014-02-06 |
* | Produce hover text for many of the refinement omissions (i.e., "..." and the ... | Rustan Leino | 2014-01-31 |
* | Fix a bug in the interaction between opaque and generics | Bryan Parno | 2014-01-23 |
* | Added a missing autoReq resolution step | Bryan Parno | 2014-01-14 |
* | Improve autoReq's interactions with opaque | Bryan Parno | 2014-01-13 |
* | Small fix to the order in which AutoReq adds its requirements. | Bryan Parno | 2014-01-13 |
* | Manually adjusted merge | Rustan Leino | 2014-01-08 |
* | Add autoReq support for matches. | Bryan Parno | 2014-01-08 |
* | Added support for automatic generation of function requirements via the :auto... | Bryan Parno | 2014-01-08 |
* | Added an .EndTok for every statement. (Note, in some places, especially in V... | Rustan Leino | 2013-12-19 |
* | Don't expand {:opaque} for inherited functions. (Note, more design is still ... | Rustan Leino | 2013-12-17 |
* | Add support for the :axiom attribute for ghost methods. | Bryan Parno | 2013-12-13 |
* | Added support for opaque function definitions, indicated via the {:opaque} at... | Bryan Parno | 2013-12-13 |
* | When inlining the body of a predicate (in a proof obligation--via TrSplitExpr), | Rustan Leino | 2013-04-24 |
* | Disallow allocations in ghost contexts | Rustan Leino | 2013-03-06 |