我有以下示例代码：
typedef struct {
BYTE fs_type; /* FAT sub-type (0:Not mounted) */
BYTE drv; /* Physical drive number */
} FATFS_temp;
FATFS_temp *FatFs_temp[1]; /* Pointer to the file system objects (logical drives) */
/*@
@ requires (vol <= 0) && (fs != \null) ==> \valid((fs)) ; // problematic one
@ behavior mount:
@ //assumes \valid(fs) && vol <= 0;
@ assumes fs != \null && vol <= 0;
@ ensures (vol <= 0) ==> (FatFs_temp[vol] == \old(fs));
@ ensures fs->fs_type == 0;
@ behavior unmount:
@ assumes fs == \null && vol <= 0;
@ ensures (vol <= 0) ==> (FatFs_temp[vol] == \null);
@ behavior error:
@ assumes vol > 0;
@ ensures \result == 88;
@ complete behaviors mount, unmount, error;
@ disjoint behaviors mount, unmount, error;
*/
int f_mount_temp (
BYTE vol, /* Logical drive number to be mounted/unmounted */
FATFS_temp *fs /* Pointer to new file system object (NULL for unmount)*/
)
{
FATFS_temp *rfs;
if (vol >= 1) /* Check if the drive number is valid */
return 88;
rfs = FatFs_temp[vol]; /* Get current fs object */
if (rfs) {
rfs->fs_type = 0; /* Clear old fs object */
}
if (fs) {
fs->fs_type = 0; /* Clear new fs object */
}
FatFs_temp[vol] = fs; /* Register new fs object */
return 22;
}
但是 Frama-C / Why3 无法证明代码中注释的“要求”之一。.Why 文件说明以下内容：
goal WP "expl:Pre-condition (file src/ff_temp.c, line 12) in 'f_mount_temp'":
forall vol_0 : int.
forall malloc_0 : map int int.
forall fatFs_temp_0 : map int addr.
forall fs_0 : addr.
(fs_0 <> null) ->
(vol_0 <= 0) ->
((linked malloc_0)) ->
((is_uint8 vol_0)) ->
(forall k_0 : int. (0 <= k_0) -> (k_0 <= 0) -> (null = fatFs_temp_0[k_0])) ->
((valid_rw malloc_0 fs_0 2))
end
为了学习，我的问题是：
1）该前提条件有什么问题？
2）基于 .Why 文件中的输出，我应该采取什么方法来找出问题所在？
3）有人可以指点我学习如何调试我的函数合同的资源吗？
编辑：
我使用以下标志运行 Frama-c：“-wp -wp-rte -wp-fct f_mount_temp”我没有从其他地方调用这个 f_mount_temp。我运行 Frama-c 直接检查这个 f_mount_temp()。
现在对我来说更清楚了，它可能是导致先决条件失败的额外断言。处理的函数契约如下，注释指示每个断言的状态：
/*@ requires vol ≤ 0 ∧ fs ≢ \null ⇒ \valid(fs); // unknown
behavior mount: // unknown
assumes fs ≢ \null ∧ vol ≤ 0;
ensures \old(vol) ≤ 0 ⇒ FatFs_temp[\old(vol)] ≡ \old(fs);
ensures \old(fs)->fs_type ≡ 0;
behavior unmount: //unknown
assumes fs ≡ \null ∧ vol ≤ 0;
ensures \old(vol) ≤ 0 ⇒ FatFs_temp[\old(vol)] ≡ \null;
behavior error: //unknown
assumes vol > 0;
ensures \result ≡ 88;
complete behaviors mount, unmount, error; // green
disjoint behaviors mount, unmount, error; // green
*/
-wp-rfe 标志添加的内联断言是：
int f_mount_temp(BYTE vol, FATFS_temp *fs) {
int __retres;
FATFS_temp *rfs;
if ((int)vol >= 1) {
__retres = 88;
goto return_label;
}
/*@ assert rte: index_bound: vol < 1; */ // ok
rfs = FatFs_temp[vol];
if (rfs) {
/*@ assert rte: mem_access: \valid(&rfs->fs_type); */ //unknown
rfs->fs_type = (unsigned char)0;
}
if (fs) {
/*@ assert rte: mem_access: \valid(&fs->fs_type); */ // unknown
fs->fs_type = (unsigned char)0;
}
/*@ assert rte: index_bound: vol < 1; */ // unknown
FatFs_temp[vol] = fs;
__retres = 22;
return_label: return __retres;
}