summaryrefslogtreecommitdiff
Commit message (Expand)AuthorAge
* Merge my autoTriggers work into the master branchGravatar Clément Pit--Claudel2015-07-17
|\
* | Clean up new trigger declarations in Translator.csGravatar Clément Pit--Claudel2015-07-17
* | Clean up runTests after 2015/07/17 meetingGravatar Clément Pit--Claudel2015-07-17
* | Enable autoTriggers in LitTriggers and SeqFromArrayGravatar Clément Pit--Claudel2015-07-17
* | Add /autoTriggers to TriggerInPredicate's RUN specificationGravatar Clément Pit--Claudel2015-07-17
* | Fix column numbers in warning and info messagesGravatar Clément Pit--Claudel2015-07-16
* | Clean up a few thing and set proper defaults before mergingGravatar Clément Pit--Claudel2015-07-16
| * MergeGravatar Rustan Leino2015-07-16
| |\
| | * Fixed bugs in the parsing of explicit type arguments.Gravatar Rustan Leino2015-07-16
* | | Force IsTriggerKiller to return false when /autoTriggers is offGravatar Clément Pit--Claudel2015-07-16
* | | Use MapConcat instead of String.Join in TriggerGeneratorGravatar Clément Pit--Claudel2015-07-16
* | | Minor fixes in .expect filesGravatar Clément Pit--Claudel2015-07-16
* | | Strip literals from triggersGravatar Clément Pit--Claudel2015-07-16
| * | Add license text and Linux setup notesGravatar Clément Pit--Claudel2015-07-16
| * | [IronDafny] fix for ambiguous identifier error.Gravatar Michael Lowell Roberts2015-07-15
* | | Weaken the trigger cycling check to allow more patternsGravatar Clément Pit--Claudel2015-07-15
* | | Fix broken interaction between triggers and inlining of function callsGravatar Clément Pit--Claudel2015-07-14
* | | Detect matching loops at the mutli-trigger levelGravatar Clément Pit--Claudel2015-07-13
* | | Start adding missing triggers to the translatorGravatar Clément Pit--Claudel2015-07-13
* | | Fix multiple tests that relied on z3 triggering on $BoxGravatar Clément Pit--Claudel2015-07-13
* | | Add /printTooltips and /autoTriggers to the CLIGravatar Clément Pit--Claudel2015-07-13
* | | Register the trigger generator as a a rewriter in the Resolver.Gravatar Clément Pit--Claudel2015-07-13
* | | Initial import of the TriggerGenerator code.Gravatar Clément Pit--Claudel2015-07-13
* | | Make attributes enumerable.Gravatar Clément Pit--Claudel2015-07-13
| * | [IronDafny] implemented workaround for "import opened" bug(s).Gravatar Michael Lowell Roberts2015-07-13
| * | Auto-merged heads.Gravatar Michael Lowell Roberts2015-07-08
| |\|
| * | added unit tests for exclusive refinement.Gravatar Michael Lowell Roberts2015-07-08
| | * Fixed crashes in overrides checking of function decreases clauses, and improv...Gravatar Rustan Leino2015-07-07
* | | Add a new test, with a FIXMEGravatar Clément Pit--Claudel2015-07-06
| | * Report warnings only once. (This is the last step in fixing Issue #86.)Gravatar Rustan Leino2015-07-06
* | | Small refactoring of Printer.csGravatar Clément Pit--Claudel2015-07-06
| | * MergeGravatar Rustan Leino2015-07-02
| | |\ | | |/ | |/|
| | * Added command-line option /warnShadowing, which emits warnings if variables s...Gravatar Rustan Leino2015-07-02
| | * Type parameters in method/function signatures are no longer auto-declared. A...Gravatar Rustan Leino2015-07-02
| * | multiple changes...Gravatar Michael Lowell Roberts2015-07-02
| |/
| * Added another lemma to a test fileGravatar Rustan Leino2015-07-02
| * MergeGravatar leino2015-07-02
| |\
| | * Fixed a contract error provoked by one of the tests.Gravatar Bryan Parno2015-07-02
| * | Made code contracts compliantGravatar leino2015-07-01
| * | MergeGravatar leino2015-07-01
| |\|
| * | Fixed bug in BplImp!Gravatar leino2015-07-01
| | * Compile function methods into C# in a more efficient manner,Gravatar Bryan Parno2015-07-01
| | * Add the ability to specify how much "fuel" a function should have,Gravatar Bryan Parno2015-07-01
| | * MergeGravatar Bryan Parno2015-07-01
| | |\
| | * | Add code to calculate various interesting statistics about Dafny files.Gravatar Bryan Parno2015-07-01
| |/ / |/| |
| * | Fixed bugs in encoding of preconditions of function values, Issue #84.Gravatar leino2015-06-30
| * | Additional test case for instance functionsGravatar leino2015-06-30
| |/
| * Fix identifiers in nested match patterns not showing in the IDE bug. RememberGravatar qunyanm2015-06-29
|/
* MergeGravatar leino2015-06-25
|\
* | Tried to reduce frame-axiom instantiations by saying the earlier heap must be...Gravatar leino2015-06-25
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-03 13:54:26 +0000