Yves, The annotation /*@noreturn@*/ at the function DisplayMessage() means that this function does NOT return. Therefore Splint's conclusion is correct.
Anyway, your code looks a bit over-annotated to me... Concerning the memory bounds checks, my experiences with Splint are mixed. Some things work, some don't (either way, no reports on erroneous code and reports on correct code), and so we gave up using Splint for memory bounds checks. Additionally Splint can't handle more than one dimension... HTH, Bodo _______________________________________________ splint-discuss mailing list [email protected] http://www.cs.virginia.edu/mailman/listinfo/splint-discuss
