c - 删除 Splint 中的空警告

Question

我一直在尝试Splint使用我最近编写的 C 程序并试图理解和删除它给出的警告。一个我理解但无法理解如何删除它的代码来自以下代码片段:

static MyType_t *findById(const int id)
{
    int i;

    for (i = 0; i < MY_ARR_SIZE; i++) {
            if (my_arr[i].id == NOT_SET) {
                    /* Items are sorted so that items with 
                    NOT_SET as ID are at the end of the array */
                    break;
            }
            if (my_arr[i].id == id) {
                    return &(my_arr[i]);
            }
    }
    return NULL; 
}

Splint 对函数可以返回 NULL 感到不高兴，但在这种情况下它非常有意义。

我尝试使用/@nullwhenfalse@/但它似乎只有在函数返回 true/false 时才有效，并且还尝试更改代码以使用 retVal 并尝试了两者/@ null@/和/@relnull@/在声明的前面，但是这些什么也没做。

(作为旁注，该表只有 20 个大 atm，因此没有必要使用聪明的搜索算法。)

Answer 1

你应该仔细检查声明前面的/*@null@*/的使用。

在您示例的以下可编译版本中，它确实删除了警告(使用夹板 3.1.2):

typedef struct { int id; } MyType_t;
#define NOT_SET -1
#define MY_ARR_SIZE 20
static MyType_t my_arr[MY_ARR_SIZE];

/*@null@*/ static MyType_t *findById(const int id)
{
    int i;
    for (i = 0; i < MY_ARR_SIZE; i++) {
            if (my_arr[i].id == NOT_SET) {
                    /* Items are sorted so that items with 
                    NOT_SET as ID are at the end of the array */
                    break;
            }
            if (my_arr[i].id == id) {
                    return &(my_arr[i]);
            }
    }
    return NULL;
}

int main() {
    (void)findById(10);
    return 0;
}

如果您仍然有类似的警告，是否与您的代码的另一部分有关？