frama-c - 用frama-c计算不同c文件之间的依赖关系

Question

我正在尝试计算具有不同 c 文件的项目中的变量依赖关系。这些文件中的每一个都有一个主要功能，并且它们不会相互调用。但是它们有共享变量，我需要计算它们之间的最终依赖关系。

例如，我有两个 c 文件：“File1.c”和“File2.c”以及一个定义三个全局变量的头文件“Header.h”。

文件1.c

#include "header.h"

 void main1(){
   var1 = var2;
 }

文件2.c

  #include "header.h"

    void main2(){
      var2 = var3;
    }

头文件.h

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

如果我在 frama-c 上调用依赖项模块，我必须指定入口点，因此选择 main1 或 main2 作为入口点，所以要么我得到 main1.c 的依赖项：

来自 var2 的 var1

或来自 main2.c 的依赖项：

来自 var3 的 var2

相反，我想获得两个文件之间的依赖关系：

来自 var3 的 var1

我还尝试包装从另一个函数调用它们的两个电源，但 frama 字面意思是“没有影响”。我希望使用frama-c可以实现我想要得到的东西。