Frama C 中的显式值分析
Explicit-value analysis in Frama C
我正在尝试将 Frama-C 的价值分析插件作为我项目中的抽象解释后端。特别是，该项目是关于将具有 POSIX 线程的并发 C 程序转换为模拟相应并发程序的等效顺序 C 程序，并使用顺序分析工具来分析顺序程序 (Cseq)。
该插件确实为我的程序中的变量提供了非常好的近似值。然而，为了使后端工作，需要精确跟踪顺序程序中的一组特定变量，这称为显式值分析（受本文影响explicit-value-analysis）。例如，对于表示控制流或上下文切换点的变量，需要在每个语句（特定值）中精确跟踪它们的值，而不仅仅是在枚举或间隔中。我想知道 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 中可用，TIS Analyzer 是一种基于 Frama-C 的商用静态分析器。您可以联系销售它的公司 TrustInSoft 以获取许可证。免责声明：我在那里工作。
如果你事先知道important可以取的值集，你可以用析取来模拟同样的效果：
/*@ assert important == value1 || important == value2 || … ; */
断言会很快变得笨拙，但由于我们谈论的是自动检测，它只需要足够小以由框架自动生成和处理。
可以修改框架，这样就不需要上面的检测步骤了。这种修改是有效的，所以你必须准备好更详细地解释你的实验的需要，这样任何可能做这项工作的人都不会浪费他们的时间，而且你必须准备好分享科学的功劳最终结果，这将是合作的产物。
我正在尝试将 Frama-C 的价值分析插件作为我项目中的抽象解释后端。特别是，该项目是关于将具有 POSIX 线程的并发 C 程序转换为模拟相应并发程序的等效顺序 C 程序，并使用顺序分析工具来分析顺序程序 (Cseq)。
该插件确实为我的程序中的变量提供了非常好的近似值。然而，为了使后端工作，需要精确跟踪顺序程序中的一组特定变量，这称为显式值分析（受本文影响explicit-value-analysis）。例如，对于表示控制流或上下文切换点的变量，需要在每个语句（特定值）中精确跟踪它们的值，而不仅仅是在枚举或间隔中。我想知道 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 中可用，TIS Analyzer 是一种基于 Frama-C 的商用静态分析器。您可以联系销售它的公司 TrustInSoft 以获取许可证。免责声明：我在那里工作。
如果你事先知道important可以取的值集，你可以用析取来模拟同样的效果：
/*@ assert important == value1 || important == value2 || … ; */
断言会很快变得笨拙，但由于我们谈论的是自动检测，它只需要足够小以由框架自动生成和处理。 可以修改框架，这样就不需要上面的检测步骤了。这种修改是有效的，所以你必须准备好更详细地解释你的实验的需要，这样任何可能做这项工作的人都不会浪费他们的时间，而且你必须准备好分享科学的功劳最终结果，这将是合作的产物。