[splint-discuss] Passed storage not completely defined

[Jason blank]

From: Michael.Wojcik at microfocus.com
But Perm has been initialized - it points to the same
object as "array" in main, which was initialized from the values in
argv.

 

And while Permute does not operate on the contents pointed to by
the values in the Perm array, it does use those values (as it rearranges them).
So an @out@ annotation would be incorrect, even if it suppresses the error.

 

I don't see any reasonable interpretation here other than that
the diagnostic from Splint is incorrect. In the call to Permute in main, "*array"
is identical to "array[0]", and array[0] has been initialized unless
one of the following holds:

 

- argc < 2 (and the program should have checked for this,
since it causes undefined behavior if argc==0 and implementation-defined
behavior if argc==1, both of which are possible)

- argv[1] is undefined (which should not happen in a hosted
implementation if argc >= 2, and Splint should know that)

 

Some other criticisms might be leveled against the code (why is
temp in Permute an array, when only the first element is ever used?), but
unless I'm missing something, this is an incorrect diagnostic from Splint.

 
The code I posted was an example program that demonstates the problem in as small a working program as possible.  The whole program is to large to post.  In the real program I do check the argument count.

Good point about the temp array.  I don't know what the answer is; I didn't write that code.  I will fix it in my version.

Thanks,

 		 	   		  
_________________________________________________________________
Hotmail: Powerful Free email with security by Microsoft.
http://clk.atdmt.com/GBL/go/196390710/direct/01/
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.cs.virginia.edu/pipermail/splint-discuss/attachments/20100127/172f4914/attachment.html