Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
IncompleteOperationErrors are reported, if the a dataflow path does not end in an accepting state. However, if there are multiple dataflow paths, multiple IncompleteOperationErrors are reported, although some paths lead to an accepting state. For example, for
the analysis reports an error at the call to
init
with the info that a call todoFinal
is missing, and it reports an error at the call todoFinal
with the info that a call todoFinal
is missing. The second error is not quite correct becausedoFinal
is called on the corresponding dataflow path. Hence, this is a false positive.This PR adds the logic for reporting the errors only on the correct positions (here at
init
) and adds the information that there is a potential dataflow path, where a call todoFinal
is missing. This holds also for loops.Fixes #51