search

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

Does every pointer value have a cell/node associated with it? #68

Closed zvonimir closed 4 years ago

zvonimir commented 4 years ago

To me it seems that when SeaDSA finishes, all pointer values in a program should have a cell/node associated with them. Unless, of course, there are bugs in SeaDSA. Is that right or am I missing something? Thanks!

agurfinkel commented 4 years ago

Yes.

At first, SeaDSA runs over every pointer producing instruction and allocates a node for it and a associates a cell with the instruction.

After that, the nodes are propagated and merged and moved between different functions (in context sensitive version).

zvonimir commented 4 years ago

Thanks! Makes sense. Btw, that was not completely the case with LLVM DSA, but I would guess that was due to bugs in there.