0

生成可能な配列フィールドは常に同じ CFS に属しますか? リスト フィールドの 1 つに制約があり、別のフィールドに別の制約があり、それらが接続されていない場合。両方のフィールドが同じ CFS に属しますか?

4

2 に答える 2

0

質問は完全に明確ではありませんが、ここで答えようとします：

  1. これが複数のフィールドを持つ構造体のリストである場合、異なるフィールドは、接続されている場合にのみ同じ CFS に属します (たとえば、l[0].x と l[0].y は、制約がある場合にのみ同じ CFS に属します)。それらを接続します）。

  2. 質問が同じリスト パスの異なるインデックス (例: l[0].x と l[1].x、または m[0] と m[1]) を参照していると仮定すると、静的とランタイムを区別する必要があります。考慮事項:

静的に、両方のパスが同じ CFS に属していると見なされます。たとえば、ICFS 分析では、「keep x < f(m[0]); keep m[1] < g(x)」で ICFS が作成されると仮定します。

実行時に、パフォーマンス上の理由から、IntelliGen はリスト アイテムを 1 つずつ (異なる CFS にあるかのように) 解決しようとします。ただし、IntelliGen の用語で「レース」と呼ばれるリスト項目が (直接または別の変数に) 接続されている場合、それらは実際には 1 つの CFS として解決され、非常に大きくなる可能性があります。

詳細については、IntelliGen ユーザー ガイドのセクション 4.3 (「リスト要素間の依存関係の回避」) を読むことをお勧めします。

于 2016-02-16T09:41:51.273 に答える