gpt4 book ai didi

c - 如何证明 Frama-C + EVA 中非确定性值的简单等式?

转载 作者:太空狗 更新时间:2023-10-29 15:31:12 24 4
gpt4 key购买 nike

我对 Frama-C 18.0 版(Argon)的行为有点困惑。

给定以下程序:

#include <assert.h>
#include <limits.h>


/*@ requires order: min <= max;
assigns \result \from min, max;
ensures result_bounded: min <= \result <= max ;
*/
extern int Frama_C_interval(int min, int max);


int main() {

int i,j;

i = Frama_C_interval(INT_MIN, INT_MAX);

j = i;

assert(j == i);

return 0;
}

我希望使用任何跟踪相等性的抽象域都能很容易地证明该断言。然而,调用

frama-c -eva -eva-equality-domain -eva-polka-equalities foo.c

给予:

[eva] Warning: The Apron domains binding is experimental.
[kernel] Parsing stupid_test.c (with preprocessing)
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization

[eva] using specification for function Frama_C_interval
[eva] using specification for function __FC_assert
[eva:alarm] foo.c:20: Warning:
function __FC_assert: precondition 'nonnull_c' got status unknown.
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
i ∈ [--..--]
j ∈ [--..--]
__retres ∈ {0}

我错过了什么吗?

最佳答案

很有趣。您的示例未由 -eva -eva-equality-domain 处理,它是为其他目的而编写的。因此,当 xy 已知相等时 x == y 的特殊情况尚未写入。这将很容易添加。

(考虑到域的名称,这可能会令人惊讶。当我们有无趣的别名(例如内核添加的临时别名)时,相等域更适合启用更多的向后传播。)

关于来自 Apron 的域,这更令人惊讶。我这样修改了你的例子:

  j = i;

int b = j - i;
int c = j == i;
Frama_C_dump_each_domain();

运行 frama-c -eva -eva-polka-equalities foo.c -value-msg-key d-apron 得到以下结果:

[eva] c/eq.c:23: 
Frama_C_dump_each_domain:
# Cvalue domain:
i ∈ [--..--]
j ∈ [--..--]
b ∈ {0}
c ∈ {0; 1}
__retres ∈ UNINITIALIZED
# Polka linear equalities domain:
[|-i_44+j_45=0; b_46=0|]

可以看到,Apron已经推断出ij(后缀为行号)之间的关系,将b简化为0,但没有将 c 简化为 1。这让我感到惊讶,但解释了您观察到的不精确性。它不适用于八边形域。

我不太熟悉关系域上的抽象转换器,所以这可能是预料之中的,但这确实令人费解。处理关系运算符的代码存在于 Frama-C/Eva/Apron 中,但部分是自己编写的(它不仅仅是对 Apron 原语的简单调用)。特别是,它调用减法运算符,并分析结果与 0 是否相等。很难理解为什么 b 是精确的而 c 不是。

关于c - 如何证明 Frama-C + EVA 中非确定性值的简单等式?,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/56175449/

24 4 0
Copyright 2021 - 2024 cfsdn All Rights Reserved 蜀ICP备2022000587号
广告合作:1813099741@qq.com 6ren.com