Skip to content

Commit

Permalink
Deprecate :dllimport and :handle (dafny-lang#3399)
Browse files Browse the repository at this point in the history
Fixes dafny-lang#2778 and recent discussion: deprecates :dllimport and :handle

<small>By submitting this pull request, I confirm that my contribution
is made under the terms of the [MIT
license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>

Co-authored-by: davidcok <davidcok@github.com>
Co-authored-by: Fabio Madge <fmadge@amazon.com>
Co-authored-by: Aaron Tomb <aarotomb@amazon.com>
Co-authored-by: Remy Willems <rwillems@amazon.com>
Co-authored-by: Mikaël Mayer <MikaelMayer@users.noreply.github.com>
Co-authored-by: stefan-aws <120379523+stefan-aws@users.noreply.github.com>
Co-authored-by: Aaron Tomb <aarontomb@gmail.com>
Co-authored-by: Alex Chew <alex-chew@users.noreply.github.com>
  • Loading branch information
9 people committed Feb 1, 2023
1 parent 70b805e commit c958452
Show file tree
Hide file tree
Showing 4 changed files with 19 additions and 1 deletion.
9 changes: 8 additions & 1 deletion Source/DafnyCore/Dafny.atg
Original file line number Diff line number Diff line change
Expand Up @@ -120,6 +120,12 @@ void CheckDeclModifiers(ref DeclModifierData dmod, string declCaption, AllowedDe
}
}

void CheckAttribute(Errors errors, IToken attr) {
if (attr.val == "dllimport" || attr.val == "handle") {
errors.Deprecated(attr, $"Attribute :{attr.val} is deprecated and will be removed in Dafny 4.0");
}
}

bool IsAssumeTypeKeyword(IToken la) {
return la.kind == _assume || la.kind == _assert || la.kind == _expect;
}
Expand Down Expand Up @@ -5175,7 +5181,8 @@ Attribute<ref Attributes attrs>
AttributeName<out x>
[ Expressions<args> ]
"}" (. closeBrace = t; .)
(. attrs = new UserSuppliedAttributes(x, openBrace, closeBrace, args, attrs);
(. CheckAttribute(errors, x);
attrs = new UserSuppliedAttributes(x, openBrace, closeBrace, args, attrs);
attrs.RangeToken = new RangeToken(openBrace, t);
.)
.
Expand Down
6 changes: 6 additions & 0 deletions Test/git-issues/git-issue-2778/git-issue-2778.dfy
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
// RUN: %baredafny resolve --use-basename-for-filename "%s" > "%t"
// RUN: %diff "%s.expect" "%t"

class {:handle} A {}

method {:dllimport "x"} m() {}
4 changes: 4 additions & 0 deletions Test/git-issues/git-issue-2778/git-issue-2778.dfy.expect
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
git-issue-2778.dfy(4,8): Warning: Attribute :handle is deprecated and will be removed in Dafny 4.0
git-issue-2778.dfy(6,9): Warning: Attribute :dllimport is deprecated and will be removed in Dafny 4.0

Dafny program verifier did not attempt verification
1 change: 1 addition & 0 deletions docs/dev/news/3399.fix
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
The attributes :dllimport and :handle are now deprecated. They were undocumented, untested, and not maintained.

0 comments on commit c958452

Please sign in to comment.