Frama-C WP无法验证带signed int成员的结构体插入函数，但unsigned int可通过验证

我最近在用Frama-C的WP插件验证一个结构体数组插入函数时，碰到了一个很有意思的现象：当结构体Item_t的成员是带符号的int时，WP无法完成所有性质的验证，存在多个未通过的项；但只要把成员类型改成unsigned int，所有验证项就都能顺利通过了。以下是详细情况：

完整的代码实现（含ACSL注解） #

#define mARRAY_LEN(a) ((int)(sizeof(a) / sizeof((a)[0])))

typedef struct {
    int value; // 改成unsigned int时验证通过
} Item_t;

typedef struct {
    Item_t items[10];
    int count;
} Table_t;

/*@ requires \valid(table);
    requires 0 <= index <= table->count;
    requires table->count < mARRAY_LEN(table->items);
    assigns table->items[index..\old(table->count)];
    assigns table->count;
    ensures \forall integer j; 0 <= j < index ==> table->items[j] == \old(table->items[j]);
    ensures \forall integer j; index < j <= \old(table->count) ==> table->items[j] == \old(table->items[j-1]);
    ensures table->items[index] == item;
    ensures table->count == \old(table->count) + 1;
 */
static void tableInsert(Table_t *table, int index, Item_t item) {
    /*@ loop invariant index <= i <= table->count;
        loop invariant \forall integer j; 0 <= j < i ==> table->items[j] == \at(table->items[j], Pre);
        loop invariant \forall integer j; i < j <= table->count ==> table->items[j] == \at(table->items[j-1], Pre);
        loop assigns i, table->items[index+1 .. table->count];
        loop variant i - index;
     */
    for (int i = table->count; i > index; i--) {
        //@ assert(i > 0);
        table->items[i] = table->items[i - 1];
    }
    table->items[index] = item;
    table->count++;
}

当Item_t成员为int时的WP验证输出 #

我使用的验证命令是：

frama-c -wp-verbose 0 -wp Test.c -then -report

输出结果如下：

[kernel] Parsing Test.c (with preprocessing)
[wp] Warning: Missing RTE guards
[report] Computing properties status...
--------------------------------------------------------------------------------
--- Properties of Function 'tableInsert'
--------------------------------------------------------------------------------
[ Partial ] Post-condition (file Test.c, line 21)
  By Wp.typed, with pending:
    - Loop assigns (file Test.c, line 40)
    - Invariant (file Test.c, line 32)
    - Invariant (file Test.c, line 37)
[ Partial ] Post-condition (file Test.c, line 22)
  By Wp.typed, with pending:
    - Loop assigns (file Test.c, line 40)
    - Invariant (file Test.c, line 32)
    - Invariant (file Test.c, line 37)
[ Partial ] Post-condition (file Test.c, line 23)
  By Wp.typed, with pending:
    - Loop assigns (file Test.c, line 40)
    - Invariant (file Test.c, line 32)
    - Invariant (file Test.c, line 37)
[ - ] Post-condition (file Test.c, line 25)
  tried with Wp.typed.
[ Valid ] Exit-condition (generated) by Unreachable Annotations.
[ Partial ] Termination-condition (generated)
  By Trivial Termination, with pending:
    - Loop assigns (file Test.c, line 40)
    - Invariant (file Test.c, line 32)
    - Invariant (file Test.c, line 37)
[ - ] Loop assigns (file Test.c, line 40)
  tried with Wp.typed.
[ - ] Assigns (file Test.c, line 18)
  tried with Wp.typed.
[ Partial ] Loop variant at loop (file Test.c, line 44)
  By Wp.typed, with pending:
    - Loop assigns (file Test.c, line 40)
    - Invariant (file Test.c, line 32)
    - Invariant (file Test.c, line 37)
[ - ] Invariant (file Test.c, line 32)
  tried with Wp.typed.
[ Partial ] Invariant (file Test.c, line 34)
  By Wp.typed, with pending:
    - Loop assigns (file Test.c, line 40)
    - Invariant (file Test.c, line 32)
    - Invariant (file Test.c, line 37)
[ - ] Invariant (file Test.c, line 37)
  tried with Wp.typed.
[ Partial ] Assertion (file Test.c, line 45)
  By Wp.typed, with pending:
    - Loop assigns (file Test.c, line 40)
    - Invariant (file Test.c, line 32)
    - Invariant (file Test.c, line 37)
[ - ] Default behavior tried with Frama-C kernel.
--------------------------------------------------------------------------------
--- Status Report Summary
--------------------------------------------------------------------------------
1 Completely validated
7 Locally validated
6 To be validated
14 Total
--------------------------------------------------------------------------------

当Item_t成员改为unsigned int时的WP验证输出 #

仅修改Item_t的成员类型为unsigned int，执行同样的验证命令，输出结果如下：

[kernel] Parsing Test.c (with preprocessing)
[wp] Warning: Missing RTE guards
[report] Computing properties status...
--------------------------------------------------------------------------------
--- Properties of Function 'tableInsert'
--------------------------------------------------------------------------------
[ Valid ] Post-condition (file Test.c, line 21) by Wp.typed.
[ Valid ] Post-condition (file Test.c, line 22) by Wp.typed.
[ Valid ] Post-condition (file Test.c, line 23) by Wp.typed.
[ Valid ] Post-condition (file Test.c, line 25) by Wp.typed.
[ Valid ] Exit-condition (generated) by Unreachable Annotations.
[ Valid ] Termination-condition (generated) by Trivial Termination.
[ Valid ] Loop assigns (file Test.c, line 40) by Wp.typed.
[ Valid ] Assigns (file Test.c, line 18) by Wp.typed.
[ Valid ] Loop variant at loop (file Test.c, line 44) by Wp.typed.
[ Valid ] Invariant (file Test.c, line 32) by Wp.typed.
[ Valid ] Invariant (file Test.c, line 34) by Wp.typed.
[ Valid ] Invariant (file Test.c, line 37) by Wp.typed.
[ Valid ] Assertion (file Test.c, line 45) by Wp.typed.
--------------------------------------------------------------------------------
--- Status Report Summary
--------------------------------------------------------------------------------
13 Completely validated
0 Locally validated
0 To be validated
13 Total
--------------------------------------------------------------------------------

内容来源于stack exchange