Skip to content

Commit

Permalink
improve error message text for the RLC (#4896)
Browse files Browse the repository at this point in the history
  • Loading branch information
kelloggm committed Aug 20, 2021
1 parent 4480e55 commit 8fb6f74
Show file tree
Hide file tree
Showing 2 changed files with 10 additions and 4 deletions.
Expand Up @@ -534,7 +534,11 @@ private void checkCreatesMustCallForInvocation(
}

String missingStrs = StringsPlume.join(", ", missing);
checker.reportError(node.getTree(), "reset.not.owning", missingStrs);
checker.reportError(
node.getTree(),
"reset.not.owning",
node.getTarget().getMethod().getSimpleName().toString(),
missingStrs);
}

/**
Expand Down Expand Up @@ -1251,6 +1255,7 @@ private void checkEnclosingMethodIsCreatesMustCallFor(
checker.reportError(
enclosingMethod,
"missing.creates.mustcall.for",
enclosingMethodElt.getSimpleName().toString(),
receiverString,
((FieldAccessNode) lhs).getFieldName());
return;
Expand All @@ -1276,6 +1281,7 @@ private void checkEnclosingMethodIsCreatesMustCallFor(
checker.reportError(
enclosingMethod,
"incompatible.creates.mustcall.for",
enclosingMethodElt.getSimpleName().toString(),
receiverString,
((FieldAccessNode) lhs).getFieldName(),
String.join(", ", checked));
Expand Down
@@ -1,6 +1,6 @@
required.method.not.called=@MustCall %s may not have been invoked on %s or any of its aliases.\nThe type of object is: %s.\nReason for going out of scope: %s
missing.creates.mustcall.for=This method re-assigns the non-final, owning field %s.%s, but does not have a corresponding @CreatesMustCallFor annotation.
incompatible.creates.mustcall.for=This method re-assigns the non-final, owning field %s.%s, but its @CreatesMustCallFor annotation targets %s.
reset.not.owning=Calling this method resets the must-call obligations of the expression %s, which is non-owning. Either annotate its declaration with an @Owning annotation, extract it into a local variable, or write a corresponding @CreatesMustCallFor annotation on the method that encloses this statement.
missing.creates.mustcall.for=Method %s re-assigns the non-final, owning field %s.%s, but does not have a corresponding @CreatesMustCallFor annotation.
incompatible.creates.mustcall.for=Method %s re-assigns the non-final, owning field %s.%s, but its @CreatesMustCallFor annotation targets %s.
reset.not.owning=Calling method %s resets the must-call obligations of the expression %s, which is non-owning. Either annotate its declaration with an @Owning annotation, extract it into a local variable, or write a corresponding @CreatesMustCallFor annotation on the method that encloses this statement.
creates.mustcall.for.override.invalid=Method %s cannot override method %s, which defines fewer @CreatesMustCallFor targets.\nfound: %s\nrequired: %s
destructor.exceptional.postcondition=Method %s must resolve the must-call obligations of the owning field %s along all paths, including exceptional paths. On an exceptional path, the @EnsuresCalledMethods annotation was not satisfied.\nFound: %s\nRequired: %s

0 comments on commit 8fb6f74

Please sign in to comment.