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 を使用して、このようなプログラムを正常にチェックできた人はいますか? 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 に答える