summaryrefslogtreecommitdiff
path: root/Source
Commit message (Collapse)AuthorAge
* Fix type inference bug in data rank comparison when one side can be a TypeVarGravatar Dan Rosén2014-08-19
|
* Consider lambdas literals + create literal axioms when an argument is a functionGravatar Dan Rosén2014-08-18
|
* Fix type equality for UserDefinedTypesGravatar Dan Rosén2014-08-15
|
* Refactor resolver, and really allow reads to take fields of type A -> set<obj>Gravatar Dan Rosén2014-08-15
| | | | twoState and codeContext is moved to a new class ResolveOpts
* Fix a performance issue regarding requires for top level function handlesGravatar Dan Rosén2014-08-14
|
* Make arrow types not look like reference types for the resolverGravatar Dan Rosén2014-08-14
|
* Optimise ApplyExpr to FunctionCallExpr when possible in translatorGravatar Dan Rosén2014-08-14
|
* Generate function handle requires for functions without a bodyGravatar Dan Rosén2014-08-14
|
* Reword error message for type error in lambda requires clauseGravatar Dan Rosén2014-08-14
|
* Fix bug in type substitution for type variablesGravatar Dan Rosén2014-08-14
|
* Allow reads to take fields of type A -> set<object>Gravatar Dan Rosén2014-08-14
|
* Refactor: Change ApplyExpr's Receiver to FunctionGravatar Dan Rosén2014-08-14
|
* Re-included lost calls to CheckEqualityTypes_TypeGravatar leino2014-08-13
| | | | Modified syntax in some tests, since predicates now require parentheses (without parentheses refers to a predicate, not an application of the predicate)
* MergeGravatar leino2014-08-13
|\
* | Check for proper use of equality-supporting types also in local variables ↵Gravatar leino2014-08-13
| | | | | | | | and forall statements, and more expressions
| * Addressed CodeContract complaint about purityGravatar Rustan Leino2014-08-12
| |
| * Forget the extra copy of DafnyRuntime.cs that gets copied into DafnyExtensionGravatar Rustan Leino2014-08-12
| |
| * Compile lambda functions and apply expressions, and change let expr compilationGravatar Dan Rosén2014-08-12
| |
| * MergeGravatar Dan Rosén2014-08-11
| |\ | |/ |/|
| * Add higher-order-functions and some other goodiesGravatar Dan Rosén2014-08-11
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | * The reads clause now needs to be self framing. * The requires clause now needs to be framed by the reads clause. * There are one-shot lambdas, with a single arrow, but they will probably be removed. * There is a {:heapQuantifier} attribute to quantifiers, but they will probably be removed. * Add smart handling of type variables * Add < and > for datatype & type parameter
* | Resolved further merge issuesGravatar leino2014-08-05
| |
* | MergeGravatar leino2014-08-02
|\ \
* | | Fixed bug Issue 37: expand type synonyms in more (hopefully all) places in ↵Gravatar leino2014-08-02
| |/ |/| | | | | the resolver and translator
| * - fixed a bug in inheriting members from a traitGravatar Reza Ahmadi2014-07-20
| | | | | | | | | | | | | | => ResolvedClass in userdefinedtypes used to be null-> fixed - checking only bodyless methods and functions to make sure they have been implemented in the child class - added one more test
| * - fixed an issue regarding including ghost functions in the compiled interfaceGravatar Reza Ahmadi2014-07-20
| | | | | | | | - added one more test
| * added trait feature:Gravatar Reza Ahmadi2014-07-18
|/ | | | | | -possibility to declare traits in Dafny -possibility to extend a class by a trait -possibility to override body-less methods
* Fixed build break from recent changeGravatar leino2014-07-15
|
* Renamed "arbitrary type" to "opaque type"Gravatar Rustan Leino2014-07-15
|
* Allow an arbitrary-type to take type parametersGravatar Rustan Leino2014-07-15
|
* Support for type synonyms in refinementsGravatar Rustan Leino2014-07-14
| | | | Started allowing arbitrary types to have type parameters
* MergeGravatar Rustan Leino2014-07-11
|\
* | Added type synonyms. (No support yet for these in refinements.)Gravatar Rustan Leino2014-07-11
| |
| * Check that type arguments to map display expressions are fully resolvedGravatar Dan Rosén2014-07-11
| | | | | | | | Also add a test case for the different display expressions.
| * Don't assume can calls for quantifiersGravatar Dan Rosén2014-07-11
|/ | | | Fixes regression in Cyclic in Floyd Cycle Detection.
* Make reveal axioms from opaque functions quantify over layersGravatar Dan Rosén2014-07-10
|
* Worked on the more advanced verification result caching.Gravatar wuestholz2014-07-10
|
* Worked on the more advanced verification result caching.Gravatar wuestholz2014-07-10
|
* MergeGravatar Rustan Leino2014-07-09
|\
* | Ignore checked-only and free-only split expressions in places where they ↵Gravatar Rustan Leino2014-07-09
| | | | | | | | | | | | "don't belong". (This currently breaks dafny0/FunctionSpecifications.dfy and cloudmake/CloudMake-CachedBuilds.dfy, but a fix for those is underway.)
| * Worked on the more advanced verification result caching.Gravatar wuestholz2014-07-09
|/
* Build VS Extension for both VS 2012 and VS 2013.Gravatar Rustan Leino2014-07-08
| | | | Currently builds only in VS 2012. To build in VS 2013, change MinimumVisualStudioVersion from 11.0 to 12.0 in these two .csproj files.
* Further resolved merge conflictsGravatar Rustan Leino2014-07-08
|
* MergeGravatar Rustan Leino2014-07-08
|\
* | Implemented compilation of the int<->real conversions, and changed the ↵Gravatar Rustan Leino2014-07-08
| | | | | | | | | | | | resolution and verification implementations of these. Changed FreshExpr to be a UnaryExpr, and also introduced the UnaryOpExpr subclass.
| * MergeGravatar Dan Rosén2014-07-07
| |\
| * | New logical encoding of types with Is and IsAllocGravatar Dan Rosén2014-07-07
| | |
| | * MergeGravatar leino2014-07-03
| | |\
| | * | Translate CanCallAssumption with the same fuel value as in the body of the ↵Gravatar leino2014-07-03
| | | | | | | | | | | | | | | | function definition axiom (which prevents some matching loops)
| | | * Changed "dummy" checksums to "stable" and added more tests for the ↵Gravatar wuestholz2014-07-03
| | | | | | | | | | | | | | | | verification result caching.
* | | | Fixed a crash in the translation of fresh(seq<T>).Gravatar Rustan Leino2014-07-02
| |_|/ |/| |
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-05 02:23:22 +0000