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

Question

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

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即使将两个s都注释为abstract也不会触发它。

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

Answer 1

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

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时收到警告，即使使用演员表也是如此。