ACSL "назначает" аннотацию для внутренних структур и полей кода C

Question

Предположим, у нас есть такая структура данных:

#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 не выполнен. Как правильно написать "назначает" для договора инициализации?

Answer 1

Предполагая, что вы используете плагин WP (см. Комментарий выше), ваша главная проблема заключается в том, что вы не написали loop assigns для вашей петли в Initialize функция. loop assigns являются обязательными для каждого цикла, появляющегося в функциях, над которыми вы хотите использовать WP. Кроме того, если ваш контракт имеет ensures пункты, вам, скорее всего, понадобится loop invariantопять же для каждого цикла в анализируемом коде.

Обновление С помощью предоставленного вами кода и frama-c Silicon - единственное, что не подтверждено frama-c -wp file.c является ли цикл инвариантным в Initialize около ResetB, Причина, почему это не доказано, состоит в том, что это неправильно. Реальный инвариант должен читать \forall integer i; 0<=i<Index ==> ResetB(&(Arg->A_Array[i])), В следующем полном примере все разряжается, по крайней мере, с помощью Silicon:

#define MAX_SIZE 100

typedef struct
{
int  C_Field;
int D_Field;
}C;

typedef struct
{
C B_Array[MAX_SIZE];
}B;

typedef struct
{
 B A_Array[MAX_SIZE];
}A;

/*@ predicate 
      ResetB (B * Arg) =
        \forall integer Index; 0<= Index < MAX_SIZE ==>
                 Arg -> B_Array[Index].C_Field == 0;
*/

void Reset(B * Arg);

// @ 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 \forall integer i; 0<=i<Index ==> ResetB(&(Arg->A_Array[i]));
     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;
 }
}