search

sosy-lab / sv-benchmarks

Collection of Verification Tasks (MOVED, please follow the link)
https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks
184 stars 170 forks source link

Floating-point rounding mode set directly due to preprocessing #571

Open zvonimir opened 6 years ago

zvonimir commented 6 years ago

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 commented 6 years ago

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