Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Fix: Reveal statements can now invoke instance functions statically #4180

Merged
merged 21 commits into from
Jun 20, 2023
Merged

Fix: Reveal statements can now invoke instance functions statically #4180

Show file tree
Hide file tree
Changes from 5 commits
Commits
Show all changes
21 commits
Select commit Hold shift + click to select a range
0e4c92e
Fixed issue #4176 by changing generated reveal lemmas to be static
EkanshdeepGupta Jun 14, 2023
633961e
Added test for github issue 4176
EkanshdeepGupta Jun 14, 2023
47cc712
Added doc file for bugfix
EkanshdeepGupta Jun 14, 2023
6d884d4
Renamed tests
EkanshdeepGupta Jun 14, 2023
c38fcfb
removed blank line from end of test file
EkanshdeepGupta Jun 14, 2023
142e26b
Added twostate function in git-issue-4176.dfy test and undid spurious…
EkanshdeepGupta Jun 14, 2023
0335cb4
Merge branch 'master' into fix-4176-reveal-crash
MikaelMayer Jun 15, 2023
3754a54
Merge branch 'master' into fix-4176-reveal-crash
MikaelMayer Jun 15, 2023
d5c1c37
updated fix to make members of DefaultClassDecl be non-static
EkanshdeepGupta Jun 15, 2023
9e6a621
updated static computation for added reveals lemmas
EkanshdeepGupta Jun 16, 2023
dce07e8
Merge branch 'master' into fix-4176-reveal-crash
EkanshdeepGupta Jun 16, 2023
2e20e18
Merge branch 'master' into fix-4176-reveal-crash
EkanshdeepGupta Jun 19, 2023
71d94cb
Allowed autogenerated members of DefaultDecl to be static
EkanshdeepGupta Jun 19, 2023
c938ca7
Skipping generating reveal lemma for functions with empty field
EkanshdeepGupta Jun 19, 2023
6a7bdb9
Merge branch 'master' into fix-4176-reveal-crash
EkanshdeepGupta Jun 19, 2023
924d3ee
rebasing changes from master
EkanshdeepGupta Jun 19, 2023
64f4826
Removed extra whitespace
EkanshdeepGupta Jun 19, 2023
6d925d8
Removed extra whitespace
EkanshdeepGupta Jun 19, 2023
33ece45
Merge branch 'master' into fix-4176-reveal-crash
EkanshdeepGupta Jun 20, 2023
712afc4
Added feat file
EkanshdeepGupta Jun 20, 2023
b267888
Merge branch 'master' into fix-4176-reveal-crash
EkanshdeepGupta Jun 20, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 2 additions & 2 deletions Source/DafnyCore/Rewriters/OpaqueMemberRewriter.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -140,11 +140,11 @@ private void GenerateRevealLemma(MemberDecl m, List<MemberDecl> newDecls) {
}
Method reveal;
if (m is TwoStateFunction) {
reveal = new TwoStateLemma(m.RangeToken, m.NameNode.Prepend("reveal_"), m.HasStaticKeyword, new List<TypeParameter>(), new List<Formal>(), new List<Formal>(), new List<AttributedExpression>(),
reveal = new TwoStateLemma(m.RangeToken, m.NameNode.Prepend("reveal_"), true, new List<TypeParameter>(), new List<Formal>(), new List<Formal>(), new List<AttributedExpression>(),
EkanshdeepGupta marked this conversation as resolved.
Show resolved Hide resolved
new Specification<FrameExpression>(new List<FrameExpression>(), null), ens,
new Specification<Expression>(new List<Expression>(), null), null, lemma_attrs, null);
} else {
reveal = new Lemma(m.RangeToken, m.NameNode.Prepend("reveal_"), m.HasStaticKeyword, new List<TypeParameter>(), new List<Formal>(), new List<Formal>(), new List<AttributedExpression>(),
reveal = new Lemma(m.RangeToken, m.NameNode.Prepend("reveal_"), true, new List<TypeParameter>(), new List<Formal>(), new List<Formal>(), new List<AttributedExpression>(),
new Specification<FrameExpression>(new List<FrameExpression>(), null), ens,
new Specification<Expression>(new List<Expression>(), null), null, lemma_attrs, null);
}
Expand Down
10 changes: 10 additions & 0 deletions Source/IntegrationTests/IntegrationTests.csproj
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -47,6 +47,16 @@
<Content Include="..\..\node_modules\**\*.*" LinkBase="TestFiles\LitTests\LitTest\node_modules">
<CopyToOutputDirectory>PreserveNewest</CopyToOutputDirectory>
</Content>
<Content Update="..\..\Test\git-issues\github-issue-4176.dfy">
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Please remove this change. We don't need this here, tests are discovered automatically. It was probably added by Rider.

<Link>TestFiles\LitTests\LitTest\git-issues\github-issue-4176.dfy</Link>
</Content>
<Content Update="..\..\Test\git-issues\github-issue-4176.dfy.expect">
<Link>TestFiles\LitTests\LitTest\git-issues\github-issue-4176.dfy.expect</Link>
</Content>
</ItemGroup>

<ItemGroup>
<Folder Include="TestFiles\LitTests\LitTest\git-issues\" />
</ItemGroup>

</Project>
14 changes: 14 additions & 0 deletions Test/git-issues/git-issue-4176.dfy
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,14 @@
// RUN: %baredafny verify %args %s > %t
// RUN: %diff "%s.expect" "%t"

method test() {
var c := new Class();
reveal Class.P();
assert c.P();
}

class Class {
opaque function P() : bool { true }

constructor () { }
}
2 changes: 2 additions & 0 deletions Test/git-issues/git-issue-4176.dfy.expect
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@

Dafny program verifier finished with 1 verified, 0 errors
1 change: 1 addition & 0 deletions docs/dev/4176.fix
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
Revealing opaque instance functions can now be done statically