summaryrefslogtreecommitdiff
path: root/Source/Dafny/DafnyPipeline.csproj
Commit message (Collapse)AuthorAge
* merged IronDafny updates. two unit tests related to traits do not pass if ↵Gravatar Michael Lowell Roberts2015-09-21
| | | | ENABLE_IRONDAFNY is defined but this isn't critical and will be addressed shortly.
* Small cleanups, fixes, and refactoringsGravatar Clément Pit--Claudel2015-08-18
| | | | | In particular, start detecting loops between terms that don't look like each other at the Dafny level, such as {a[x]} and {x in a} (when a is a multiset)
* Draft out a more advanced version of trigger generationGravatar Clément Pit--Claudel2015-08-19
| | | | This new version will include a cleaner pipeline, and trigger splitting.
* Refactor the error reporting codeGravatar Clément Pit--Claudel2015-08-18
| | | | | The new error reporting system has a simpler interface, isn't tied to the resolver, and contains error source information.
* Register the trigger generator as a a rewriter in the Resolver.Gravatar Clément Pit--Claudel2015-07-13
|
* Add a compatibility layer over BigInteger.ParseGravatar Clément Pit--Claudel2015-06-07
| | | | | | | Mono currently does not implement support for BigInteger.Parse, so use Int64 if possible, and throw the same error as was previously returned otherwise. This is not too much of a problem in practice, because most of the integers that we actually come across in real-life source files seem to fit in an Int64.
* DafnyExtension: Did some refactoring and worked towards integrating the ↵Gravatar wuestholz2013-07-26
| | | | Dafny menu more tightly.
* DafnyExtension: Cleaned up some references and disabled non-functional ↵Gravatar wuestholz2013-06-07
| | | | support for VS 2010.
* Updated several project files.Gravatar wuestholz2013-05-21
| | | | | Note that the 'boogie' directory is expected to be a sibling of the 'dafny' directory.
* Put all sources under \Source directoryGravatar Rustan Leino2012-10-04
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-03 21:52:05 +0000