一部の契約を静的分析から簡単に除外できますか？

Question

静的アナライザーが証明できないことがわかっている特定の契約があります。特定の種類の契約違反エラーを関数全体から除外できますが、これは広すぎます。 baseline.xml機能を使用して特定の違反エラーを除外することはできますが、チーム環境での監査や文書化は本質的に不可能です。要するに

、それは静的アナライザの行き止まりのように見えるサードパーティライブラリで作られた特定の契約もあります

Contract.Requires(DoesHalt() == true, ExcludeFromStaticAnalysis=true);

ような何かを行うことが可能です。私は静的解析のためにそれらを無効にしたいと思います。 1つの好きな例は、.NETグラフライブラリに構築された契約です。グラフ内のどの頂点で検索を開始するかを指定する深さ第1探索関数への引数は、その頂点がグラフのメンバーであることを要求するContract.Requiresを有する。賢明な契約、おそらくデバッグビルドで実行する価値はありますが、静的に証明されるのは遠いです。しかし、私が深さの最初の検索を使用するたびに、静的な違反を無視する方法を見つけなければなりません。 （Contract.Assumeで解決できません）

不確かなものから証明可能なものを分割する機能がなければ、小さなクリーンなコードベースであっても静的解析が単純すぎるほど騒々しくなることがわかります。

Answer 1

静的解析では、これを行う方法はわかりません。ランタイムチェッカーには、これが可能なカスタムランタイムがありますが、スタティックチェッカーにはありません。

"ベースライン機能"を利用することができます。静的チェッカーが特定の時間にあなたに与えるすべての警告を非表示にすることができます。これらの警告は、ベースライン機能をオフにするまで、XMLファイルに収集されます。

これにより、既存のコードベースの静的チェッカーのノイズを大幅に削減できます。