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; 
} 
}