frama-c wp const variable and const array

Question

I'm trying to prove some C code with the WP plugin of Frama-C and have problem with example below:

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

Command:

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

My frama-c has Version: Sodium-20150201, and alt-ergo is 0.95.2

The result is

[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)

I have noticed that when I will change

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

to

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

and

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

the result is

[wp] Proved goals:    4 / 4

but I don't want to rely on 'requires STRING_LEN == 5;' and prove first example with 'const'. How to achieve that?

Answer 1

Option -wp-init-const will instruct WP to consider that const globals indeed have keep their initial value throughout program execution (this is not the default, as, although this invokes undefined behavior at some point, some C code seems to consider that const is more an advice than a binding rule).

However, in that case, you still won't be able to prove your pre-condition, as it is indeed false: &globalStringArray[0] is not valid, since it is an array of const. If you modify the contract of copyMemory to say \valid_read(dest), then everything will be proved with the -wp-init-const option.

A few additional notes on your specification, even though they are not directly related to your question:

• The requires clause of copyMemory does not require src and dest to point to a valid block of length at least len. Presumably you want to write something like \valid(src+(0 .. length - 1))
• I guess that you should swap the role of src and dest, since it is a bit weird to pass a const array as the destination of a copy function.
• Finally, remember that for using WP, every function that is called (such as copyMemory here) must come with an assigns clause indicating which memory locations might be modified by the callee