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

Handle functions that do not return but contain unreacahble instructions #139

Closed adrianherrera closed 1 week ago

adrianherrera commented 2 years ago

Attempts to fix issue #138

This occurs, for example, if a function calls exit. In this case, we still mark cells with mem.in markers. However, we only mark cells with mem.out if they return (because an unreachable instruction implies the program has terminated).

I'm not sure if this is 100% correct, so please let me know if not!