这在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 || … ; */
该断言可以很快地变得笨拙，但是由于我们正在谈论自动检测，因此它只需要足够小就可以由框架自动生成和处理。可以修改框架，从而甚至不需要上面的检测步骤。进行此修改是可行的，因此您必须准备更详细地说明实验的需求，以便任何人进行这项工作都不会浪费他们的时间，并且您必须准备分享对实验的科学贡献。最终结果，这将成为协作的产物。
本文收集自互联网，转载请注明来源。
如有侵权，请联系[email protected] 删除。
我来说两句