Skip to content

Draft: Create branch add_c_function_atexit

Daniel Baier requested to merge add_c_function_atexit into trunk

This MR discusses the addition of the C function atexit() (C11 7.22.4.2) to CPAchecker by adding it in the CFA. Similarly to function pointers, we add assumption edges to the CFA that handle entering of atexit() after each normal program terminating edge.

A CPA that handles this mechanic independently for trivial cases is to be added in a different MR later.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/branches/add_c_function_atexit@46959 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c

Merge request reports