seahorn / sea-dsa

A new context, field, and array-sensitive heap analysis for LLVM bitcode based on DSA.
Other
157 stars 29 forks source link

Imprecise call graph #97

Closed shaobo-he closed 4 years ago

shaobo-he commented 4 years ago

Hello sea-dsa developers,

sea-dsa of dev10 branch appears to generate an imprecise call graph for the attached C file. Specifically, parse_input should call at least c1. But the call graph produced and attached only shows that it calls strcmp.

To reproduce the call graph, please use the following commands,

clang -c -emit-llvm -S bftpd_2.i
seadsa --sea-dsa-callgraph-dot bftpd_2.ll
dot -Tpdf callgraph.dotdot -o callgraph.pdf

bftpd_2.txt callgraph.pdf

caballa commented 4 years ago

Thanks again for sending a simple example to debug. I've committed a fix in dev10.

shaobo-he commented 4 years ago

Thank you for the fix, @caballa.

Closed this issue.