sec2 - Splint翻訳 Wiki - Splint翻訳

Up: マニュアル

Prev: 1 Operation（操作）

Next: 3 Undefined Values（未定義の値）

Section：1　2　3　4　5　6　7　8　9　10　11　12　13　14　A　B　C　D　E

2 Null Dereferences（NULLポインタへの値の参照）

プログラムエラーの一般的な原因は、 nullポインタが参照されるときです。 Splintはインタフェースの境界にてNULLの可能性のあるポインタを識別することによってこれらのエラーを発見します。

nullアノテーションは ポインタの値がNULLである可能性があることを示すために使用されます。 nullアノテーションが 宣言されていないポインタはNULLではない場合があります。 nullチェックが有効になった場合（nullにより制御される） Splintはnullの可能性のあるポインタがパラメータとして渡されたり、戻り値として返されたり、 もしくはnull修飾子のない 外部参照へ割り当てられたりしたとき、エラーを報告します。

ポインタがnullアノテーション付きで宣言された場合、 ポインタ（又は、nullアノテーションが無い値として渡されたか戻されたポインタ）の参照先へアクセスする全ての経路で NULLではないことをコードはチェックしなければなりません。 nullの可能性のあるポインタへ参照する際は、ポインタがNULLでは無いことを チェックする条件文かアサーション（assertions）（どのような'assert'が宣言されているかはSection 8.1を見てください。 ）によって保護されている可能性があります。

図2でのfirstCharの2つの実装を考えます。firstChar1の場合、 Splintは参照されているポインタがnullアノテーションで宣言されているため エラーを報告します。 firstChar2の場合、関数が戻る場合はs == NULLの分岐が真（true）のためsがNULL では無いときだけsの参照がされるため、エラーは報告されません。

null.c	Running Splint
char firstChar1 (/*@null@*/ char *s) { 3  return *s; }   char firstChar2 (/*@null@*/ char *s) {    if (s == NULL) return ‘’; 9  return *s; }	> splint null.c Splint 3.0.1   null.c: (in function firstChar1) null.c:3:11: Dereference of possibly null pointer s: *s    null.c:1:35: Storage s may become null   Finished checking --- 1 code warning found

図 2.  Nullチェック Splintを走らせた出力は sans-serif フォントで表示しています。 コマンドラインは >が前につき、残りはSplintからの出力です。 コードやsplintの出力に追加される説明はイタリックで表示します。 このドキュメント内の図で示されるコードはSplintのウェブサイト http://www.splint.org から利用可能です。 9行目に対してはエラーは報告されません。なぜなら、 s がnullではない場合のみ、参照を行うためです。 図の多くに対して、短縮された出力を得るため、 -linelen 55 -hints –showcol オプションが、 エクスポートされた宣言についての警告を禁止するため –exportlocal オプションが 使用されています。

2.1.1 Predicate Functions（叙述関数）

（訳注：叙述関数とは戻り値の型がbool型の関数のこと）

nullへの参照を保護するもう１つの方法は、nullwhentrue、又は、falsewhennull（これらのアノテーションは元々はfalsenullとtruenullであり、論理非対称性をはっきりさせるために名前を変更されましたが、falsenullとtruenullは未だに使用されている可能性があります）を使用して関数を宣言し、nullアノテーションが付いたポインタへの参照をする前に 条件文にてその関数を呼ぶことです。

nullwhentrueでアノテーションされた関数が真（true）で返るとき最初に渡された引数がNULLであることを意味します。 偽（false）で返る場合、パラメータはNULLではありません。NULLではないパラメータに対して真（true）が返っても良いことに注意してください。 nullwhentrueに対するより説明的な名称は「結果が偽（false）の場合、パラメータはnullではない。」です。例えば、isNullが以下のように宣言されたていた場合、

/*@nullwhentrue@*/ bool isNull (/*@null@*/ char *x);

我々はfirstChar2を以下のように書くことができます。

   char firstChar2 (/*@null@*/ char *s)
   {
      if (isNull (s)) return '\0';
      return *s;
   }

isNull(s)が偽（false）のときのみsへの参照が行われるため、エラーは報告されません。isNullがnullwhentrueアノテーション付きで宣言されているため、sはnullにならないことを意味します。

falsewhennullアノテーションは完全に論理的にnullwhentrue の逆というわけではありません。 falsewhennullで宣言された関数が 真（true）を返した場合、それは明確にパラメータがNULLではないことを意味します。もし、偽（false）を返した場合、パラメータはNULLかもしれませんし、そうではないかもしれません。 つまり、falsewhennullはNULLパラメータが渡されたときは常に偽（false）を返します。NULLではないパラメータが渡されたときはときどき偽（false）が返るかもしれません。

例えば、我々は、パラメータがNULLではなく、かつ、NULL終端文字の前に 最低1文字以上ある場合に真（true）を返すisNonEmptyを定義できます。

   /*@falsewhennull@*/ bool isNonEmpty (/*@null@*/ char *x)
   {
      return (x != NULL && *x != ‘\0’);
   }

Splintはnullwhentrueもしくはfalsewhennullで宣言された関数の実装がアノテーションと一致していることをチェックしません。 しかし、関数を呼ぶコードがチェックされるときに、アノテーションが正しいと仮定します。

2.1.2 Notnull Annotations（Notnullアノテーション）

notnullアノテーションは宣言が明確にNULLではないことを示します。 デフォルトではこれが指定されます。しかし、型宣言上でnullを上書きするためにnotnullを使用する必要がある場合があります。 nullアノテーションは型の全てのインスタンスがNULLでも良いことを示すために型宣言にて使用される場合があります。 nullを使用して宣言されている型の 宣言に対して、型定義中のnullアノテーション はnotnullで無効にされます。 関数が呼び出されるか、決してNULLにならないことが知られている関数の結果の前にnullテストが既に完了している 抽象型（Section 4.3参照）のstatic（静的な）操作を隠すために これは特に便利です。 抽象型に対して、notnullフラグは 外部関数への引数に対して使用されないでしょう。なぜなら、 クライアントは具象実表現がNULLで良い場合かどうかに気づくべきではないためです。 実装モジュール内での静的関数への引数は、しかしながら、notnullを使用して宣言されるでしょう。 実表現がアクセス可能である場所からのみ呼ばれることが出来るためです。static、あるいは外部関数に対する戻り値はnotnullを使用して宣言されてもかまいません。

2.1.3 Relaxing Null Checking（NULLチェックの緩和）

追加のアノテーション、relnullはnullチェックを緩くするために使用することができます。 relnull値の参照先にアクセスする際、もしくは、nullの可能性のある値がrelnullを使用して宣言された識別子に 割り当てられた場合、エラーは報告されません。

これは一般的に他のいくつかの制約に依存しているnullであっても無くても良い 構造体のフィールドに対して使用されます。NULLがrelnull参照へ割り当てられた場合、あるいはrelnull参照が参照先にアクセスされた場合、 Splintは報告やエラーを出しません。 ポインタの参照先にアクセスする前にこの制約が満足していることを保障するのは プログラマの責任です。

このドキュメントはSplint(英)のサイトを元に作成しました

Up: マニュアル

Prev: 1 Operation（操作）

Next: 3 Undefined Values（未定義の値）