0

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

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

4

1 回答 1

3

在此代码上运行 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变量，值分析无法表示的关系不变量）。

于 2015-12-26T23:43:25.913 回答