frama-c值分析自动加宽

Question

我正在寻找一种在没有用户提示的情况下对循环执行扩展的方法。我将用一个例子来解释：

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 中执行此操作？

Answer 1

When running frama-c value analysis on this code, the global variable z receives the interval [--,--].

不，它没有：

~ $ 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 的值的关系不变量，值分析无法表示的关系不变量）。

frama-c值分析自动加宽

Automatic widening in frama-c value analysis

c

frama-c

abstract-interpretation