夹板警告“声明无效”由于函数指针

Question

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

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

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

这是由通过函数指针进行函数调用引起的。我不想使用 no-effect-uncon 标志，而是编写更多注释来修复它。因此，我用适当的 @modizes 子句装饰了我的 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);
}

我已阅读手册，但信息不多关于函数指针及其语义注释，所以我不知道我是否做错了什么或者这是某种错误（顺便说一句，它还没有在这里列出： 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：< /strong> 我对禁止警告不感兴趣。这很简单：

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

我正在寻找的是表达以下内容的正确方式：

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

Answer 1

我相信警告是正确的。您将一个值转换为指针，但不对其执行任何操作。

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

Answer 2

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

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

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

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

Answer 3

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

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