frama-c - frama-c を使用して異なる c ファイル間の依存関係を計算する

Question

異なる c ファイルを含むプロジェクトで変数の依存関係を計算しようとしています。これらの各ファイルにはメイン関数があり、互いに呼び出していません。ただし、それらには共有変数があり、それらの間の最終的な依存関係を計算する必要があります。

たとえば、「File1.c」と「File2.c」の 2 つの c ファイルと、3 つのグローバル変数を定義するヘッダー ファイル「Header.h」があります。

File1.c

#include "header.h"

 void main1(){
   var1 = var2;
 }

File2.c

  #include "header.h"

    void main2(){
      var2 = var3;
    }

Header.h

int var1=1;
int var2=2;
int var3=3;

frama-c で依存関係モジュールを呼び出す場合は、エントリ ポイントを指定する必要があるため、エントリ ポイントとして main1 または main2 を選択する必要があるため、main1.c の依存関係を取得します。

var1 から var2

または main2.c からの依存関係:

var2 から var3

代わりに、両方のファイル間の依存関係を取得したいと思います。

var1 から var3

また、別の関数から呼び出す 2 つのメインをラップしようとしましたが、frama は文字通り「効果なし」と言っています。私が手に入れたいものがframa-cで可能になることを願っています。