使用Frama-C验证线性搜索

Question

我再次对一个简单的验证工作感到困惑,这一次是在使用WP插件的Frama-C(Sodium)中,因为我无法让Jessie在uni工作站上工作(在由管理人员/团队安装的过程中) .)我一直在阅读'ACSL by example'和手册.虽然我认为这个例子很简单,但很快就能正确行事.在使用Dafny和Whiley验证相同的算法后,我可能会变得有点污点.

#include <stdio.h>
// A linear search over a sorted array looking for a given element.

/*@ requires len > 0;
  @ requires \valid( ls+ ( 0..(len - 1) ) );
  @ requires \forall size_t k; 0 <= k < (len - 1) ==> ls[k] <= ls[k + 1];
  @ assigns \nothing;
  @ behavior found:
  @   assumes \exists size_t k; 0 <= k < len && ls[k] == item;
  @   ensures \result >= 0;
  @ behavior nfound:
  @   assumes \forall size_t k; 0 <= k < len ==> ls[k] != item;
  @   ensures \result == -1;
  @ complete behaviors found, nfound;
  @ disjoint behaviors found, nfound;
  */
int search( int ls[], const size_t len, int item )
{
  size_t i = 0;

  /*@ loop invariant 0 <= i <= len;
    @ loop invariant \forall size_t k; 0 <= k < i ==> ls[k] != item;
    @ loop assigns i;
    @ loop variant len - i;
    */
  while ( i < len )
  {
    if ( ls[i] == item )
      return i;
    ++i;
  }
  return -1;
}

int main()
{
  int src[] = { 1, 2, 3, 4, 5, 6, 7, 8, 9, 10 };
  if ( search( src, 10, 5 ) >= 0 ) printf( "found item" );
  else printf( "no item found" );
}

和我在尝试验证时得到的输出是:

$ frama-c -pp-annot -wp -wp-rte -wp-timeout 100 search.c    
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing search.c (with preprocessing)
/tmp/ppannot97a491.c:1:0: warning: "__STDC_VERSION__" redefined
 #define __STDC_VERSION__ 201112L
 ^
<built-in>: note: this is the location of the previous definition
/tmp/ppannot97a491.c:2:0: warning: "__STDC_UTF_16__" redefined
 #define __STDC_UTF_16__ 1
 ^
<built-in>: note: this is the location of the previous definition
/tmp/ppannot97a491.c:3:0: warning: "__STDC_UTF_32__" redefined
 #define __STDC_UTF_32__ 1
 ^
<built-in>: note: this is the location of the previous definition
[wp] Running WP plugin...
[wp] Collecting axiomatic usage
[rte] annotating function main
[rte] annotating function search
[wp] 20 goals scheduled
[wp] [Qed] Goal typed_main_call_search_pre : Valid
[wp] [Qed] Goal typed_main_call_search_pre_2 : Valid
[wp] [Alt-Ergo] Goal typed_search_complete_found_nfound : Valid (10ms) (19)
[wp] [Alt-Ergo] Goal typed_search_loop_inv_preserved : Valid (17ms) (21)
[wp] [Alt-Ergo] Goal typed_search_disjoint_found_nfound : Valid (13ms) (19)
[wp] [Qed] Goal typed_search_loop_inv_established : Valid
[wp] [Qed] Goal typed_search_loop_inv_2_established : Valid
[wp] [Alt-Ergo] Goal typed_main_call_search_pre_3 : Valid (383ms) (93)
[wp] [Alt-Ergo] Goal typed_search_loop_inv_2_preserved : Valid (17ms) (33)
[wp] [Qed] Goal typed_search_loop_assign : Valid
[wp] [Alt-Ergo] Goal typed_search_assert_rte_mem_access : Valid (50ms) (89)
[wp] [Alt-Ergo] Goal typed_search_assert_rte_unsigned_overflow : Valid (13ms) (30)
[wp] [Qed] Goal typed_search_assign_part1 : Valid
[wp] [Qed] Goal typed_search_assign_part2 : Valid
[wp] [Qed] Goal typed_search_assign_part3 : Valid
[wp] [Qed] Goal typed_search_assign_part4 : Valid
[wp] [Qed] Goal typed_search_loop_term_decrease : Valid (3ms)
[wp] [Qed] Goal typed_search_loop_term_positive : Valid
[wp] [Alt-Ergo] Goal typed_search_nfound_post : Valid (17ms) (33)
[wp] [Alt-Ergo] Goal typed_search_found_post : Unknown (54.3s)
[wp] Proved goals:   19 / 20
     Qed:            11  (3ms-3ms)
     Alt-Ergo:        8  (10ms-383ms) (93) (unknown: 1)

Answer 1

这让我困惑了一段时间,但在尝试了Coq证明之后,我发现你无法证明这种found行为的原因只是......这是不正确的.也就是说,对于len > INT_MAX和在阵列item的INT_MAX第一个单元格中找不到但在某个地方稍后出现的结果,结果int将被视为负数.

从技术上讲,这是实现定义,如C99,6.3.1.3§3中所述:

否则,新类型将被签名,并且值无法在其中表示; 结果是实现定义的,或者引发实现定义的信号.

如果将该选项添加-warn-signed-downcast到命令行,您将看到一个新的RTE生成的断言,但未经证明:

     /*@ assert rte: signed_downcast: i ? 2147483647; */

然后在found假设所述断言成立的情况下证明行为的后置条件.