On Wed, Mar 13, 2002 at 02:36:59PM -0500, David Richard Larochelle wrote:
After reading in the manual (Version 3.0.1, 7 January 2002)
I tried to check some code like given in the manual
int buf[10];
buf[10] = 3;
and was prepared that Splint 3.0.1.6 would give me some
warnings/errors. But nothing at all, not even at -strict
level I saw a related warning.
Do I miss a suitable flag, is the implementation behind
the documentation, ...?
You need to use the flag +bounds to turn on bounds errors.
(You can also use +bounds-write or +bounds-read if you only care about out of
bounds reads or writes.)
And another flag I didn't know yet. Great.
Can someone explain this:
$ cat test.c
#define N 10
void g(void)
{
int i;
double arr[N];
for (i = 0; i N; i++) {
arr[i] = 0.0;
}
}
$ splint +bounds test.c
Splint 3.0.1.6 --- 11 Feb 2002
test.c: (in function g)
test.c:10:5: Possible out-of-bounds store:
arr[i]
Unable to resolve constraint:
requires i @ test.c:10:9 = 9
needed to satisfy precondition:
requires maxSet(arr @ test.c:10:5) = i @ test.c:10:9
A memory write may write to an address beyond the allocated buffer. (Use
-boundswrite to inhibit warning)
Finished checking --- 1 code warning
$
Does this mean that I have to annotate every variable? IMHO there are
enough information in the for statement that splint can do the job by
its own.
Yes this should be enough information for splint to analyze the loop
correctly. I'll try to fix this in the next version.
As a temporary work-around you can use the +orconstraint flag which will
strengthen the splint to the point where no warning is produced. However,
there are currently some problems with this flag which will cause splint to
miss certainly types of buffer overflow it would otherwise catch.
Raimar
--
email: [EMAIL PROTECTED]
+#if defined(__alpha__) defined(CONFIG_PCI)
+ /*
+* The meaning of life, the universe, and everything. Plus
+* this makes the year come out right.
+*/
+ year -= 42;
+#endif
-- Patch for 1.3.2 (kernel/time.c) from Marcus Meissner
