Subj : Re: Problem in jsscope.c?
To   : MA
From : Brendan Eich
Date : Tue Sep 21 2004 01:06 pm

MA wrote:

> Brendan Eich <brendan@meer.net> wrote in message news:<414F3751.40003@meer.net>...
> 
>>It may be that Klocwork's static analysis is not up to reasoning 
>>completely about the code, and my analysis (and intent and design and 
>>review when writing this code) is correct.  Otherwise, you'd have to 
>>point out how the invariant that the last chunk is never empty is violated.
> 
> 
> Well, that answers my question. I just wanted to be sure that the intention
> was to ensure that kids[0] is never NULL. Although code in lines 678 - 683
> makes sure of that, its not sufficient. The code that adds a  new chunk to 
> the list of chunks also has to make sure that kids[0] of new chunk  is 
> non-null, and  the rest of the code must not mess around with it. 


Sure, else why allocate the chunk? ;-)


> IMO, neither Klocwork nor any other software can be expected to 
> verify that. 


We may be past the limits of static analysis of C code.  Maybe Rob can 
read back in this thread and comment.


> Thanks very much for the help.


Np.

/be

.