Floating-point rounding mode set directly due to preprocessing

[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?

[zvonimir]

@tautschnig : It seems that you contributed these tasks, and so maybe you could pitch in here. Thanks!