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; 

似乎邮资-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; 
} 
} 

功能复位的合同是满意的，但功能初始化的合同是没有的。如何为Initialize的合同写一个正确的“赋值”？

Answer 1

假设您使用插件WP（请参阅上面的注释），您的主要问题是您没有在Initialize函数中为您的循环编写loop assigns。对于要在其中使用WP的函数中出现的每个循环，都必须使用loop assigns。另外，如果您的合同有ensures条款，那么您很可能需要loop invariant，对于正在分析的代码中的每个单一循环来说都是如此。

更新 有了您提供的代码，邮资-C硅，不与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; 
} 
}