2011-04-20 109 views
3

我想用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的東西,所以它確實有副作用 - 效果「

回答

-1

我相信警告是正確的。你正在將一個值作爲一個指針來投入,但卻無所作爲。

一個演員只是使值以不同的方式顯示;它不會以任何方式更改值。在這種情況下,你已經告訴編譯器將「foobar」視爲一個指針,但由於你沒有對該視圖進行任何操作,所以該語句沒有做任何事情(沒有任何效果)。

+0

您可以使用一個函數指針,就好像它是在一個呼叫的函數名。 'my_function_pointer'是一個指向函數的指針,它接受一個int並返回void。 – 2011-04-20 14:39:46

+0

我沒有投入價值;我[通過函數指針調用函數](http://www.newty.de/fpt/fpt.html#call)。在這個特定的情況下,我通過'my_function_pointer'調用函數'foo'。 – 2011-04-20 15:35:11

+0

我的不好。最後我錯過了缺失的「_type」。 – 2011-04-21 06:43:45

0

我不熟悉splint,但它在我看來它會檢查函數調用以查看它們是否產生效果,但它不會執行分析來查看函數指針指向什麼。因此,只要我們關心的,一個函數指針可以是任何東西,和「什麼」包括沒有效果的功能,所以你會繼續得到任何使用函數指針的警告調用一個函數,除非你這麼與返回值的東西。手冊中沒有太多關於函數指針的事實可能意味着它們不能正確處理它們。

是否有某種「相信我」的註釋爲,您可以使用函數通過指針調用使用整個語句?這不太理想,但它可以讓你得到一個乾淨的運行。

+0

我知道如何_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

1

也許你在使用my_function_pointer時,依賴於從「函數名稱」到「指向函數的指針」的隱式轉換,令人困惑。相反,請嘗試以下操作:

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

現在您已經進行了明確的轉換並且不需要夾板。

這只是猜測,但。我沒有測試過它。

+0

不,它不起作用。我已經嘗試過,斯普林特不斷抱怨。我甚至嘗試瞭解引用函數指針(像這樣:'(* my_function_pointer)(foobar);'),但後來又發出了一個警告:'可能越界讀取:* my_function_pointer'。不管怎麼說,還是要謝謝你 :) – 2011-04-20 19:36:58