[Checkers] Question about the flow algorithm

[Mahmood Ali]

Greetings,

Now that I have read your code more thoroughly, I think the proposed  
algorithm has one bug.  It assumes that catches never throw an  
exception implicitly.  Here is an example:

   String s = null;
   try {
     methodThrowingException();
     s = "m";
     // annosAfterNormal = {NonNull={s}}
     // annosBeforeCatch = {NonNull={}}
   } catch (Exception e) {
     methodThrowingException();
     s = "m"; // <-- basically dead-code
     // annosAfterCatch = {NonNull={s}}, alive == true
   } catch(Error e) {
     s = "m";
     return;
     // annosAfterCatch = {NonNull={s}}, alive == false;
   } finally {
     // what's the type of 's' here?
     s.toString();
   }

annosAfterNormal and annosAfterCatch for all catches has 's' as  
NonNull.  However, 's' is null because s is never assigned.

> Then we come to evaluating the finally block; it is evaluated twice,
> with initial annotation sets:
> (1) conjunction of all annosAfterCatch where catchAlive == true and
> the "annosAfterNormal" set
> (2) conjunction of all annosAfterCatch where catchAlive == false
>
> The annotation set after the whole try-catch-construct should be the
> annotation set after evaluating finally (1).

I assume that your algorithm here assumes the presence of catches for  
all possible throwables.  Otherwise, we would need another evaluation  
with annosBeforeCatch as initial set for the case where an exception  
is not caught.

- Mahmood