[splint-discuss] Bug report: typedef'ing abstract types

[Dirk Herrmann]

Hello,

I want to report a bug in splint.  For the following piece of code, I 
get no warnings, although I expected that the expression x + y would 
cause a warning about incompatible types to be issued.

-------- start of test.c --------
typedef /*@abstract@*/ int foo;
typedef /*@abstract@*/ int bar;

int main (int /*@unused@*/ argc, char /*@unused@*/ *argv[])
{
    foo x = 0;
    bar y = 1;

    return x + y;
}
--------- end of test.c ---------

The output of splint (with different flags) looks as follows:

dirk(users)@trillian:~/tmp/splint > splint +strict test.c
Splint 3.1.1 --- 28 Apr 2003

Finished checking --- no warnings
dirk(users)@trillian:~/tmp/splint > splint test.c
Splint 3.1.1 --- 28 Apr 2003

Finished checking --- no warnings
dirk(users)@trillian:~/tmp/splint > splint +impabstract test.c
Splint 3.1.1 --- 28 Apr 2003

Finished checking --- no warnings

Best regards,
Dirk Herrmann