frama-c wp константная переменная и константный массив

Question

Я пытаюсь доказать некоторый код C с плагином WP Frama-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 глобальные переменные действительно сохраняют свое начальное значение на протяжении всего выполнения программы (это не значение по умолчанию, так как, хотя в какой-то момент это вызывает неопределенное поведение, в некотором коде на Си кажется, что const это скорее совет, чем обязательное правило).

Однако в этом случае вы все равно не сможете доказать свое предварительное условие, так как оно действительно неверно: &globalStringArray[0] недопустимо, так как это массив const, Если вы измените договор copyMemory сказать \valid_read(dest), тогда все будет доказано с -wp-init-const вариант.

Несколько дополнительных замечаний по вашей спецификации, хотя они не имеют прямого отношения к вашему вопросу:

• requires пункт о copyMemory не требует src а также dest указать на действительный блок длины, по крайней мере len, Предположительно, вы хотите написать что-то вроде \valid(src+(0 .. length - 1))
• Я думаю, что вы должны поменяться ролью src а также dest, так как это немного странно, чтобы передать const массив как destначало функции копирования.
• Наконец, помните, что для использования WP, каждая функция, которая вызывается (например, copyMemory здесь) должен прийти с assigns предложение, указывающее, какие ячейки памяти могут быть изменены вызываемым пользователем