c - frama-c wp const 変数と const 配列

Question

Frama-C の WP プラグインを使用していくつかの C コードを証明しようとしていますが、以下の例に問題があります。

typedef unsigned char uint8_t;

const uint8_t globalStringArray[] = "demo";
const int STRING_LEN = 5;

/*@ requires \valid(src) && \valid(dest) && len < 32 ; */ 
void copyMemory(uint8_t * src, uint8_t * dest, unsigned int len);

/*@ requires \valid(arrayParam) && len < 32 ; */
uint8_t func(uint8_t * arrayParam, unsigned int len)
{   
    uint8_t arrayBig[512] = { 0 };
    uint8_t * array_ptr = arrayBig;

    copyMemory(array_ptr, arrayParam, len);
    array_ptr = array_ptr + len;

    copyMemory(array_ptr, globalStringArray, STRING_LEN);
    array_ptr = array_ptr + STRING_LEN;


    return array_ptr[0];
}

指示：

frama-c -wp -wp-rte test.c

私のframa-cのバージョンはSodium-20150201で、alt-ergoは0.95.2です

結果は

[kernel] warning: No code nor implicit assigns clause for function copyMemory, generating default assigns from the prototype
[rte] annotating function func
[wp] 4 goals scheduled
[wp] [Qed] Goal typed_func_assert_rte_mem_access : Valid
[wp] [Qed] Goal typed_func_call_Frama_C_bzero_pre : Valid
[wp] [Alt-Ergo] Goal typed_func_call_copyMemory_pre : Valid (275ms) (209)
[wp] [Alt-Ergo] Goal typed_func_call_copyMemory_pre_2 : Unknown (907ms)

気がついたらいつ変わるんだろう

const uint8_t globalStringArray[] = "demo";
const int STRING_LEN = 5;

に

uint8_t globalStringArray[] = "demo";
int STRING_LEN = 5;

と

  /*@ requires \valid(arrayParam) && len < 32 && \valid(globalStringArray);
    requires STRING_LEN == 5;*/
uint8_t func(uint8_t * arrayParam, unsigned int len)
{ 

結果は

[wp] Proved goals:    4 / 4

しかし、「requires STRING_LEN == 5;」に頼りたくありません。'const' を使用して最初の例を証明します。それを達成する方法は？