frama-c - 如何为字符数组添加注释？

Question

我是 Frama-C 的新手，我一直在寻找一些关于如何为 char 数组编写注释的注释。通常在示例中我看到他们使用整数。所以我不确定我写的是否正确。

我有这个功能：

    User *login(char id[25], char pass[25], User *list);

我写了如下注释，但我不太确定：

    /*@ requires \valid(list);
      @ requires \valid_range(id, 0, 25-1);
      @ requires \valid_range(pass, 0, 25-1);
    */

Answer 1

It is difficult to tell for sure without having an informal description of what your function is supposed to take as argument, but your specification seems indeed correct, although it might be slightly incomplete. Here is what your requires says about the arguments:

• list must be a valid pointer
• id and pass must be pointers (remember that in formals declarations, you don't have arrays, only pointers) to blocks of (at least) 25 char. More precisely, you must be able to dereference id, id+1 ... id+24.

Note that \valid_range is deprecated in favor of \valid(id+(0 .. 24-1)) which carries exactly the same meaning.

These requirements make sense, but, depending on what the function is supposed to do, you might need other ones. For instance, are id and pass supposed to be 0-terminated string?