QAC 8.0 / QAC++ 3.0 以降

QAC 8.0 / QAC++ 3.0 以降のデータフロー解析(DFA)にはクエリタイムアウトと関数タイムアウトの2つのタイムアウトがあります。

ここでは【クエリタイムアウト】について説明します。

DFA の実行中には、コード内の様々な場所でそのコードが問題を引き起こす可能性を Theorem Solver に問い合わせます。この Theorem Solver への問い合わせをクエリと呼びます。

※詳しくは『DFA の仕組み』をご覧ください

Theorem Solverからの応答がクエリタイムアウトの設定値以内に返らない場合、タイムアウトとなります。
クエリタイムアウトは -prodoption オプションを用いてミリ秒単位で設定します。例えば、クエリタイムアウトを1000ミリ秒に設定するには

-prodoption df::query_timeout=1000

と設定します。

QAC / QAC++ は2種類のクエリを使用します。1つ目のクエリがタイムアウトすると、2つ目のクエリが発行されます。QAC 9.1.0 / QAC++ 4.1.0 以降では2つのクエリが両方ともタイムアウトした場合に、クエリタイムアウトメッセージ(メッセージ 2758)が出力されます。

ただし、メッセージ2758が使用する設定であり、かつ -prodoption オプションに

-prodoption df::query_timeout_message+

の設定がある場合です。

メーカーの調査によると、コードの内容や解析にお使いのマシンのスペックにも因りますが、クエリに対する結果が返る場合は、概ね1秒以内に返ってくるという結果が得られています。
言い換えると、1秒で結果が返らないクエリは、タイムアウトする可能性が高いです。
また、1つ目のクエリはタイムアウトするものの、2つ目のクエリはタイムアウトせず解析が続行される場合があります。

そのため、クエリタイムアウトの設定値は長くとも 1000～2000 (ミリ秒) 程度に設定することをお勧めします。 

例：クエリタイムアウト設定値を 10000(10秒)から1000(1秒)に変更した場合