CHC: fopen library summary #1
Description
The behavior of the fopen library function is undefined if the mode argument is not equal to one of a given set of strings. This precondition can currently not be expressed. Request to add the option to specify this precondition, and to add the precondition to the fopen function.