Splint警告“声明没有效果”，由于功能指针

我想用Splint（严格模式）检查一个C程序。我使用语义注释注释了源代码，以帮助Splint 了解我的程序。一切都很好，但我就是无法摆脱一个警告：Splint警告“声明没有效果”，由于功能指针

声明没有效果（通过调用函数不受约束可能my_function_pointer修改undected）。

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

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

#include <stdio.h> 

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

typedef void (*my_function_pointer_type)(int) 
/*@globals [email protected]*/ 
/*@modifies [email protected]*/; 

int main(/*@[email protected]*/ int argc, /*@[email protected]*/ char * argv[]) 
/*@globals [email protected]*/ 
/*@modifies [email protected]*/ 
{ 
    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在严格模式下检查这样的程序？请帮我找到让斯普林特高兴的方法:)

在此先感谢。（windows版本）会产生警告，而splint-3.1.1（Linux x86版本）并不会抱怨它。

更新＃2：夹板并不关心分配和调用是否短或长方式：

/* 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：我没兴趣禁止的警告。这很简单：

/*@[email protected]*/ 
my_function_pointer(foobar); 
/*@[email protected]*/

什么我要找的是正道来表达：

“这个函数指针指向一个函数，它@modifies的东西，所以它确实有副作用 - 效果“

来源

2011-04-20 Guillermo Calvo

-1

我相信警告是正确的。你正在将一个值作为一个指针来投入，但却无所作为。

一个演员只是使值以不同的方式显示;它不会以任何方式更改值。在这种情况下，你已经告诉编译器将“foobar”视为一个指针，但由于你没有对该视图进行任何操作，所以该语句没有做任何事情（没有任何效果）。

来源

2011-04-20 14:17:59

您可以使用一个函数指针，就好像它是在一个呼叫的函数名。 'my_function_pointer'是一个指向函数的指针，它接受一个int并返回void。 – 2011-04-20 14:39:46

我没有投入价值;我[通过函数指针调用函数]（http://www.newty.de/fpt/fpt.html#call）。在这个特定的情况下，我通过'my_function_pointer'调用函数'foo'。 – 2011-04-20 15:35:11

我的不好。最后我错过了缺失的“_type”。 – 2011-04-21 06:43:45

我不熟悉splint，但它在我看来它会检查函数调用以查看它们是否产生效果，但它不会执行分析来查看函数指针指向什么。因此，只要我们关心的，一个函数指针可以是任何东西，和“什么”包括没有效果的功能，所以你会继续得到任何使用函数指针的警告调用一个函数，除非你这么与返回值的东西。手册中没有太多关于函数指针的事实可能意味着它们不能正确处理它们。

是否有某种“相信我”的注释为，您可以使用函数通过指针调用使用整个语句？这不太理想，但它可以让你得到一个干净的运行。

来源

2011-04-20 15:02:23

我知道如何_inhibit_警告： /* @ - @ noeffectuncon */ my_function_pointer（foobar的）; /* @ = noeffectuncon @ */ 但我想这样做_The权way_。事实是，Splints接受： typedef void（* my_function_pointer_type）（int） /* @ globals fileSystem @ */ /* @修改fileSystem @ * /; 所以很显然，'my_function_pointer_type'是一个**函数**指针（因为它'@修改了某些东西）。但后来，Splint没有考虑到这一点，并告诉我函数指针不会有任何影响。 – 2011-04-20 15:38:49

也许你在使用my_function_pointer时，依赖于从“函数名称”到“指向函数的指针”的隐式转换，令人困惑。相反，请尝试以下操作：

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

现在您已经进行了明确的转换并且不需要夹板。

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

来源

2011-04-20 19:20:00 Philip

不，它不起作用。我已经尝试过，斯普林特不断抱怨。我甚至尝试了解引用函数指针（像这样：'（* my_function_pointer）（foobar）;'），但后来又发出了一个警告：'可能越界读取：* my_function_pointer'。不管怎么说，还是要谢谢你：） – 2011-04-20 19:36:58

Splint警告“声明没有效果”，由于功能指针

回答

相关问题