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

function value can depend on set of allocated objects #1419

Closed
erniecohen opened this issue Sep 7, 2021 · 2 comments · Fixed by #1924
Closed

function value can depend on set of allocated objects #1419

erniecohen opened this issue Sep 7, 2021 · 2 comments · Fixed by #1924
Assignees
@RustanLeino
Labels
kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label logic An inconsistency in Dafny's logic (e.g. in the Boogie prelude) part: verifier Translation from Dafny to Boogie (translator)

Comments

@erniecohen
Copy link

The following verifies:

type Obs = set<object>
predicate lotsOfObjects() { 
    exists o:Obs :: |o| > 10
}

(It doesn't verify if you replace o:Obs with o:set<object>.)
@robin-aws robin-aws added kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label part: verifier Translation from Dafny to Boogie (translator) logic An inconsistency in Dafny's logic (e.g. in the Boogie prelude) labels Sep 21, 2021
@robin-aws
Copy link
Member

This looks very similar to #19, which is also about failing to recognize all possible ways of indirectly quantifying over allocated objects.

@RustanLeino
Copy link
Collaborator

RustanLeino commented Mar 21, 2022 •
edited
Loading

I think the fix to this issue is to insert the NormalizeExpand(). in the following line in Type.IsAllocFree:

          return NormalizeExpand().TypeArgs.All(ta => ta.IsAllocFree);

but I haven't tried it with the whole test suite. (The call to NormalizeExpand() should apparently not be placed earlier in Type.IsAllocFree, because IsOpaqueType/AsOpaqueType apparently must use just Normalize(), or so a comment in AsOpaqueType says.)

RustanLeino added a commit to RustanLeino/dafny that referenced this issue Mar 21, 2022
@RustanLeino
Add tests
5b940ce 
Fixes dafny-lang#1419
@RustanLeino RustanLeino mentioned this issue Mar 21, 2022
Merged
@RustanLeino RustanLeino mentioned this issue Mar 30, 2022
Merged
@cpitclaudel cpitclaudel mentioned this issue Apr 1, 2022
Closed
@cpitclaudel cpitclaudel mentioned this issue Apr 25, 2022
Closed
RustanLeino added a commit that referenced this issue Apr 28, 2022
@RustanLeino
Properly check if types may contain references (#1924)
f933262 
Previously, types were not properly checked for whether or not they may contain references. This PR fixes that.

Fixes #1419

More details:

* fix: Checking of MayInvolveReferences

* fix: Compute MayInvolveReference correctly for datatypes

* fix: Replace (buggy) IsAllocFree with !MayContainReferences

* Use `older` modifier on parameter in the Schorr-Waite test programs, the absence of which is now properly detected.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@RustanLeino RustanLeino

Labels
kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label logic An inconsistency in Dafny's logic (e.g. in the Boogie prelude) part: verifier Translation from Dafny to Boogie (translator)
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Properly check if types may contain references RustanLeino/dafny
3 participants
@erniecohen @RustanLeino @robin-aws