c - 夹板警告 "Statement has no effect"由于函数指针

Question

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

Statement has no effect (possible undected modification through call to unconstrained function my_function_pointer).

Statement has no visible effect --- no values are modified. It may modify something through a call to an unconstrained function. (Use -noeffectuncon to inhibit warning)

这是通过函数指针调用函数引起的。我不喜欢使用 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 不关心赋值和调用是短还是长方式:

    /* 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@*/

我正在寻找的是正确的表达方式:

"this function pointer points to a function which @modifies stuff, so it does have side-effects"

Answer 1

也许您在分配 my_function_pointer 时依赖于从“函数名称”到“函数指针”的隐式转换，从而混淆了 splint。相反，请尝试以下操作:

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

现在您有了显式转换，夹板不需要猜测。

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