3

我正在尝试使用 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);
}

我已经阅读了手册，但是关于函数指针及其语义注释的信息并不多，所以我不知道是我做错了什么还是这是某种错误（顺便说一下，这里还没有列出：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，所以它确实有副作用”

4

3 回答 3

1

也许您在分配my_function_pointer. 相反，请尝试以下操作：

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

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

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

于 2011-04-20T19:20:00.630 回答
0

I'm not familiar with splint, but it looks to me that it will check function calls to see if they produce an effect, but it doesn't do analysis to see what a function pointer points to. Therefore, as far as it's concerned, a function pointer could be anything, and "anything" includes functions with no effect, and so you'll continue to get that warning on any use of a function pointer to call a function, unless you so something with the return value. The fact that there's not much on function pointers in the manual may mean they don't handle them properly.

Is there some sort of "trust me" annotation for an entire statement that you can use with function calls through pointers? It wouldn't be ideal, but it would allow you to get a clean run.

于 2011-04-20T15:02:23.310 回答
-1

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

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

于 2011-04-20T14:17:59.690 回答