#16 parse problem /*NOTREACHED*/
$ cat test1.c
/*NOTREACHED*/
$ splint +keep test1.c
Splint 3.1.2 --- 14 Oct 2010
test1.c:1:15: Traditional lint comment /*NOTREACHED*/ used. Splint interprets
this in the same way as most Unix lints, but it is preferable to replace it
with the /*@notreached@*/ semantic comment.
A traditional lint comment is used. Some traditional lint comments are
interpreted by Splint to enable easier checking of legacy code. It is
preferable to replace these comments with the suggested Splint alternative.
(Use -warnlintcomments to inhibit warning)
test1.c:1:15: Parse Error. (For help on parse errors, see splint -help
parseerrors.)
*** Cannot continue.
Temporary files kept:
/home/dmitry/test1.c:1
/tmp/cl4BAA.c:1
$ cat /tmp/cl4BAA.c
# 1 "/home/dmitry/test1.c"
%{l_notreach%}
$
substitute /*NOTREACHED*/ to /* NOTREACHED*/ can fix this
This is not a parse problem (or if it is you have it backwards). The /*NOTREACHED*/ without a space is being parse and the program is just telling you there is a better way to annotate this. I am not sure why it does not provide the same message for the second case. It is just ignoring it as per a normal comment.