ロック lint ユーザーインタフェース

ロック lint との対話の操作には、ソースコードへの注釈の挿入とコマンド行インタフェースの 2 通りの方法が用意されています。

• ソースコードへの注釈の挿入とは、ロック lint に情報を渡すためにソースコード中に置かれるアサーションおよび NOTE です。ロック lint は、コード中の特定のポイントにおけるロックの状態に関するアサーションを検査し、挿入された注釈はロック動作が正しいかどうかの検証や、不要なエラーメッセージの回避に利用されます。

  詳細については、「ソースコードへの注釈の挿入」 の項を参照してください。

• もう 1 つは、ロック lint サブコマンドを使用して、関連 .ll ファイルを読み込み、アサーションを指定する方法です。このロック lint とのインタフェースは、lock_lint コマンドおよび lock_lint コマンド行で指定する一連のサブコマンドから構成されます。

lock_lint サブコマンドの特色を以下に示します。

• 対応する注釈挿入を持たないいくつかの追加制御を実行することができる。

• プログラム中の関数、変数、関数ポインタ、ロックについての便利なクエリーを数多く作成できる。

  ロック lint サブコマンドは、コードを解析し、ロックによって確実に保護されていない変数を発見する手助けとなります。どの変数がロックによって保護され、関数の呼び出し時にはどのロックが確立されるかといった、アサーションを決定することができるでしょう。適切なアサーションの下で、解析を実行することによって、そのアサーションがどこで違反されるかが示されます。

  付録 A 「ロック lint コマンドリファレンス」を参照してください。

ほとんどのプログラマは、コマンド行サブコマンドよりもソースコードへの注釈挿入を好むことが報告されています。しかし、両者の間には必ずしも 1 対 1 の対応関係は存在していないことも事実です。