tala como realizar análise de contaminação

Question

Como realizar a análise de contaminação usando Splint?

Eu instalei o Splint no meu Ubuntu 12.04.Criei um pequeno caso de teste conforme abaixo:

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

Também foi criado o arquivo splint.xh com o seguinte conteúdo:

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 @*/ ;

Também foi criado o arquivo splint.mts com o conteúdo abaixo:

    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

Finalmente executei a ferramenta splint com o comando:

    splint -mts splint prg001.c

Onde prg001.c é a entrada de amostra, "splint" refere-se aos arquivos splint.mts e splint.xh.Todos os arquivos estão no diretório atual.

A saída que recebi é:

Tala 3.1.2 --- 21 de agosto de 2012

prg001.c:(na função principal) PRG001.C: 6: 1:O parâmetro de string de formato para printf não é uma constante de tempo de compilação:Um parâmetro de formato não é conhecido em tempo de compilação.Isso pode levar a vulnerabilidades de segurança porque os argumentos não podem ser marcados.(Utilização -formatconst para inibir aviso) prg001.c:3:14:Parâmetro argc não utilizado Um parâmetro de função não é usado no corpo da função.Se o argumento é necessário para compatibilidade de tipo ou planos futuros, use /@não utilizado@/ no declaração de argumento.(Use -paramuse para inibir o aviso)

Verificação concluída --- 2 avisos de código

Não há indícios de qualquer análise de contaminação na saída.Alguém pode me ajudar sobre como fazer a análise de contaminação usando Splint.

Obrigado

Answer 1

O problema estava com o arquivo splint.xh.

Mudei printf para printfxxx e funcionou bem.

Isso implicava que a definição padrão estava substituindo meu arquivo .xh.Isso resolveu meu problema e agora o splint gera variáveis ​​contaminadas e o fluxo de contaminação.