example code for using exceptional successor stores in a transfer function?

[msridhar]

I was wondering if there is a checker that makes use of exceptional successor stores in a transfer function for method calls (or something similar) that we could use as an example. Here is our current transfer function code:

https://github.com/kelloggm/object-construction-checker/blob/master/object-construction-checker/src/main/java/org/checkerframework/checker/objectconstruction/ObjectConstructionTransfer.java#L40

Here is where the stores are updated:

https://github.com/kelloggm/object-construction-checker/blob/69c119b2711ec4be2ada2906ab584883b1a43042/object-construction-checker/src/main/java/org/checkerframework/checker/objectconstruction/ObjectConstructionTransfer.java#L80-L87

I'd like to change this code to also update types in the stores for any exceptional successors. But the result store obtained from calling the superclass visitMethodInvocation method does not have any exceptional successor stores (result.getExceptionalStores() is null).

I'm thinking what we want to do is:

• figure out the possible exception types for the invocation
• make a copy of the input store copy
• make a map excStores from each exception type to copy
• update copy just like we are updating the then and else store
• stick excStores in the returned TransferResult

Is there any checked that already does something like that we can learn from?

[msridhar]

For the record the strategy outlined above seemed to work out. Here is a commit that does it:

msridhar/object-construction-checker@de71cb7