Skip to content

Commit

Permalink
Don't complain about determinism for traits (dafny-lang#5711)
Browse files Browse the repository at this point in the history
### Description

After dafny-lang#5632, Dafny started complaining about traits lacking constructors
(which they can't have) when `--enforce-determinism` was enabled. This
changes back to the previous behavior of warning only about classes
without constructors.

### How has this been tested?

Updated `dafny0/ForbidNondeterminismResolve.dfy` to include a trait
declaration.

By submitting this pull request, I confirm that my contribution
is made under the terms of the MIT license.
  • Loading branch information
atomb authored and dnezam committed Sep 21, 2024
1 parent ee6d30c commit 6c9e016
Show file tree
Hide file tree
Showing 2 changed files with 10 additions and 6 deletions.
10 changes: 5 additions & 5 deletions Source/DafnyCore/Resolver/ModuleResolver.cs
Original file line number Diff line number Diff line change
Expand Up @@ -1479,16 +1479,16 @@ public void ResolveTopLevelDecls_Core(List<TopLevelDecl> declarations,
// ----------------------------------------------------------------------------

foreach (TopLevelDecl d in declarations) {
if (d is ClassLikeDecl classLikeDecl) {
var classIsExtern = !Options.DisallowExterns && Attributes.Contains(classLikeDecl.Attributes, "extern");
if (d is ClassDecl classDecl) {
var classIsExtern = !Options.DisallowExterns && Attributes.Contains(classDecl.Attributes, "extern");
if (Options.ForbidNondeterminism &&
!classIsExtern &&
!classLikeDecl.Members.Exists(member => member is Constructor) &&
classLikeDecl.Members.Exists(member => member is Field && !(member is ConstantField { Rhs: not null }))) {
!classDecl.Members.Exists(member => member is Constructor) &&
classDecl.Members.Exists(member => member is Field && !(member is ConstantField { Rhs: not null }))) {
// This check should be moved to the resolver once we have a language construct to indicate the type is imported
// Instead of the extern attribute
Reporter.Error(MessageSource.Resolver, GeneratorErrors.ErrorId.c_constructorless_class_forbidden,
classLikeDecl.tok,
classDecl.tok,
"since fields are initialized arbitrarily, constructor-less classes are forbidden by the --enforce-determinism option");
}
}
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -142,4 +142,8 @@ ghost method M2(c: C)
a[i] := *; // error: nondeterministic
}
modify c; // error: nondeterministic
}
}

trait t { // no error: traits can't have constructors
var f: real
}

0 comments on commit 6c9e016

Please sign in to comment.