Skip to content

Draft: Pointer aliasing for backward analysis (work in progess)

Nian-Ze Lee requested to merge backward-pointer-aliasing into trunk

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/branches/backward-pointer-aliasing@44347 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c

This MR implements pointer aliasing for backward analysis, such as backward BMC. It is the third milestone of the Google Summer of Code project by Bas Laarakker.

This MR is a work in progress. It has not yet implemented support for pointers to struct or union.

The results of backward BMC without and with pointer aliasing on ReachSafety tasks excluding subcategories LDV and product lines (because many tasks in these subcategories use pointers to struct or union) are attached: results.2023-08-23_09-04-37.table.html.

On 6362 tasks, enabling pointer aliasing increased the correct results of backward BMC by 11% and reduced the wrong alarms from 484 to 8.

This MR is only for code review. Merging has to be done via SVN.

Merge request reports