exit 関数・ return 関数の取り扱い

ことが可能となってしまうのである。注意すべき点がここにある。もし、バイナリモデル 検査が開始され、検査環境Cプログラムがexit関数を呼び出すと、検査用に動作してい るCプログラムpanまで終了してしまうのである。検査プログラムにとっては、予期し ない終了であるため反例結果も得ることができず検査が失敗してしまう。return関数につ いても同様でc code内でreturn関数を呼び出すとpanが終了してしまう。しかし、exit 関数と異なりc code内で呼び出した関数内で返り値を返す際に使われる分には問題がな い。つまり、panを終了させるような使われ方がされていなければ問題はない。以後、説 明で取り上げるreturn関数はpanを終了させてしまうreturn関数のことであるとする。

そこで、この問題の解決策としてexit関数とreturn関数を呼び出すような記述が検査 対象のプログラムにあった場合は以下のように対処する。

ˆ 手順

– c code内に直接、exit関数あるいはreturn関数が記述されていた場合：exit関 数あるいはreturn関数をPromelaのassert(false)に置き換える。どうしても 検査をその段階で止めたくない場合(正常終了なので反例は出したくない場合 など)は、適切なPromela記述と置き換える。

– c code内で呼び出すC関数が内部でexit関数を呼んでいる場合：そのC関数

のexit関数をコメントアウトしてしまい、エラー終了の旨を返り値として返す ようにC関数を変更する。またはCの大域変数を作成しフラグとして利用し、

Promelaから関数の状態を判定できるようにする。そして、Promela側で エラー値を処理し、エラーであったらPromelaのassert(false)に遷移するよ うに記述する。

以上の対処方法に基づいて、lsプログラムの検査ではどのように実装したかを説明する。

ˆ lsプログラム検査での実装手順

– c code内に直接、exit関数あるいはreturn関数が記述される場合の最も典型

的な例はCプログラム終了時の呼び出しである。lsプログラムの検査に際し ても、このことは当然あてはまる。よって、lsプログラムにはあるプログラム 終了時のexit関数はPromelaにはない。また、正常終了の遷移であるため assert(false)も記述していない。

– 図3.24では、直前で呼び出した関数の終了時の状態を表す値であるPtest → resultをc exprで判定している。もし、Ptest →resultがエラー値を示せば、

メッセージを出力した後にPromelaのassert(false)に遷移するようCソース を変更した。このようにすることで、関数の動作による検査プログラムの予期 せぬ終了を阻止している。

図 3.23: exit関数置き換えイメージ

¶ ³

1 if

2 ::c_expr{Ptest->result == -1} ->

3 c_code{printf("Error cnt_dir function");};

4 assert(false);

5 ::c_expr{Ptest->result == 0} ->

6 c_code{printf("No File");};

7 assert(false);

8 ::else -> skip;

9 fi;

µ ´

図 3.24: C変数の値を条件にassertに遷移するよう変更した例