Re: INCLUDE header option
On Wed, Oct 16, 2002 at 12:51:51PM +0530, Vasan V S wrote: Hi, Can someone explain me how to make SPLINT to include header files available in some customised path? I tried # splint -I INclude path C filename and it does not seem to work. You need to do -IINCLUDE path i.e. there is no space between the -I and the include path. This is a bit odd but it is the way gcc and must other unix cc programs do things. Any other ways of specifying the include path would be much appreciated. Thanks, Vasan
Re: out of bounds problem
Argenton, Currently, this is a limitation of Splint. Right now we only try to detect array accesses in which the index is greater than the maximum allowable value. We do not currently try to detect cases in which the index is less than the minimum safe value. We didn't include this type of checking because reads beyond the end of an array are a more common problem and checking for reads before the bringing of an array tended to produce large numbers of false positives. We'll look into adding some type of functionality to detect reads before the bringing of an array in a future release. On Tue, Oct 08, 2002 at 04:44:47PM +0200, Argenton Paolo wrote: Hi all, I was just playing around with splint and typed in the following code fragment: int a[ 10 ]; a[ 10 ] = 0; /* this is correcty detected */ a[ -1 ] = 0; /* this is NOT detected */ where am I wrong ? is it a Splint flaw ? thanks Paolo
Re: maxRead()/Set() annotations
Splint does not allow #defined constants to be used in function constraints unless
they are defined with the constant anotation.
For example in the code below after the line
#define SIZE1024
you would add
/*@constant int SIZE=1024@*/
(In most other cases Splint does handle #defined constants correctly even if the the
constant annotation is not used.)
The version of splint in CVS has now been patched in print an error describing the
problem and suggestioning the constant annotation instead of crashing.
On Sat, Jun 29, 2002 at 04:01:14AM -0400, David Richard Larochelle wrote:
I was able to verify the problem and I'll try to put together a patch for the
internal error in the next few days.
-David
On Thu, Jun 27, 2002 at 06:33:31PM +0200, Enrico Scholz wrote:
Hello,
while trying to check the following program-fragment which copies the
content of one list into another one, splint generates bounds-checking
warnings.
The first one probably appears because 'src-elems[i]-data' may contain
uninitialized values. The
(maxRead(src-elems[].data)+1) == SIZE
in the @requires@ clause in line 20 does not help. I tried a helper
function 'getData()' (lines 10-14), but when using it by uncommenting
line 26, splint fails with an internal error:
| vec.c:33:2: *** Fatal bug: Invalid sRef
| *** Last code point: exprNode.c:10066
| *** Previous code point: exprNode.c:10066
| *** Please report bug to [EMAIL PROTECTED] ***
The last two warnings are caused because splint can not derive
maxSet(dst-elems) = i
from the
(maxRead(dst-elems)+1) = src-cnt (line 19)
and
isrc-cnt(line 24)
relations. I tried to give hints like 'assert(i=src-cnt-1)' but the
warnings remain.
How can I write the code so that it can be checked with splint?
--
1 #include string.h
2 #define SIZE1024
3 struct Data {
4 chardata[SIZE];
5 };
6 struct Vector {
7 /*@owned@*/struct Data *elems;
8 unsigned intcnt;
9 };
10 char *getData(/*@returned@*/struct Data *dta)
11 /*@ensures (maxRead(result)+1) == SIZE@*/
12 {
13return dta-data;
14 }
15 void foo(struct Vector *dst,
16 /*@in@*/struct Vector const *src)
17 /*@modifies dst-elems@*/
18 /*@requires (maxRead(src-elems)+1) == src-cnt
19 /\ (maxRead(dst-elems)+1) = src-cnt
20 /\ (maxRead(src-elems[].data)+1) == SIZE
21 @*/
22 {
23unsigned int i;
24for (i=0; isrc-cnt; ++i) {
25 memcpy(dst-elems[i].data, src-elems[i].data, SIZE);
26 //memcpy(getData(dst-elems+i), getData(src-elems+i), SIZE);
27}
28 }
--
| $ splint +bounds vec.c
| Splint 3.0.1.6 --- 17 Jun 2002
|
| vec.c: (in function foo)
| vec.c:30:5: Possible out-of-bounds read:
| memcpy(dst-elems[i].data, src-elems[i].data, 1024)
| Unable to resolve constraint:
| requires undef = 1024
| needed to satisfy precondition:
| requires maxRead(src-elems[i].data @ vec.c:30:32) = 1023
| derived from memcpy precondition: requires maxRead(parameter 2) =
| parameter 3 + -1
| A memory read references memory beyond the allocated storage. (Use
| -boundsread to inhibit warning)
| vec.c:30:12: Possible out-of-bounds read:
| dst-elems[i]
| Unable to resolve constraint:
| requires maxRead(dst-elems @ vec.c:30:12) = i @ vec.c:30:23
| needed to satisfy precondition:
| requires maxRead(dst-elems @ vec.c:30:12) = i @ vec.c:30:23
| vec.c:30:32: Possible out-of-bounds read:
| src-elems[i]
| Unable to resolve constraint:
| requires *(parameter 2).cnt = i @ vec.c:30:43 + 1
| needed to satisfy precondition:
| requires maxRead(src-elems @ vec.c:30:32) = i @ vec.c:30:43
|
| Finished checking --- 3 code warnings
Enrico
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: Manual versions
Also the HTML complete file which one might be tempted to download is not a stand-alone file, IIRC it links images, style-sheets, etc. Perhaps one should offer a package for offline viewing? (some .tar.gz archive perhaps including all required files). You could try using mget to pull down the files you need. --- 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]
