-
Notifications
You must be signed in to change notification settings - Fork 254
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.
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
Fix: Optional pre-type won't cause a crash anymore #5442
Changes from 6 commits
5906960
a44d8b1
79dfa4c
87aa2c5
eb0327c
cfa8acb
12310a8
0faf793
4445b96
File filter
Filter by extension
Conversations
Jump to
Diff view
Diff view
There are no files selected for viewing
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -583,6 +583,8 @@ public enum CommonConfirmationBag { | |
preType = preType.Normalize(); | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Can you add a comment to There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. I can't, as I don't understand the code at a level high enough to do that. I don't have a mental model of what ConfirmConstraint does, nor about what code context it was called with. I'll leave it for @RustanLeino to comment on it. |
||
if (preType is PreTypeProxy) { | ||
return false; | ||
} else if (preType is UnusedPreType) { | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Can you add a comment to the class |
||
return true; | ||
} | ||
|
||
var pt = (DPreType)preType; | ||
|
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,43 @@ | ||
// RUN: %exits-with 2 %baredafny verify %args --type-system-refresh "%s" > "%t" | ||
// RUN: %diff "%s.expect" "%t" | ||
|
||
ghost function f2(items: set<nat>): (r:nat) | ||
requires |items| > 0 { | ||
var item :| item in items; | ||
item | ||
} | ||
|
||
function f(items: set<nat>) : (r:nat) | ||
requires |items| > 0 { | ||
//assume exists item :: item in items && forall other <- items :: item == other || item < other; | ||
//assert exists item Smallest() | ||
var item :| IsSmallest(items, item); | ||
item | ||
} | ||
|
||
predicate IsSmallest(s: set<nat>, item: nat) | ||
requires item in s { | ||
m in s && forall y: nat :: y in s ==> m <= y | ||
} | ||
|
||
lemma Smallest(s: set<nat>) returns (m: nat) | ||
requires s != {} | ||
ensures m in s && IsSmallest(s, m) | ||
decreases s | ||
{ | ||
m :| m in s; | ||
if y: nat :| y in s && y < m { | ||
ghost var s' := s - {m}; | ||
assert y in s'; | ||
m := ThereIsASmallest(s'); | ||
} | ||
} | ||
|
||
function smallest(items: set<nat>): (r: nat) | ||
requires |items| > 0 | ||
|
||
method m(items: set<nat>) returns (r:nat) | ||
requires |items| > 0 { | ||
var item :| item in items; | ||
return item; | ||
} |
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,6 @@ | ||
git-issue-5369.dfy(20,2): Error: expression is not allowed to invoke a method (m) | ||
git-issue-5369.dfy(20,40): Error: expression is not allowed to invoke a method (m) | ||
git-issue-5369.dfy(20,42): Error: arguments to <= must have a common supertype (got int and (unused -- call to method m)) | ||
git-issue-5369.dfy(20,4): Error: expecting element type to be assignable to nat (got (unused -- call to method m)) | ||
git-issue-5369.dfy(32,9): Error: unresolved identifier: ThereIsASmallest | ||
5 resolution/type errors detected in git-issue-5369.dfy |
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1 @@ | ||
Optional pre-type won't cause a crash anymore |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
What do you mean by
MemberSelect
not being considered an expression? It inherits fromExpression
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
It weirdly is an Expression, but not a true Dafny expression: you cannot use it in a regular Dafny expression. Consider the following:
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
It is also used for fields, in which case it is an expression, right?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
It seems nice to conceptually consider a
MemberSelectExpr
that references a method still an expression, even if we don't allow it in an expression context. If we do that, then I would expect to assign some sort of callable type to it. Could we renameUnusedPreType
toMethod[Pre]Type
?There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Yes, it's used for fields and in that case it's indeed an expression.
I did the renaming, hoping it won't break any future development.