forked from klee/klee
-
Notifications
You must be signed in to change notification settings - Fork 2
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
1 parent
7911dfb
commit d140272
Showing
3 changed files
with
91 additions
and
1 deletion.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,55 @@ | ||
/* | ||
* Copyright (c) Huawei Technologies Co., Ltd. 2021-2021. All rights reserved. | ||
* | ||
* @description FORWARD_NULL, 如果字符串或者指针作为函数参数,为了防止空指针引用错误,在引用前必须确保该参数不为NULL, | ||
* 如果上层调用者已经保证了该参数不可能为NULL,在调用本函数时,在函数开始处可以加ASSERT进行校验。 | ||
* | ||
* @bad TestBad5; | ||
* | ||
* @CWE 476; | ||
* | ||
* @secureCoding | ||
* | ||
* @csec | ||
* | ||
* @tool Coverity:FORWARD_NULL;SecBrella:SecB_ForwardNull; | ||
* | ||
* @author xwx356597; m00489032 | ||
* | ||
*/ | ||
|
||
#include <stdlib.h> | ||
#include <stdio.h> | ||
#include <string.h> | ||
//#include "securec.h" | ||
|
||
struct TEACHER { | ||
unsigned int id; | ||
char *name; | ||
}; | ||
|
||
struct STU { | ||
unsigned int id; | ||
char *name; | ||
struct TEACHER *teacher; | ||
}; | ||
|
||
/* | ||
* @mainScene 开始事件:变量赋值NULL,结束事件:指针解引用运算 | ||
* @subScene 指针是结构体类型,直接赋值为{0},之后访问成员变量 | ||
*/ | ||
void TestBad5(struct STU *pdev, const char *buf, unsigned int count) | ||
{ | ||
struct TEACHER *tea; | ||
// 开始事件,assign_zero - 结构体变量被赋予 {0} 值 | ||
struct STU *stu = 0; | ||
/* POTENTIAL FLAW: 结束事件,var_deref_op - null 指针解引用运算,访问成员变量 */ | ||
tea = stu->teacher; // CHECK: KLEE: WARNING: True Positive at: /mnt/d/dev/klee-test/src-bc-reports/sources/secbrella/SecB_ForwardNull/BadCase/AssignNull_Scene_BadCase02.c:47 | ||
unsigned int teacherID = tea->id; | ||
printf("teacher id is %ud", teacherID); | ||
} | ||
|
||
// RUN: %clang %s -emit-llvm -c -g -O0 -Xclang -disable-O0-optnone -o %t1.bc | ||
// RUN: rm -rf %t.klee-out | ||
// RUN: %klee --output-dir=%t.klee-out --execution-mode=error-guided --mock-external-calls --posix-runtime --libc=klee --skip-not-lazy-and-symbolic-pointers --max-time=120s --analysis-reproduce=%s.json %t1.bc | ||
// RUN: FileCheck -input-file=%t.klee-out/warnings.txt %s |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,33 @@ | ||
{ | ||
"errors": [ | ||
{ | ||
"category": "NULL pointer deference", | ||
"trace": [ | ||
{ | ||
"location": { | ||
"file": "/mnt/d/dev/klee-test/src-bc-reports/sources/secbrella/SecB_ForwardNull/BadCase/AssignNull_Scene_BadCase02.c", | ||
"reportLine": 45, | ||
"function": "TestBad5" | ||
}, | ||
"event": { | ||
"kind": "AssignZero" | ||
} | ||
}, | ||
{ | ||
"location": { | ||
"file": "/mnt/d/dev/klee-test/src-bc-reports/sources/secbrella/SecB_ForwardNull/BadCase/AssignNull_Scene_BadCase02.c", | ||
"reportLine": 47, | ||
"function": "TestBad5" | ||
}, | ||
"event": { | ||
"kind": "Error", | ||
"error": { | ||
"sort": "NullDereference", | ||
"target": "stu" | ||
} | ||
} | ||
} | ||
] | ||
} | ||
] | ||
} |