如何摆脱警告：“忽略已保存文件中的 1 个状态。在此 Frama-C 配置中无效。”？

Question

在某些情况下，例如使用 Eva 的抽象域时，加载会话总是发出以下形式的警告：

[kernel] Warning: 1 state in saved file ignored. It is invalid in this Frama-C configuration.

例如，下面是如何使用只包含 main 函数 (int main() {}) 的简单 C 文件重现它：

frama-c main.c -eva -eva-domains gauges -save framac.sav
frama-c -load framac.sav

使用frama-c-script make-template生成的模板并在EVAFLAGS中启用抽象域时也会出现警告。

Answer 1

关于忽略已保存文件中的状态的警告大多是无害的。它只是意味着 Frama-C 有（在 -save 期间）一些当前配置 (-load) 中未使用的数据。发生这种情况的主要情况有两种：

1. 加载插件较少的状态时；例如，如果在 -save 之前加载了一些外部插件，但没有在 -load;
之前加载
2. 将 Eva 的替代域与 memexec 一起使用时（默认打开）。 Eva 在每次执行时用启用的域实例化一个仿函数，并且这个仿函数保存在会话文件中。稍后加载时，它会发出消息，可以安全地忽略它。

另一种可能导致此警告的情况是，如果您在保存会话后重新编译 Frama-C，并使用不同的二进制文件重新加载它。会话在不同版本之间不可移植，因此版本检查可以防止意外发生，但是在不更改版本号的情况下重新编译自己时，可能会发生这种情况。在这种情况下，警告应引起注意，重新生成会话文件应将其消除。