CHB: add postcondition attribute for non-returning to gcc attribute support

[sipma]

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.