如何触发Splint的抽象类型检查器？

Question

我想使用Splint来检测具有相同底层类型的typedef之间的隐式强制转换，如以下代码所示：

typedef int counter;
typedef int delta;

static int func(int a, int b, int c)
{
    return a + b + c;
}

int main(void)
{
    int a = 5;
    counter b = a;
    delta c = (int) 8;
    return func(a, b, c);
}

看起来我可以使用Splint来做这件事，但是它不会产生任何警告。即使将两个typedef都注释为abstract也不会触发它。

如何让Splint像这样进行“强”类型检查？

Answer 1

由于您在声明这些类型的同一文件中使用这些类型，因此Splint假定该文件可以访问抽象类型。您需要使用@noaccess@告诉Splint该文件不能访问抽象类型的内部结构。例如，您可以这样做

typedef /*@abstract@*/ int counter; /*@noaccess counter@*/
typedef /*@abstract@*/ int delta; /*@noaccess delta@*/

int main(void)
{
  int a = 5;
  counter /*@unused@*/ b = a;
  delta /*@unused@*/ c = (int) 8;
  return 0;
}

请注意，您不仅会在赋值给b时收到警告，而且还会给c赋值，即使是在强制转换的情况下也是如此。