如何使用Frama-C追踪变量并切分其关联的所有代码

问题原因 #

你最初使用的-slice-value x参数仅会将x本身的直接使用作为切片保留标准，Frama-C切片器默认不会保留未被标记为需要观测的副作用：由于你没有指定要保留storage数组的修改，切片器判定insert(x, y)调用不会对x的取值产生后续影响，因此直接移除了该调用，最终得到的切片仅保留了x的定义。

无需显式指定函数名的解决方案 #

有两种常用方案可以实现你要的效果：

• 方案一：将关联的副作用对象加入切片标准
  由于insert函数的核心作用是修改全局数组storage，你可以将storage也加入切片的保留目标，命令如下：

  frama-c slice_issue.c -no-frama-c-stdlib -slice-value x -slice-value storage -then-on 'Slicing export' -print
  

  此时切片器会识别出x被用作insert的入参来修改你指定的保留对象storage，会自动保留insert调用，无需手动指定函数名。
• 方案二：调高切片保留等级
  使用-slicing-level 2参数，该等级下切片器会默认保留所有函数调用的可观测副作用，不需要单独指定每个被调用的函数，命令如下：

  frama-c slice_issue.c -no-frama-c-stdlib -slice-value x -slicing-level 2 -then-on 'Slicing export' -print
  

补充说明 #

Frama-C切片的核心逻辑是仅保留与你指定的切片准则相关的代码，默认的低切片等级会尽可能移除无关联的代码，包括看起来没有影响指定目标的函数调用。如果你的场景需要追踪变量跨函数的所有传递路径，调高切片等级或者关联变量的读写对象作为切片准则即可。

内容的提问来源于stack exchange，提问作者Ashfaqur Rahaman