Open Geoffrey1014 opened 1 year ago
I got a false positive error when compiling the following CMVE program:
#include <stdio.h>
int *a(int i) {
int *n = 0;
return n;
}
int main() {
int d;
int *e;
int **f = &e;
for (int g = 0; g < 3; g++)
for (d = 2; d; d--) {
printf("NPD_FLAG\n");
*f = a(f == 0);
}
}
Compiling the above code with Clang (trunk) with -Xclang -analyzer-config -Xclang widen-loops=true --analyze --analyzer-output text -Xclang -analyzer-display-progress
in https://godbolt.org/z/96z6j5EMf result in:
ANALYZE (Syntax): <source> a : 12.4 ms
ANALYZE (Syntax): <source> main : 0.1 ms
ANALYZE (Path, Inline_Regular): <source> main : 35.7 ms
<source>:14:10: warning: Dereference of null pointer (loaded from variable 'f') [core.NullDereference]
*f = a(f == 0);
~ ^
<source>:11:3: note: Loop condition is true. Entering loop body
for (int g = 0; g < 3; g++)
^
<source>:12:5: note: Loop condition is true. Entering loop body
for (d = 2; d; d--) {
^
<source>:12:5: note: Loop condition is true. Entering loop body
<source>:12:5: note: Loop condition is false. Execution continues on line 11
<source>:11:3: note: Loop condition is true. Entering loop body
for (int g = 0; g < 3; g++)
^
<source>:12:17: note: Value assigned to 'f'
for (d = 2; d; d--) {
^
<source>:12:5: note: Loop condition is true. Entering loop body
for (d = 2; d; d--) {
^
<source>:14:14: note: Assuming 'f' is equal to null
*f = a(f == 0);
^~~~~~
<source>:14:10: note: Dereference of null pointer (loaded from variable 'f')
*f = a(f == 0);
~ ^
===-------------------------------------------------------------------------===
Analyzer timers
===-------------------------------------------------------------------------===
Total Execution Time: 0.0053 seconds (0.0497 wall clock)
---User Time--- --System Time-- --User+System-- ---Wall Time--- --- Name ---
0.0022 ( 62.9%) 0.0011 ( 62.9%) 0.0033 ( 62.9%) 0.0357 ( 71.8%) Path exploration time
0.0003 ( 8.0%) 0.0001 ( 8.0%) 0.0004 ( 8.0%) 0.0125 ( 25.1%) Syntax-based analysis time
0.0010 ( 29.1%) 0.0005 ( 29.1%) 0.0015 ( 29.1%) 0.0015 ( 3.1%) Path-sensitive report post-processing time
0.0035 (100.0%) 0.0018 (100.0%) 0.0053 (100.0%) 0.0497 (100.0%) Total
1 warning generated.
Compiler returned: 0
First, there exists proof in function main
that f
cannot be null but CSA still takes the assumption " 'f' is equal to null ".
Second, the path notes contain a weird message:
<source>:12:17: note: Value assigned to 'f'
for (d = 2; d; d--) {
There is no variable f
in the expression for (d = 2; d; d--) {
GSA not FP: https://godbolt.org/z/YbfKqc6bc
date: 2022-10-16 commit: 8c1a508616b438ace29429f4da3f4912772c5503 args: -Xclang -analyzer-config -Xclang widen-loops=true --analyze --analyzer-output text -Xclang -analyzer-display-progress test:
report: https://github.com/llvm/llvm-project/issues/58644 fix: original: