First, a "Dank u wel!" to mailto://Arjan M Van Vught <[EMAIL PROTECTED]>
for a ~/.splintrc to work with VC++6.00. I shall try his work.
Now my problem. I have the following scenario.
C:\ftm\fromaix.6\src\c\libs> type t.c
#include <time.h> /* For strftime */
typedef char date_now_t[7+1]; /* YYYYDDD */
/*@dependent@*/ static const char *
fdate_now(/*@out@*/ /*@notnull@*/ date_now_t string, time_t const timenow)
{
struct tm *l = localtime(&timenow);
(void)strftime(string, 7+1, "%Y%j", l);
return string;
}
#include <stdio.h>
void call(void) {
date_now_t date_space;
(void)puts(fdate_now(date_space, time(NULL)));
}
C:\ftm\fromaix.6\src\c\libs> splint -fixedformalarray t.c
Splint 3.0.1.6 --- 11 Feb 2002
t.c: (in function fdate_now)
t.c(7,41): Possibly null storage l passed as non-null param: strftime (..., l)
A possibly null pointer is passed as a parameter corresponding to a formal
parameter with no /*@null@*/ annotation. If NULL may be used for this
parameter, add a /*@null@*/ annotation to the function parameter declaration.
(Use -nullpass to inhibit warning)
t.c(6,20): Storage l may become null
Finished checking --- 1 code warning
C:\ftm\fromaix.6\src\c\libs>
The first problem I have is with the need for the -fixedformalarray
filter. I understand that C degrades a "char foo[8]" parameter to
"char *foo". I am trying to communicate that any call of "fdate_now" has
"string" passed as a set of 8 bytes.
Am I wrong to be surprised the following gives no buffer overflow
message: "char foo[1]; foo[1] = 'b';"
The second problem is the message I am invited to suppress.
After I started writing this, I suppressed it with code like
if (l) strftime(string,, 7+1, "%Y%j", l) else strcpy(string, "YYYYDDD");
I then moved on and hit another point involving localtime().
It does not have an error interface specified in either C89 or
IEEE 1003-2001. I infer the same applies in C99.
I quote from IEEE 2001.
> 23036 RETURN VALUE
> 23037 The localtime() function shall return a pointer to the broken-
> down time structure.
> 23040 ERRORS
> 23041 No errors are defined.
splint allows localtime() to return NULL on failure. I think it should
not. I changed lib/standard.h, rebuilt *.lcd and migrated them to the
PC. (I had already reported a segmentation fault on the PC to
[EMAIL PROTECTED])
Should splint not report unreachable code with constructs like:
"if (0) return 0; else return 1;"
It does with "return 0; return 1;" which gives "This code will never be
reached on any possible execution. (Use -unreachable to inhibit
warning)"
I am sorry this became so complicated. I hope it sorts itself out!
--
Walter Briscoe
