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.

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

Improve error message text for the RLC #4896

Merged
merged 1 commit into from
Aug 20, 2021
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Jump to
Jump to file
Failed to load files.
Diff view
Diff view
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