c - 夹板如何进行污点分析

如何使用夹板进行污染分析？
我已经在我的Ubuntu 12.04上安装了Splint创建了一个小测试用例，如下所示：

#include<stdio.h>
#include<string.h>
int main(int argc, char *argv[]) {
    char a[10];
    strncpy(a,argv[1],10);
    printf(a);
    return 0;
}

还创建了包含以下内容的splint.xh文件：

int printf  (/*@untainted@*/ char *fmt, ...);
char *fgets (char *s, int n, FILE *stream) /*@ensures tainted s@*/ ;
char *strcat (/*@returned@*/ char *s1,  char *s2) /*@ensures s1:taintedness = s1:taintedness | s2:taintedness @*/ ;
void strncpy (/*@returned@*/ char *s1,  char *s2, size_t num)    /*@ensures s1:taintedness = s1:taintedness | s2:taintedness @*/ ;

还创建了包含以下内容的splint.mts文件：

    attribute taintedness
       context reference char *
       oneof untainted, tainted
       annotations
         tainted reference ==> tainted
         untainted reference ==> untainted
                       transfers
         tainted as untainted ==> error "Possibly tainted storage used where untainted required."
       merge
          tainted + untainted ==> tainted
       defaults
          reference ==> tainted
          literal ==> untainted
          null ==> untainted
    end

最后用命令运行夹板工具：

    splint -mts splint prg001.c

其中prg001.c是示例输入，“splint”是指splint.mts和splint.xh文件所有文件都在当前目录中。
我收到的输出是：
夹板3.1.2---2012年8月21日
prg001.c:（在函数main中）
prg001.c:6:1:将字符串参数格式化为printf不是编译时常量：
一
格式参数在编译时未知这会导致安全
无法对参数进行类型检查，因此存在漏洞（使用
-禁止警告的formatconst）
prg001.c:3:14:参数argc未使用
函数体中不使用函数参数如果论点
对于类型兼容性或将来的计划，需要使用/@unused@/
参数声明（使用-paramuse禁止警告）
检查完毕---2个代码警告
在输出中没有任何污染分析的迹象有人能帮我用夹板做污染分析吗。
谢谢

最佳答案

问题出在splint.xh文件上。
我把printf改成printfxxx，效果很好。
这意味着标准定义正在覆盖我的.xh文件这解决了我的问题，现在夹板输出污染变量和污染流。

关于c - 夹板如何进行污点分析，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/12649864/