2

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

#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 报告它无法解决maxSet(result) >= 0f 中的约束：

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 而无需添加任何注释。为什么夹板抱怨？

4

1 回答 1

1

据我所知，夹板报告它无法使用任何无法验证指向实际缓冲区或数组的指针来验证约束。这似乎很奇怪，因为它似乎没有理由不能将单个变量处理为等于 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;
}

夹板给出以下输出：

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$

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

顺便说一句，在您的f()函数中，您无法真正推断resultin 指向的内容main()。虽然当您单独查看这两个函数时，似乎很明显result指向应该是一个有效的参考，据 splint 所知，可以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;
}

出于这个原因，夹板会警告 in 的分配f()，但不会警告 in 的分配。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为 single char，您也会遇到相同的问题，因为 splint 不会验证带注释的约束是否得到满足，因此：

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$
于 2015-03-28T01:36:58.673 回答