代码静态分析工具——splint的学习与使用

splint *.c

 1 //splint_msg.c
 2 int func_splint_msg1(void)
 3 {
 4      int a;
 5      return 0;
 6 }
 7 int func_splint_msg2(void)
 8 {
 9     int* a = (int*)malloc(sizeof(int));
10     a = NULL;
11     return 0;
12 }

splint_msg.c: (in function func_splint_msg1)
splint_msg.c:4:6: Variable a declared but not used
  A variable is declared but never used. Use /*@unused@*/ in front of
  declaration to suppress message. (Use -varuse to inhibit warning)

splint_msg.c: (in function func_splint_msg2)
splint_msg.c:10:2: Fresh storage a (type int *) not released before assignment:
                      a = NULL
  A memory leak has been detected. Storage allocated locally is not released
  before the last reference to it is lost. (Use -mustfreefresh to inhibit
  warning)
   splint_msg.c:9:37: Fresh storage a created

Finished checking --- 2 code warnings

splint -showcol a.c   //在检测a.c时，告警消息中列数不被打印
splint -varuse  a.c   //在检测a.c时，告警消息中未使用变量告警不被打印

1 //null_dereferences.c
2 int func_null_dereferences(void)
3 {
4      int* a = NULL;
5      return *a;
6 }

null_dereference.c: (in function func_null_dereferences)
null_dereference.c:5:10: Dereference of null pointer a: *a
  A possibly null pointer is dereferenced.  Value is either the result of a
  function which may return null (in which case, code should check it is not
  null), or a global, parameter or structure field declared with the null
  qualifier. (Use -nullderef to inhibit warning)
   null_dereference.c:4:11: Storage a becomes null

Finished checking --- 1 code warnin

1 //types.c
2 void splint_types(void)
3 {
4     short a = 0;
5     long b = 32768;
6     a = b;
7     return;
8 }

types.c: (in function splint_types)
types.c:6:2: Assignment of long int to short int: a = b
  To ignore type qualifiers in type comparisons use +ignorequals.

Finished checking --- 1 code warning

1 //memory_management1.c
2 void memory_management1(void)
3 {
4     int* a = (int*)malloc(sizeof(int));
5     int* b = a;
6     free(a);
7     *b = 0;
8     return;
9 }

memory_management1.c: (in function memory_management1)
memory_management1.c:7:3: Variable b used after being released
  Memory is used after it has been released (either by passing as an only param
  or assigning to an only global). (Use -usereleased to inhibit warning)
   memory_management1.c:6:7: Storage b released
memory_management1.c:7:3: Dereference of possibly null pointer b: *b
  A possibly null pointer is dereferenced.  Value is either the result of a
  function which may return null (in which case, code should check it is not
  null), or a global, parameter or structure field declared with the null
  qualifier. (Use -nullderef to inhibit warning)
   memory_management1.c:5:11: Storage b may become null

Finished checking --- 2 code warnings

1 //memory_management2.c
2 void memory_management2(void)
3 {
4      int* a = (int*)malloc(sizeof(int));
5      a = NULL;
6      return;
7 }

memory_management2.c: (in function memory_management2)
memory_management2.c:5:2: Fresh storage a (type int *) not released before assignment:
                 a = NULL
  A memory leak has been detected. Storage allocated locally is not released
  before the last reference to it is lost. (Use -mustfreefresh to inhibit
  warning)
   memory_management2.c:4:37: Fresh storage a created

Finished checking --- 1 code warning

1 //bounds1.c
2 void bounds1(void)
3 {
4     int a[10];
5     a[10] = 0;
6     return;
7 }

bounds1.c: (in function bounds1)
bounds1.c:5:2: Likely out-of-bounds store: a[10]
    Unable to resolve constraint:
    requires 9 >= 10
     needed to satisfy precondition:
    requires maxSet(a @ bounds1.c:5:2) >= 10
  A memory write may write to an address beyond the allocated buffer. (Use
  -likelyboundswrite to inhibit warning)

Finished checking --- 1 code warning

 1 //bounds2.c
 2 void bounds2(char* str)
 3 {
 4     char* tmp = getenv("HOME");
 5     if(tmp != NULL)
 6     {
 7         strcpy(str, tmp);
 8     }
 9     return;
10 }

bounds2.c: (in function bounds2)
bounds2.c:7:3: Possible out-of-bounds store: strcpy(str, tmp)
    Unable to resolve constraint:
    requires maxSet(str @ bounds2.c:7:10) >= maxRead(getenv("HOME") @
    bounds2.c:4:14)
     needed to satisfy precondition:
    requires maxSet(str @ bounds2.c:7:10) >= maxRead(tmp @ bounds2.c:7:15)
     derived from strcpy precondition: requires maxSet(<parameter 1>) >=
    maxRead(<parameter 2>)
  A memory write may write to an address beyond the allocated buffer. (Use
  -boundswrite to inhibit warning)

Finished checking --- 1 code warning