夹板无法在指向堆栈变量的指针上检查maxSet
夹板无法在指向堆栈变量的指针上检查maxSet
提问于 2015-03-27 14:57:34
我有一个程序，它执行如下操作：
#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。为什么夹板会抱怨？
回答 1
Stack Overflow用户
回答已采纳
发布于 2015-03-28 01:36:58
据我所知，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;
}夹板输出如下：
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指向了一个应该是有效的引用，据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;
}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，也会遇到相同的问题，因为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$ 页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持
原文链接：
https://stackoverflow.com/questions/29303720
复制相关文章
相似问题
腾讯云开发者
