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

[Ralf Wildenhues]

Hi Dirk,

* Dirk Herrmann wrote on Thu, Nov 25, 2004 at 11:20:01PM CET:
> 
> 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.

I don't think this is a bug in splint, because of the access heuristics
employed:  If you declare an abstract type foo in some file bar.c or
header bar.h, then by default code in both bar.h and bar.c are declared
to have access to the abstract type.  (Think of the files as the
implementation of the type, if you like.)

This behavior can be overridden with the annotations
  /*@access foo@*/
and
  /*@noaccess foo@*/
which hold for code following these annotations in the same file.

The following example will warn unless you enable the access by
replacing the ':' with '@'.

Regards,
Ralf

/* a.c */
#include "a.h"
#include "b.h"

/*:access bar:*/

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

   return x + y;
}
====
/* a.h */
typedef /*@abstract@*/ int foo;
====
/* b.h */
typedef /*@abstract@*/ int bar;