Floating-point rounding mode set directly due to preprocessing

Created by: zvonimir

See this line for example: https://github.com/sosy-lab/sv-benchmarks/blob/4c95243e3aff4b6c8da7a8c6ce18feb2a8306738/c/floats-cbmc-regression/float-rounding1_true-unreach-call.i#L1092

According to the specification for these functions: "Attempts to establish the floating-point rounding direction equal to the argument round, which is expected to be one of the floating point rounding macros." If you look at the original C file, things are done properly using macros, and so this problem happens due to preprocessing which automatically inlines machine-specific constants. How should we resolve this? Should we just fix the preprocessed files?