如何用Frama-C Wp插件形式化验证返回指针的C函数？

1. 返回字符串字面量的函数验证（strlit.c） #

原代码：

// strlit.c
/*@ assigns \nothing;
    ensures \result[0] == 'b' && \result[1] == 'l' && \result[2] == 'a' && \result[3] == 'h' && \result[4] == 0;
*/
const char *foo()
{
    return "blah";
}

执行frama-c-gui -wp -wp-rte strlit.c后出现的问题：

• ensures子句无法验证
• 警告：No 'assigns \result \from ...' specification for function 'foo'returning pointer type. Callers assumptions might be imprecise.

解决方法 #

Frama-C要求返回指针的函数必须明确\result的来源，同时需让Wp识别返回指针指向的字符串字面量属性：

1. 修正assigns子句：添加\result \from \nothing，因为字符串字面量是程序全局只读常量，返回的指针不依赖任何输入参数。
2. 优化ensures子句：直接断言返回指针等于字符串字面量地址，同时确保指针指向的内存可安全读取，这样Wp能直接关联到字面量的内容。

修改后的代码：

// strlit.c
/*@ assigns \result \from \nothing;
    ensures \result == "blah";
    ensures \valid_read(\result + 0..4);
*/
const char *foo()
{
    return "blah";
}

重新执行验证命令后，ensures子句可顺利验证，警告也会消失。

2. 返回动态分配内存的函数验证（alloc.c） #

原代码：

// alloc.c
#include <stdlib.h>

/*@ assigns \nothing;
    ensures \object_pointer(\result);
    ensures \valid(\result + (0..4)) ==> \result[0] == 'b' && \result[1] == 'l' && \result[2] == 'a' && \result[3] == 'h' && \result[4] == 0;
*/
char *foo()
{
    char *s = (char *)malloc(5);
    if (s == NULL) return NULL;
    s[0] = 'b';
    s[1] = 'l';
    s[2] = 'a';
    s[3] = 'h';
    s[4] = 0;
    return s;
}

执行验证后出现的问题：

• assigns子句无法验证
• 两个ensures子句均显示“在假设下有效”
• 出现与第一个问题相同的指针返回规范警告

解决方法 #

问题核心在于原assigns子句错误，函数实际修改了动态分配的内存区域，同时ensures子句的逻辑需要覆盖malloc成功和失败的所有情况：

1. 修正assigns子句：明确标注函数修改了\result（malloc返回的指针）以及\result指向的内存区域（*(\result + 0..4)），来源为\nothing（malloc的分配不依赖输入）。
2. 调整ensures子句：用逻辑或区分\result == NULL和\result != NULL的情况，确保所有分支都满足规范，消除“假设下有效”的依赖。

修改后的代码：

// alloc.c
#include <stdlib.h>

/*@ assigns \result, *(\result + 0..4) \from \nothing;
    ensures \object_pointer(\result);
    ensures \result == NULL || (\valid(\result + 0..4) && \result[0] == 'b' && \result[1] == 'l' && \result[2] == 'a' && \result[3] == 'h' && \result[4] == 0);
*/
char *foo()
{
    char *s = (char *)malloc(5);
    if (s == NULL) return NULL;
    s[0] = 'b';
    s[1] = 'l';
    s[2] = 'a';
    s[3] = 'h';
    s[4] = 0;
    return s;
}

重新执行验证命令后，assigns子句可验证通过，两个ensures子句也能完全满足，不再依赖额外假设。

内容的提问来源于stack exchange，提问作者T0mmiTheGreat