我想用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
的東西,所以它確實有副作用 - 效果「
您可以使用一個函數指針,就好像它是在一個呼叫的函數名。 '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