多个函数调用，依赖关系混淆

Question

在使用 Frama-C 时，我遇到了一些奇怪的依赖关系。当函数被多次调用并且指针作为参数传递时，就会发生这些情况。以下代码将问题分解为最小值：

int sourceA = 1, sourceB = 1;
int targetA, targetB;

int deref_ptr(int* ptr){
    return *ptr;
}

int main(int argc, char* argv[]){

    targetA = deref_ptr(&sourceA);
    targetB = deref_ptr(&sourceB);

    return 0;
}

Frama-C 使用 EVA 插件计算以下依赖关系。

[kernel] Parsing test.c (with preprocessing)
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
  sourceA ∈ {1}
  sourceB ∈ {1}
  targetA ∈ {0}
  targetB ∈ {0}
[eva] done for function main
[eva:summary] ====== ANALYSIS SUMMARY ======
  ----------------------------------------------------------------------------
  2 functions analyzed (out of 2): 100% coverage.
  In these functions, 6 statements reached (out of 6): 100% coverage.
  ----------------------------------------------------------------------------
  No errors or warnings raised during the analysis.
  ----------------------------------------------------------------------------
  0 alarms generated by the analysis.
  ----------------------------------------------------------------------------
  No logical properties have been reached by the analysis.
  ----------------------------------------------------------------------------
[from] Computing for function deref_ptr
[from] Done for function deref_ptr
[from] Computing for function main
[from] Done for function main
[from] ====== DEPENDENCIES COMPUTED ======
  These dependencies hold at termination for the executions that terminate:
[from] Function deref_ptr:
  \result FROM sourceA; sourceB; ptr
[from] Function main:
  targetA FROM sourceA; sourceB
  targetB FROM sourceA; sourceB
  \result FROM \nothing
[from] ====== END OF DEPENDENCIES ======

主要功能的依赖关系在这里很有趣。预期是 targetA 依赖于 sourceA，而 targetB 依赖于 sourceB。但除此之外，Frama-C 还计算来自 deref_ptr 函数的相应其他调用的依赖关系。是否可以影响此行为，使 targetA 仅依赖于 sourceA（targetB 和 sourceB 相同）？

Answer 1

拥有启动时使用的确切命令行会有所帮助 Frama-C。从结果来看，这可能是 frama-c -deps example.c，但请注意，您使用的选项的详细信息通常很重要。

也就是说，-deps确实合并了来自每个函数的所有调用的信息。但是，如果您查看 frama-c -from-help，您会注意到还有另一个用于计算依赖项的选项：-calldeps，其描述为：

force callsite-wise dependencies (opposite option is -no-calldeps)

确实，frama-c -calldeps example.c 给了你想要的结果：

[from] ====== DISPLAYING CALLWISE DEPENDENCIES ======
[from] call to deref_ptr at example.c:10 (by main):
  \result FROM sourceA; ptr
[from] call to deref_ptr at example.c:11 (by main):
  \result FROM sourceB; ptr
[from] entry point:
  targetA FROM sourceA
  targetB FROM sourceB
  \result FROM \nothing
[from] ====== END OF CALLWISE DEPENDENCIES ======

多个函数调用，依赖关系混淆

Multiple function call, dependencies mix up

frama-c