c - 由于功能指针，夹板警告“声明无效”

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

语句无效(通过调用不受约束的函数my_function_pointer可能会进行非预期的修改)。

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

这是由通过函数指针进行的函数调用引起的。我不想使用no-effect-uncon标志，而是写一些更多的注释来修复它。因此，我使用适当的typedef子句装饰了@modifies，但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成功检查了这样的程序？请帮助我找到使夹板快乐的方法:)

提前致谢。

更新＃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@*/

我正在寻找表达的正确方法:

“此函数指针指向一个包含@modifies的函数，因此它确实有副作用”

最佳答案

也许您在my_function_pointer的分配中依靠从“函数名”到“指针到函数”的隐式转换而使夹板感到困惑。相反，请尝试以下操作:

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

现在您有了一个明确的转换，夹板不需要猜测。

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