我正在尝试将 Frama-C 的价值分析插件作为我项目中的抽象解释后端。特别是，这个项目是关于将一个带有POSIX线程的并发C程序翻译成一个等效的顺序C程序，模拟相应的并发程序，并使用顺序分析工具来分析顺序程序（Cseq）。
该插件确实为我的程序中的变量提供了非常好的近似值。但是，为了使后端工作，需要精确跟踪顺序程序中的一组特定变量，这称为显式值分析（来自本文explicit-value-analysis的影响）。例如，对于表示控制流或上下文切换点的变量，需要在每个语句（特定值）处精确跟踪它们的值，而不仅仅是在枚举或区间中。我想知道 Frama-C 是否提供此功能。如果是这样，如果有人可以帮助我，我将不胜感激。
【问题讨论】：
标签： frama-c
这在 Frama-C 中并不存在。
首先，下面的讨论假设您已经尝试过 Frama-C 的 -slevel 选项并且您正在使用它。
如果您愿意在每次修改重要变量时添加一条语句，您可以将程序更改为这样的：
…
/* original assignment: */
important = important /* already known precisely */ + unimportant;
/* instrumentation: */
tis_variable_split(&important, sizeof important, LIMIT);
…
内置的tis_variable_split 采用刚刚为变量important 计算的值，并根据需要传播尽可能多的抽象状态，在每个状态中为important 分配一个值。
内置的tis_variable_split 没有在 Frama-C 中实现（据我所知），但在 TIS Analyzer 中可用，这是一种基于 Frama-C 的商用静态分析器。您可以联系出售它的公司 TrustInSoft 以获取许可证。免责声明：我在那里工作。
如果你事先知道important可以取的一组值，你可以用析取来模拟同样的效果：
/*@ assert important == value1 || important == value2 || … ; */
断言可能会很快变得笨拙，但由于我们谈论的是自动检测，它只需要小到足以由框架自动生成和处理。 可以修改框架，以便甚至不需要上面的检测步骤。这种修改是可行的，所以你必须准备好更详细地解释你的实验的需要，这样任何可能做这项工作的人都不会浪费他们的时间，你必须准备好分享科学的功劳最终结果，这将是合作的产物。
【讨论】：
assert（第二次解决），但似乎效果不佳。我认为最好在做出选择之前了解更多价值分析背后的基本理论。您能否提供一些关于在价值分析中计算、传播和合并抽象状态以及它们与slevel 选项的关系的参考资料（论文、文章）？
assert 解决方法对应于frama-c.com/download/value-analysis-Neon-20140301.pdf 的第 70 页“案例分析”中记录的断言的用法。为此，断言必须是谓词的析取，这些谓词单独足够简单，以供价值分析利用它们。 important == <value1> 这样的谓词原则上足够简单，前提是值分析能够推断出变量 important 在该点初始化。
slevel 的值与用户断言的关系以及导致状态数量上升的原因？因为在分析的一些日志文件中有一些类似Semantic level unrolling superposing up to 100 states 的信息。谢谢
slevel的问题。谢谢。