1

我正在尝试使用 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'证明第一个例子。如何做到这一点？

4

1 回答 1

2

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

但是，在这种情况下，您仍然无法证明您的先决条件，因为它确实是 false:&globalStringArray[0]无效，因为它是const. 如果您修改合约copyMemoryto say \valid_read(dest)，那么一切都将通过-wp-init-const选项得到证明。

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

  • 的requires子句copyMemory不需要src并且dest至少指向一个有效的长度块len。大概你想写类似的东西\valid(src+(0 .. length - 1))
  • 我想您应该交换 and 的角色src，dest因为将const数组作为dest复制函数的开始传递有点奇怪。
  • 最后，请记住，对于使用 WP，调用的每个函数（例如copyMemory此处）都必须带有一个assigns子句，指示被调用者可能修改哪些内存位置
于 2015-10-06T08:15:07.333 回答