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

我对frama-c版本18.0（ar）的行为有些困惑。
给定以下程序：

#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等式域-eva polka等式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处理的，它是在考虑其他目的的情况下编写的。因此，当已知x == y和x相等时，y的特例尚未被写入。这很容易添加。
（考虑到域名，这可能会让人吃惊。当我们有不感兴趣的别名（例如内核添加的临时别名）时，equality域更倾向于启用更多的反向传播。
对于来自停机坪的域名，这更令人惊讶。我修改了你的例子：

  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|]

如您所见，Apar推断了i和j之间的关系（后缀是行号），将b简化为0，但没有将c简化为1。这让我很惊讶，但也解释了你观察到的不精确。它也不适用于八角形域。
我不太熟悉关系域上的抽象转换器，所以这可能是意料之中的，但这确实令人费解。处理关系运算符的代码存在于FrAMAC/伊娃／Pron中，但部分是家庭编写的（它不仅仅是一个简单的停机坪调用）。特别是，它调用减法运算符，并分析结果与0的相等性。很难理解为什么b是精确的而不是c。