splint *.c

 1 //splint_msg.c 2 int func_splint_msg1(void) 3 { 4 int a; 5 return0; 6 } 7 int func_splint_msg2(void) 8 { 9 int* a = (int*)malloc(sizeof(int));10     a = NULL;11 return0;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.c2 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.c2 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 longint to shortint: a = b  To ignore type qualifiers in type comparisons use +ignorequals.

Finished checking ---1 code warning

1 //memory_management1.c2 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 releasedmemory_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 returnnull (in which case, code should check it is notnull), 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.c2 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.c2 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