Splint 无法检查指向堆栈变量的指针上的 maxSet

Question

我有一个程序可以执行以下操作：

#include <stdio.h>
#include <stdlib.h>

int f(char *result)
{
    if (result != NULL)
    {
        *result = 'a';
    }
    return 0;
}

int main ()
{
    char s = 0;
    (void)f(&s);
    printf("f gave %c\n", s);
    return 1;
}

我传递一个指向函数的指针，取消引用它，然后存储一些东西。 Splint 报告它无法解决 f: 中的 maxSet(result) >= 0 约束：

test.c: (in function f)
test.c:8:9: Possible out-of-bounds store: *result
    Unable to resolve constraint:
    requires maxSet(result @ test.c:8:10) >= 0
     needed to satisfy precondition:
    requires maxSet(result @ test.c:8:10) >= 0
  A memory write may write to an address beyond the allocated buffer. (Use
  -boundswrite to inhibit warning)

&s 指向堆栈上的单个字符，因此它的 maxSet 应该为 1，而不添加任何注释。 Splint 为什么抱怨？

Answer 1

据我所知，splint 报告它无法使用任何无法验证指向实际缓冲区或数组的指针来验证约束。这看起来很奇怪，因为它似乎没有理由不能将单个变量处理为等于 1 的数组，但似乎确实如此。

例如，使用以下代码：

int main (void)
{
    int a = 5;
    int b[1] = {6};
    int * pa = &a;
    int * pb = b;

    char c = (char) 0;
    char d[1] = {(char) 0};
    char * pc = &c;
    char * pd = d;

    *pa  = 6;       /*  maxSet warning  */
    *pb  = 7;       /*  No warning      */
    *b   = 8;       /*  No warning      */

    *pc = 'b';      /*  maxSet warning  */
    *pd = 'c';      /*  No warning      */
    *d  = 'd';      /*  No warning      */

    return 0;
}

splint 给出以下输出：

paul@thoth:~/src/sandbox$ splint -nof +bounds sp.c
Splint 3.1.2 --- 20 Feb 2009

sp.c: (in function main)
sp.c:15:5: Possible out-of-bounds store: *pa
    Unable to resolve constraint:
    requires maxSet(&a @ sp.c:7:16) >= 0
     needed to satisfy precondition:
    requires maxSet(pa @ sp.c:15:6) >= 0
  A memory write may write to an address beyond the allocated buffer. (Use
  -boundswrite to inhibit warning)
sp.c:19:5: Possible out-of-bounds store: *pc
    Unable to resolve constraint:
    requires maxSet(&c @ sp.c:12:17) >= 0
     needed to satisfy precondition:
    requires maxSet(pc @ sp.c:19:6) >= 0

Finished checking --- 2 code warnings
paul@thoth:~/src/sandbox$ 

取消引用指向（一个元素）数组的第一个字符的指针，以及取消引用数组名称本身都不会产生错误，但取消引用仅指向单个变量的指针会，对于char 和int。这似乎是一种奇怪的行为，但事实就是如此。

顺便说一句，在您的f() 函数中，您无法真正推断result 在main() 中指向的内容。虽然当您单独查看这两个函数时，很明显result 指向应该是一个有效的参考，据夹板所知，可以从其他翻译单元对f 进行更多调用，并且它不知道result 在那些 的情况下可能指向什么，所以它只需要通过它本身为f() 提供的信息。

例如，这里：

static void f(char * pc)
{
    if ( pc ) {
        *pc = 'E';      /*  maxSet warning  */
    }
}

int main(void)
{
    char c[25] = "Oysters and half crowns.";
    *c = 'U';           /*  No warning      */

    f(c);

    return 0;
}

splint 将警告f() 中的分配，但不会警告main() 中的分配，正因如此。但是，如果您对其进行注释，那么它就有足够的信息来弄清楚：

static void f(char * pc) /*@requires maxSet(pc) >= 0; @*/
{
    if ( pc ) {
        *pc = 'E';      /*  No warning      */
    }
}

int main(void)
{
    char c[25] = "Oysters and half crowns.";
    *c = 'U';           /*  No warning      */

    f(c);

    return 0;
}

但即使在这里，如果您将c 更改为单个char，您也会遇到相同的问题，因为夹板不会验证是否满足带注释的约束，因此：

static void f(/*@out@*/ char * pc) /*@requires maxSet(pc) >= 0; @*/
{
    if ( pc ) {
        *pc = 'E';      /*  No warning      */
    }
}

int main(void)
{
    char c;
    f(&c);              /*  maxSet warning  */

    return 0;
}

给你这个：

paul@thoth:~/src/sandbox$ splint -nof +bounds sp3.c
Splint 3.1.2 --- 20 Feb 2009

sp3.c: (in function main)
sp3.c:11:5: Possible out-of-bounds store: f(&c)
    Unable to resolve constraint:
    requires maxSet(&c @ sp3.c:11:7) >= 0
     needed to satisfy precondition:
    requires maxSet(&c @ sp3.c:11:7) >= 0
     derived from f precondition: requires maxSet(<parameter 1>) >= 0
  A memory write may write to an address beyond the allocated buffer. (Use
  -boundswrite to inhibit warning)

Finished checking --- 1 code warning
paul@thoth:~/src/sandbox$