C 代码的内部结构和字段的 ACSL "assigns" 注释
ACSL "assigns" annotation for inner structs and fields of C code
假设我们有这样一个数据结构:
#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"?
假设您使用的是插件 WP(见上面的评论),您的主要问题是您没有在 Initialize
函数中为循环编写 loop assigns
。 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]))
。使用以下 complete 示例,所有内容都已放电,至少使用硅:
#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;
}
}
假设我们有这样一个数据结构:
#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"?
假设您使用的是插件 WP(见上面的评论),您的主要问题是您没有在 Initialize
函数中为循环编写 loop assigns
。 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]))
。使用以下 complete 示例,所有内容都已放电,至少使用硅:
#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;
}
}