[splint-discuss] Splint-3.1.2 bugs - Mudflap

[John Carter]

Here are some bugs I have found in Splint-3.1.2...

1) Meta bug :-) There doesn't seem to be a 3.1.2 tag in the CVS repository!

2) Splint 3.1.2 chokes on unary + eg...

   int i = +1;

3) I started hunting a sporadic bug when I decided it would be easier
to use gcc-4.2.3's "mudflap" facility....


So I pulled out the CVS latest version of splint and compiled it with
mudflap checking when I hit a Bug Bonanza...

In src/lcllib.c:432 an array of length 128 is used as a buffer for
input from read_readline....



# define BUFLEN 128

static bool
loadLCDFile (FILE *f, cstring name)
{
   char buf[BUFLEN];

   /*
   ** Check version.  Should be >= SPLINT_LIBVERSION
   */

   if (reader_readLine (f, buf, BUFLEN) == NULL


In src/reader.c:234

char *reader_readLine (FILE *f, char *s, int max)
{
   char *res = fgets (s, MAX_DUMP_LINE_LENGTH, f);

Where in src/Headers/constants.h
# define MAX_DUMP_LINE_LENGTH 16384

ie. Sometimes dynamic checking tools beats static analysis. :-))


An example of the mudflap output from the build time tests are appended below.

John Carter                             Phone : (64)(3) 358 6639
Tait Electronics                        Fax   : (64)(3) 359 4632
PO Box 1645 Christchurch                Email : john.carter at tait.co.nz
New Zealand

../src/splint -supcounts -nof -incondefs -nolib +impconj -DSTRICT standard.h posix.h unix.h  stdio.h stdlib.h  -dump unixstrict
Splint 3.1.2 --- 31 Jul 2008

Finished checking --- no warnings
make[2]: Leaving directory `/home/johnc/builds/splint/lib'
Making all in imports
make[2]: Entering directory `/home/johnc/builds/splint/imports'
make[2]: Nothing to be done for `all'.
make[2]: Leaving directory `/home/johnc/builds/splint/imports'
Making all in test
make[2]: Entering directory `/home/johnc/builds/splint/test'
Testing splint 3.1.2...

Version Info:
Splint 3.1.2 --- 31 Jul 2008

Maintainer: splint-bug at splint.org
Compiled using /opt/gcc-4.2.3/bin/gcc -g3 -O0 -fmudflap on Linux parore
2.6.24-19-generic #1 SMP Fri Jul 11 23:41:49 UTC 2008 i686 GNU/Linux by johnc
Splint 3.1.2 --- 31 Jul 2008

LARCH_PATH = <not set> (default = .:/usr/local/share/splint/lib:/home/johnc/buil
ds/splint/lib:)
    --- path used to find larch initialization files and LSL traits
LCLIMPORTDIR = <not set, default: .:/usr/local/share/splint/imports:/home/johnc/
builds/splint/imports>
    --- directory containing lcl standard library files (import with < ... >)
include path = <no include path> (set by environment variable CPATH and -I
flags)
    --- path used to find #include'd files
systemdirs = /usr/ (set by -systemdirs or environment variable CPATH)
    --- if file is found on this path, it is treated as a system file for error
reporting

Tests:

Checking help...
50a51,142
> *******
> mudflap violation 1 (check/write): time=1217457834.392845 ptr=0xbffbec9c size=16384
> pc=0x40026e65 location=`(fgets buffer)'
>       /opt/gcc-4.2.3/lib/libmudflap.so.0(__mf_backtrace+0x4d) [0x40024981]
> Nearby object 1: checked region begins 0B into and ends 16256B after
> mudflap object 0x882fdc8: name=`lcllib.c:432 (loadLCDFile) buf'
> bounds=[0xbffbec9c,0xbffbed1b] size=128 area=stack check=0r/3w liveness=3
> alloc time=1217457834.392755 pc=0x400268f7
> Nearby object 2: checked region begins 216B before and ends 16164B after
> mudflap object 0x882aa90: name=`lcllib.c:335 (loadStandardState) fpath'
> bounds=[0xbffbed74,0xbffbed77] size=4 area=stack check=0r/4w liveness=4
> alloc time=1217457834.391718 pc=0x400268f7
> Nearby object 3: checked region begins 580B before and ends 15800B after
> mudflap object 0x881c568: name=`llmain.c:384 (main) passThroughArgs'
> bounds=[0xbffbeee0,0xbffbeee3] size=4 area=stack check=0r/3w liveness=3
> alloc time=1217457834.386240 pc=0x400268f7
> Nearby object 66: checked region begins 104B before and ends 16276B after
> mudflap dead object 0x882edc8: name=`message.c:156 (message) pvar'
> bounds=[0xbffbed04,0xbffbed07] size=4 area=stack check=0r/0w liveness=0
> alloc time=1217457834.392253 pc=0x400268f7
> dealloc time=1217457834.392750 pc=0x400268a8
> number of nearby objects: 66
> *******
> mudflap violation 3 (check/write): time=1217457834.393553 ptr=0xbffbec9c size=16384
> pc=0x40026e65 location=`(fgets buffer)'
>       /opt/gcc-4.2.3/lib/libmudflap.so.0(__mf_backtrace+0x4d) [0x40024981]
> Nearby object 1: checked region begins 0B into and ends 16256B after
> mudflap object 0x882fdc8: name=`lcllib.c:432 (loadLCDFile) buf'
> Nearby object 2: checked region begins 216B before and ends 16164B after
> mudflap object 0x882aa90: name=`lcllib.c:335 (loadStandardState) fpath'
> Nearby object 3: checked region begins 580B before and ends 15800B after
> mudflap object 0x881c568: name=`llmain.c:384 (main) passThroughArgs'
> Nearby object 66: checked region begins 104B before and ends 16276B after
> mudflap dead object 0x882edc8: name=`message.c:156 (message) pvar'
> number of nearby objects: 66
Compilation finished at Thu Jul 31 10:54:10