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

Local pass: create fresh allocation for unsupported constants #89

Closed caballa closed 4 years ago

caballa commented 4 years ago

Before we were returning a null cell when we encounter an unsupported constant. In debug mode, some assertion will fail which makes sense. In release mode, in some cases we will get a runtime error (e.g., when this line is executed https://github.com/seahorn/sea-dsa/blob/dev10/lib/seadsa/DsaLocal.cc#L758).

This commits allocate instead a fresh node which is unsound but at least we don't crash in release mode (a warning message is still printed). This was anyway the behavior for others constants such as array/struct/vector constants.