frama-c - Frama-C での影響分析の使用

Question

使用してみframa-c-guiましたが、影響分析を実行できましたが、Frama-C のバッチ モードで影響分析を実行する必要があるステートメント番号を渡す方法がわかりません。

Answer 1

//@ impact pragma stmt;注釈に続くステートメントの影響に関心があることを示すために使用できる特別な注釈があります。次に、上記の注釈が functionfにある場合は、次のコマンド ラインを使用して、影響を受けるコードをコマンド ラインに出力できます。

frama-c -impact-pragma f -impact-slicing impact.c -then-on "impact slicing" -print

• -impact-pragma f関数のプラグマによってフラグが立てられたステートメントに関心があることを示しますf
• -impact-slicingimpact slicingは、選択したステートメントによって影響を受けるステートメントを含むという名前のプロジェクトを作成することを示します。
• -then-on "impact-slicing"プロジェクトの分析を続けましょうimpact slicing（ここで-printはコードのみですが、後に好きなオプションを付けることができます-then-on project_name）

ただし、impactプラグインは非常に実験的なものであることに注意してください。