frama-c 值分析中的自动扩展答案

【问题标题】：Automatic widening in frama-c value analysisframa-c 值分析中的自动扩展
【发布时间】：2016-04-01 02:31:21
【问题描述】：

我正在寻找一种在没有用户提示的情况下对循环进行加宽的方法。我会用一个例子来解释：

int z;
void main(void) {   
    int r = Frama_C_interval(0, MAX_INT);
    z = 0;
    for (int y=0; y<r; y++)
        z++;
}

在这段代码上运行frama-c值分析时，全局变量z接收区间[--,--]。因为z被设置为零并且循环由增量运算符组成，所以自动扩大方法应该能够推断出更准确的区间是[0，--]。在 Frama-C 中可以做到这一点吗？

【问题讨论】：

标签： c frama-c abstract-interpretation

【解决方案1】：

在这段代码上运行frama-c值分析时，全局变量z接收区间[--,--]。

不，它没有：

~ $ frama-c -version ; echo
Magnesium-20151001+dev
~ $ cat t.c
#define MAX_INT 0x7fffffff

int z;
void main(void) {   
    int r = Frama_C_interval(0, MAX_INT);
    z = 0;
    for (int y=0; y<r; y++)
        z++;
}
~ $ frama-c -val t.c
…
t.c:8:[kernel] warning: signed overflow. assert z+1 ≤ 2147483647;
…
[value] Values at end of function main:
  z ∈ [0..2147483647]
…

这是一个开发版本，但同样适用于任何版本，因为签名溢出开始被视为带有 ACSL 警报的严重错误。如果您使用的版本是在假设有符号溢出无害地产生 2 的补码结果时使用的，1）您应该升级，已经有好几年了，2）z 很难被认为是微不足道的积极因素（尽管它是积极的，因为在循环执行时链接z 和y 的值的关系不变量，值分析无法表示的关系不变量。

【讨论】：