时间戳

首页 > 解决方案 > Frama-c - 在 strlen 之前证明“分配”的问题

frama-c - Frama-c - 在 strlen 之前证明“分配”的问题

问题描述

assigns在调用其他分配到 strlen 的函数后，我遇到了证明问题。下面是一个从标准库调用函数的简单示例。功能契约基本上是strcpy需求的副本。

#include <string.h>

/*@ 
    requires valid_string_src: valid_read_string(src);
    requires room_string: \valid(dest+(0..strlen(src)));

    requires separation:
      \separated(dest+(0..strlen(src)), src+(0..strlen(src)));

    assigns dest[0..(strlen(src))];

  */
void mycpy(char *dest, const char *src) {
    strcpy(dest, src);
}

assigns即使与strcpy 匹配， Frama-c 也无法证明mycpy assigns：

Goal Assigns ... (exit):
Let a_0 = « dest@L1 + 0 ».
Let x_0 = L_strlen(µ:Mchar@L1, src@L1).
Let x_1 = 1 + x_0.
Let x_2 = L_strlen(Mchar_0, src@L1).
Assume {
  Have: 0 <= x_2.
  Type: is_sint8_chunk(µ:Mchar@L1).
  (* Heap *)
  Type: (region(dest@L1.base) <= 0) /\ (region(src@L1.base) <= 0) /\
      linked(µ:Malloc@L1) /\ sconst(µ:Mchar@L1).
  (* Goal *)
  When: !invalid(µ:Malloc@L1, a_0, 1 + x_2).
  Stmt { L1:  }
  (* Pre-condition *)
  Have: P_valid_read_string(µ:Malloc@L1, µ:Mchar@L1, src@L1) /\
      valid_rw(µ:Malloc@L1, a_0, x_1) /\
      separated(a_0, x_1, « src@L1 + 0 », x_1).
}
Prove: x_2 <= x_0.

--------------------------------------------------------------------------------
Prover Alt-Ergo 2.3.3: Timeout (Qed:6ms) (10s) (cached).

目标的完整上下文表明它试图证明：L_strlen(Mchar_0, src@L1) <= L_strlen(µ:Mchar@L1, src@L1). 但是，没有关于Mchar_0.

这是什么µ:Mchar@L1和Mchar_0？我如何证明这个分配？

Frama-c 版本：22.0（钛）。

标签： frama-c

解决方案

推荐阅读