邮资-C WP常量变量和常量数组

我想证明与邮资-C的WP插件一些C代码，并与下面的例子有问题：邮资-C WP常量变量和常量数组

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

我的邮资-C具有版本：钠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'来证明第一个例子。如何实现这一目标？

来源

2015-10-05 bataliero1234

选项-wp-init-const将指示WP考虑到const全局确实有保持其初始值在整个程序执行（这是不是默认的，因为，虽然这在某些时候调用未定义的行为，一些C代码似乎认为const是更多的建议比绑定规则）。

然而，在这种情况下，你仍然无法证明你的先决条件，因为它确实是假的：&globalStringArray[0]是不无效，因为它是const数组。如果您将copyMemory的合同修改为\valid_read(dest)，则所有内容都将通过-wp-init-const选项进行验证。

几个在你规范补充说明，即使他们不直接关系到你的问题：

的copyMemory的requires条款并不要求src和dest指向至少长度的有效区块len。想必你想写类似\valid(src+(0 .. length - 1))
我猜你应该换的src和dest的作用，因为它是一个有点怪异传递一个const数组作为dest萌发的复制功能的。
最后，请记住，使用WP，每一个被称为（如copyMemory这里）函数必须拿出一个assigns条款表明该内存位置可能由被调用方进行修改

来源

2015-10-06 08:15:07 Virgile

邮资-C WP常量变量和常量数组

回答

相关问题