c - frama-c wp 常量变量和常量数组

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

但我不想依赖“需要 STRING_LEN == 5；”并用“const”证明第一个例子。如何实现？

Answer 1

选项 -wp-init-const 将指示 WP 考虑 const 全局变量确实在整个程序执行期间保持其初始值(这不是默认值，因为，尽管这在某些时候会调用未定义的行为，但某些 C 代码似乎认为 const 与其说是绑定(bind)规则，不如说是一种建议。

但是，在那种情况下，您仍然无法证明您的先决条件，因为它确实是错误的:&globalStringArray[0] is not valid ，因为它是一个 const 数组。如果您将 copyMemory 的契约修改为 \valid_read(dest)，那么所有内容都将通过 -wp-init-const 选项进行证明.

关于您的规范的一些附加说明，即使它们与您的问题没有直接关系:

• copyMemory 的requires 子句不要求src 和dest 指向有效的长度 block 至少 len。大概你想写一些像 \valid(src+(0 .. length - 1))
• 我想你应该交换 src 和 dest 的角色，因为将 const 数组作为目标复制函数。
• 最后，请记住，对于使用 WP，调用的每个函数(例如此处的 copyMemory)都必须带有一个 assigns 子句，指示哪些内存位置可能被修改被叫者