summaryrefslogtreecommitdiff
path: root/Test/dafny0
Commit message (Expand)AuthorAge
* Make /autoTriggers:1 to be default. Add /autoTriggers:0 to tests that requiresGravatar qunyanm2016-03-28
* Update module export error messages. Also for "import Y" if there is at leastGravatar qunyanm2016-03-21
* Fix issue 93. Add per-function fuel setting that can be adjusted locally basedGravatar qunyanm2016-03-18
* Fix issue 136. Less aggressive Lit wrap for assert/assume.Gravatar qunyanm2016-02-26
* Renamed identifiers for increased geopolitical appealGravatar Rustan Leino2016-02-08
* Fix issue 125. Add the missing case 2 and 3 with refinement and opened imports.Gravatar qunyanm2016-02-05
* Mark old "import A as B" syntax as deprecated. The new syntax is "import A : B"Gravatar qunyanm2016-02-02
* Implement module export so we can export a subset of items defined in theGravatar qunyanm2016-01-29
* Fix build and test failures, cleanup grammar.Gravatar Richard L. Ford2016-01-27
* Add ExternNegative2.dfy.expect.Gravatar Richard L. Ford2016-01-27
* Implement 'extern' declaration modifier.Gravatar Richard L. Ford2016-01-27
* Fix issue 103. Emit the quantifiers for ForallStmt before AutoTrigger so thatGravatar qunyanm2015-11-25
* Fixed compilation of equality between reference typesGravatar leino2015-11-11
* Fix issue 91 - Change how we compute the bounds of quantified variables so thatGravatar qunyanm2015-10-29
* In method and iterator specifications, inline top-level predicates (exceptGravatar leino2015-10-24
* Introduced new datatype update syntax: D.(f := E)Gravatar leino2015-10-23
* Improve Dafny's ability to find fueled functions by checking the function its...Gravatar Bryan Parno2015-10-19
* Renamed ExistentialGuards... to BindingGuards...Gravatar Rustan Leino2015-10-07
* Use /env:0 to avoid full pathnames in test outputGravatar Rustan Leino2015-10-06
* Implemented resolution, verification, and (poorly performing) compilation of ...Gravatar leino2015-10-05
* Parsing and pretty printing of the new "existential guards" of the two kinds ...Gravatar leino2015-10-03
* Made /rewriteFocalPredicates:1 the defaultGravatar Rustan Leino2015-10-02
* Hover text includes #[_k-1] suffix for terms rewritten in prefix predicates/l...Gravatar Rustan Leino2015-10-02
* Removed specContextOnly parameter from ResolveStatement.Gravatar leino2015-09-28
* Removed more traces of the previous resolution checks that happened during pa...Gravatar leino2015-09-28
* Additional testsGravatar leino2015-09-28
* Whitespace changes in test fileGravatar leino2015-09-28
* Changed computation of ghosts until pass 2 of resolution.Gravatar leino2015-09-28
* Added back in various ghost testsGravatar leino2015-09-20
* Changes that only affect line numbers in test caseGravatar leino2015-09-20
* Removed tabs from test fileGravatar leino2015-09-20
* Preliminary refactoring of ghost-statement computations to after type checkingGravatar leino2015-09-20
* MergeGravatar Clément Pit--Claudel2015-09-02
|\
* | Add a small test from a discussion with BryanGravatar Clément Pit--Claudel2015-08-28
* | Implement workarounds for some tests that fail with /autoTriggers.Gravatar Clément Pit--Claudel2015-08-28
* | Suppress many warnings in the test suite.Gravatar Clément Pit--Claudel2015-08-28
| * Added tests for Boogie's new /verifySnapshots:3, which will be used by the Da...Gravatar Rustan Leino2015-08-28
|/
* Add change missing from bd47e3cdb79cGravatar Clément Pit--Claudel2015-08-23
* Added /autoTriggers to two tests where it only makes a cosmetic differenceGravatar Clément Pit--Claudel2015-08-23
* Replace b || !b by true in Snapshots5.v1.dfyGravatar Clément Pit--Claudel2015-08-23
* Fix: multi-dimensional OOB errors were sometimes reported on incorrect locati...Gravatar Clément Pit--Claudel2015-08-23
* MergeGravatar Rustan Leino2015-08-20
|\
* | Fixed compilation that involve enumeration over native-type newtype values.Gravatar Rustan Leino2015-08-20
| * Merge.Gravatar Clément Pit--Claudel2015-08-20
| |\ | |/ |/|
* | MergeGravatar Rustan Leino2015-08-20
|\ \
| | * Add a test to check that there are as many errors as failed preconditionsGravatar Clément Pit--Claudel2015-08-19
| |/
* | Refactored and improved bounds discoveryGravatar Rustan Leino2015-08-19
| * Merge.Gravatar Clément Pit--Claudel2015-08-19
| |\ | |/ |/|
| * Cleanup indentation of trigger warningsGravatar Clément Pit--Claudel2015-08-19
| * Draft out a more advanced version of trigger generationGravatar Clément Pit--Claudel2015-08-19
generated by cgit v1.2.3 (git 2.39.1) at 2024-04-29 14:48:41 +0000