由于函数指针，夹板警告“语句无效”

Question

我正在尝试使用 Splint（在严格模式下）检查 C 程序。我用语义 cmets 对源代码进行了注释，以帮助 Splint 理解我的程序。一切都很好，但我就是无法摆脱警告：

语句无效（可能通过调用不受约束的函数 my_function_pointer 进行未检测到的修改）。

语句没有可见的效果 --- 没有值被修改。它可以通过调用不受约束的函数来修改某些内容。 （使用 -noeffectuncon 禁止警告）

这是由通过函数指针的函数调用引起的。我不喜欢使用no-effect-uncon 标志，而是编写更多注释来修复它。所以我用适当的@modifies 子句装饰了我的typedef，但Splint 似乎完全忽略了它。问题可以简化为：

#include <stdio.h>

static void foo(int foobar)
/*@globals fileSystem@*/
/*@modifies fileSystem@*/
{
    printf("foo: %d\n", foobar);
}

typedef void (*my_function_pointer_type)(int)
/*@globals fileSystem@*/
/*@modifies fileSystem@*/;

int main(/*@unused@*/ int argc, /*@unused@*/ char * argv[])
/*@globals fileSystem@*/
/*@modifies fileSystem@*/
{
    my_function_pointer_type my_function_pointer = foo;
    int foobar = 123;

    printf("main: %d\n", foobar);

    /* No warning */
    /* foo(foobar); */

    /* Warning: Statement has no effect */
    my_function_pointer(foobar);

    return(EXIT_SUCCESS);
}

我已经阅读了manual，但没有太多关于函数指针及其语义注释的信息，所以我不知道是我做错了什么还是这是某种错误（顺便说一句，它尚未在此处列出：http://www.splint.org/bugs.html)。

有没有人成功地用 Splint 在严格模式下检查过这样的程序？请帮我找到让 Splint 开心的方法 :)

提前致谢。

更新 #1： splint-3.1.2（windows 版本）会产生警告，而 splint-3.1.1（Linux x86 版本）不会抱怨。

更新 #2： Splint 不关心分配和调用是 short 还是 long 方式：

    /* assignment (short way) */
    my_function_pointer_type my_function_pointer = foo;

    /* assignment (long way) */
    my_function_pointer_type my_function_pointer = &foo;

    ...

    /* call (short way) */
    my_function_pointer(foobar);

    /* call (long way) */
    (*my_function_pointer)(foobar);

更新#3：我对抑制警告不感兴趣。这很简单：

/*@-noeffectuncon@*/
my_function_pointer(foobar);
/*@=noeffectuncon@*/

我要找的是正确的表达方式：

“这个函数指针指向了一个 @modifies 的函数，所以它确实有副作用”

Answer 1

也许您在分配my_function_pointer 时依赖从“函数名”到“函数指针”的隐式转换而混淆了夹板。相反，请尝试以下方法：

// notice the &-character in front of foo
my_function_pointer_type my_function_pointer = &foo;

现在你有一个显式的转换，夹板不需要猜测。

不过，这只是猜测。我没有测试过。

Answer 2

我不熟悉夹板，但在我看来它会检查函数调用以查看它们是否产生效果，但它不会进行分析以查看函数指针指向的内容。因此，就它而言，函数指针可以是任何东西，并且“任何东西”包括无效的函数，因此您将继续收到有关使用函数指针调用函数的任何警告，除非您这样做有返回值的东西。手册中没有太多关于函数指针的事实可能意味着它们没有正确处理它们。

整个语句是否有某种“相信我”注释，您可以通过指针与函数调用一起使用？这并不理想，但它可以让您顺利运行。

Answer 3

我相信警告是正确的。您将一个值转换为指针，但对它什么也不做。

强制转换只是使值以不同的方式可见；它不会以任何方式改变值。在这种情况下，您已告诉编译器将“foobar”视为指针，但由于您没有对该视图执行任何操作，因此该语句没有执行任何操作（无效）。