Предположим, у нас есть такая структура данных:
#typedef struct
{
int C_Field;
}C;
#typedef struct
{
C B_Array[MAX_SIZE];
}B;
#typedef struct
{
B A_Array[MAX_SIZE];
}A;
Кажется, что Frama-C не назначает место для поля структуры типа C в следующем примере:
/*@
assigns Arg->A_Array[0..(MAX_SIZE - 1)].B_Array[0..(MAX_SIZE - 1)].C_Field;
*/
void Initialize (A * Arg);
Приемлема ли приведенная выше аннотация Frama-C вообще?
Код разработан следующим образом. Основная цель — сбросить поле C_Field в 0:
/*@ predicate
ResetB (B * Arg) =
\forall integer Index; 0<= Index < MAX_SIZE ==>
Arg -> B_Array[Index].C_Field == 0;
*/
//@ assigns * Arg;
// Even I tried this:
//@ assigns Arg -> A_Array[0..(MAX_SIZE - 1)];
void Initialize (A * Arg)
{
/*@ loop invariant 0 <= Index <= MAX_SIZE;
loop invariant ResetB(&(Arg->A_Array[Index]));
loop assigns Index, Arg -> A_Array[0..(MAX_SIZE - 1)];
*/
for (int Index = 0; Index < MAX_SIZE; Index++)
{
Reset(&(Arg -> A_Array[Index]));
}
}
/*@ assigns Arg -> B_Array[0..(MAX_SIZE - 1)];
ensures ResetB(Arg);
*/
void Reset(B * Arg)
{
/*@ loop invariant 0 <= Index <= MAX_SIZE;
loop invariant \forall integer i; 0<= i < Index ==>
Arg -> B_Array[i].C_Field == 0;
loop assigns Index, Arg -> B_Array[0..(MAX_SIZE - 1)];
*/
for (int Index = 0; Index < MAX_SIZE; Index++)
{
Arg -> B_Array[Index].C_Field = 0;
}
}
Контракт функции Reset выполняется, а контракт функции Initialize — нет. Как написать правильное «назначение» для контракта Initialize?
assigns
(при условии, что#
передtypedef
удалено и задано определение дляMAX_SIZE
). Не могли бы вы описать точно что вы пробовали с этим кодом и чем результат Frama-C отличается от того, что вы ожидали? - person Virgile   schedule 27.04.2017frama-c -wp file.c
, контрактReset
помечен как действительный, а контрактInitialize
- нет, но плагин, который вы используете, должен был быть упомянут явно. Есть много возможных применений Frama-C, и ответ на вопрос «Почему xxx не доказан?» будет сильно различаться в зависимости не только от xxx, но и от используемых вами подключаемых модулей. - person Virgile   schedule 27.04.2017