Skip to content

Commit

Permalink
chore: address dafny-lang/dafny#2500
Browse files Browse the repository at this point in the history
  • Loading branch information
texastony committed Jul 27, 2022
1 parent 398c7f6 commit e2bea22
Showing 1 changed file with 14 additions and 0 deletions.
14 changes: 14 additions & 0 deletions .github/PULL_REQUEST_TEMPLATE.md
Original file line number Diff line number Diff line change
Expand Up @@ -6,3 +6,17 @@


By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 license.

# Due to [dafny-lang/dafny#2500](https://github.com/dafny-lang/dafny/issues/2500), Traits are dangerous:
1. [ ] Does this PR add any traits or classes that extend a trait?
2. [ ] Are these traits annoated with `{:termination false}`?

The override checks on the specifications on a class' functions/methods/etc.
validating that specifcations are
at least as strong as those on the traits it implements
are not working correctly when
that trait is defined in a different module
(and hence must have `{:termination false}` on it).

As such, if either (1.) or (2.) is true:
Have you [ ] manually verified all the trait specifications are copied onto classes that extend them?

0 comments on commit e2bea22

Please sign in to comment.