Re: Checking Buffer Sizes
> 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
>
RE: Checking Buffer Sizes
On Wed, 13 Mar 2002 14:42:35 -0500, David Friedman wrote: >> Do I miss a suitable flag, is the implementation behind >> the documentation, ...? >> > >Yes, you need to use the +boundswrite flag. Thanks! >It seems that the necessary flags are listed >in that section of the manual, but for some reason >aren't listed in the appendix. > >David Yes, so my question was somehow worthwhile :-) BTW, the related error/warning message is "Possible out-of-bounds store", but the option is +bounds-write. For read access it is the same "Possible out-of-bounds read" and +bounds-read. I would preferto have message and flag match here. --- Alexander Mai [EMAIL PROTECTED]
Re: Checking Buffer Sizes
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
RE: Checking Buffer Sizes
> -Original Message- > From: Alexander Mai [mailto:[EMAIL PROTECTED]] > Sent: Wednesday, March 13, 2002 12:46 PM > To: [EMAIL PROTECTED] > Subject: Checking Buffer Sizes > > > 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, ...? > Yes, you need to use the +boundswrite flag. It seems that the necessary flags are listed in that section of the manual, but for some reason aren't listed in the appendix. David > > --- > Alexander Mai > [EMAIL PROTECTED] > > >
Re: Checking Buffer Sizes
> 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.) > > --- > Alexander Mai > [EMAIL PROTECTED] > > >
Checking Buffer Sizes
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, ...? --- Alexander Mai [EMAIL PROTECTED]
