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);
}

Frama-c未能证明assigns对于 mycpy 即使它匹配assignsstrcpy 的：

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([email protected] /cdn-cgi/l/email-protection) <= 0) /\ (region([email protected] /cdn-cgi/l/email-protection) <= 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 and Mchar_0？我如何证明这个分配？

Frama-c 版本：22.0（钛）。