Incorrect logic in BackwardAnalysisImpl for exceptional successors

[msridhar]

I was looking at the following code:

checker-framework/dataflow/src/main/java/org/checkerframework/dataflow/analysis/BackwardAnalysisImpl.java

Lines 256 to 263 in b256527

	if (pred instanceof ExceptionBlock
	&& ((ExceptionBlock) pred).getSuccessor() != null
	&& node != null) {
	@Nullable Block succBlock = ((ExceptionBlock) pred).getSuccessor();
	@Nullable Block block = node.getBlock();
	if (succBlock != null && block != null && succBlock.getUid() == block.getUid()) {
	// If the block of passing node is an exceptional successor of Block pred, propagate
	// store to the exceptionStores. Currently it doesn't track the label of an

It seems to be trying to check if block is an exceptional successor of pred. But the check is wrong, as ((ExceptionBlock) pred).getSuccessor() will get the non-exceptional successor (getExceptionalSuccessors() should be used instead). Reading the surrounding code, I think the impact of this bug is that in many cases, stores will not get propagated at all along exceptional control-flow edges in the backwards analysis. Not sure if there are tests for this.