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

Question

我想使用 Splint 来检测具有相同底层类型的 typedefs 之间的隐式转换，例如在以下代码中：

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，但它不会产生任何警告。即使将typedefs 都注释为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 时收到警告，即使使用演员表也是如此。