Можно ли указать предложение доступа к буферам в frama-c?

Предполагая, что у меня есть следующие функции:Можно ли указать предложение доступа к буферам в frama-c?

void process_data(uint32_t * data, size_t length) { 
    for (size_t i = 0; i < length; i++) { 
     foo(data[i]); 
    } 
}

Как я могу сказать FRAMA-C «эта функция гарантирует каждому доступ к data[i] удовлетворяет условию i < length»? Насколько я понимаю, я могу разместить утверждение рядом с каждой строкой кода, которая читает data, но есть ли лучший способ?

источник

2016-12-15 John Doe

вопрос для вас - это абсолютно гарантировано, что 'data' будет не-NULL и укажет на коллекцию' uint32_t'? Может быть, требуется утверждение, прежде чем идти в цикл 'for'? – t0mm13b

Да, 'data' является' \ valid' и указывает на массив uint32_t. –

Что значит «эта функция обеспечивает ...»? Мне кажется, что вы хотите сказать, что «эта функция требует ...» (в противном случае у вас неверные обращения к памяти), не так ли? – Anne

Чтобы предотвратить недопустимые обращения к памяти, вам необходимо проверить, что эта функция всегда вызывается указателем data, из которого могут быть прочитаны не менее length элементов. Таким образом, вы должны написать предварительное условие:

//@ requires \valid_read (data + (0 .. length-1)); 
void process_data(uint32_t * data, size_t length) {

Так что, если вы можете гарантировать, что это свойство действительно, это гарантирует, что вы не будете иметь какой-либо недействителен доступ к памяти.

источник

2016-12-16 09:28:13 Anne

Возможно, я слишком неясен в объяснении этого, извините. Я хочу, чтобы функция frama-c wp не выполняла определенную проверку, когда функция 'process_data' может потенциально получать доступ к' данным' вне параметров 'length'. Например, проверка должна завершиться неудачей, если 'process_data' содержит оператор' uint32_t a = data [length + 1] '. –

@JohnDoe Я боюсь, что ответ зависит от использования Frama-C. Например, если вы хотите использовать WP с '-wp-rte', аннотация Anne действительно нужна вам: поскольку WP только знает, что написано в запросе, любая попытка доступа к индексу, превышающему' length', приведет к Неизвестный статус в аннотации RTE. Если вместо этого вы используете Value и 'process_data' вызывается с буфером размером больше' length', вам понадобятся более конкретные аннотации, которые вы должны предоставить сами (или через собственный скрипт). Не стесняйтесь уточнять свой вопрос, чтобы мы могли предоставить соответствующий ответ. – Virgile

Это объясняет это. Я думал, что предложение требует только анализа ценности, спасибо. –

Можно ли указать предложение доступа к буферам в frama-c?

ответ

Смежные вопросы