Some function summaries in the function summary library may have signatures that conflict with how these functions are called in binaries. This especially applies to functions of the assert_fail variety. These functions typically do not return, which is reflected in the function summary's postcondition, which is used in the function construction. Adding a non-returning postcondition to the gcc attribute support provides the option to add this postcondition to a function signature in a header file, which can be tailored for each binary as appropriate.
Some function summaries in the function summary library may have signatures that conflict with how these functions are called in binaries. This especially applies to functions of the assert_fail variety. These functions typically do not return, which is reflected in the function summary's postcondition, which is used in the function construction. Adding a non-returning postcondition to the gcc attribute support provides the option to add this postcondition to a function signature in a header file, which can be tailored for each binary as appropriate.