What is a type error? [correction]

[David Hopwood]

Darren New wrote:
> David Hopwood wrote:
> 
>> public class LoopInitTest {
>>     public static String getString() { return "foo"; }
>>
>>     public static void main(String[] args) {
>>         String line = getString();
>>         boolean is_last = false;
>>
>>         while (!is_last) {
>>             if (line.charAt(0) == 'q') {
>>                 is_last = true;
>>             }
>>
>>             // insert line into inputs (not important for analysis)
>>
>>             if (!is_last) {
>>                 line = getString();
>>             }
>>         }
>>     }
>> }
>>
>> which compiles without error, because is_last is definitely initialized.
> 
> At what point do you think is_last or line would seem to not be
> initialized? They're both set at the start of the function, and (given
> that it's Java) nothing can unset them.
> 
> At the start of the while loop, it's initialized. At the end of the
> while loop, it's initialized. So the merge point of the while loop has
> it marked as initialized.

Apparently, Hermes (at least the version of it described in that paper)
essentially forgets that is_last has been initialized at the top of the
loop, and so when it does the merge, it is merging 'not necessarily initialized'
with 'initialized'.

This sounds like a pretty easy thing to fix to me (and maybe it was fixed
later, since there are other papers on Hermes' typestate checking that I
haven't read yet).

-- 
David Hopwood <david.nospam.hopwood at blueyonder.co.uk>