diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index 30063fd061..19ac15ec0c 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -3004,7 +3004,9 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { if (kgepi->offset) offset = AddExpr::create(offset, Expr::createPointer(kgepi->offset)); ref address = AddExpr::create(base, offset); - if (UseGEPExpr && !isa(address)) { + if (UseGEPExpr && + (!isa(address) || + (isa(base) && cast(base)->isZero()))) { if (isGEPExpr(base)) gepExprBases[address] = gepExprBases[base]; else diff --git a/test/Industry/AssignNull_Scene_BadCase02.c b/test/Industry/AssignNull_Scene_BadCase02.c new file mode 100644 index 0000000000..ea28aab736 --- /dev/null +++ b/test/Industry/AssignNull_Scene_BadCase02.c @@ -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 +#include +#include +//#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 \ No newline at end of file diff --git a/test/Industry/AssignNull_Scene_BadCase02.c.json b/test/Industry/AssignNull_Scene_BadCase02.c.json new file mode 100644 index 0000000000..bbcdc19260 --- /dev/null +++ b/test/Industry/AssignNull_Scene_BadCase02.c.json @@ -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" + } + } + } + ] + } + ] +} \ No newline at end of file