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.
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
