[Eva] Tests the file tests/nonlin.c with the option -warn-special-float none.
Previous commits have introduced the new runs (and oracles) without this option. This commit only contains the changes due to this option: - no alarms for non-finite floating-point values. - in the function [around_zeros], no reduction of the variable [f] as the division by 0 simply computes ∞. - volatile floating-point variables have a value in [-∞..∞] ∪ NaN.
Loading
Please register or sign in to comment