[Eva] Float_interval: slightly rewrites backward_is_finite and backward_is_nan.
These backward propagators takes a boolean argument [positive] that indicates whether the value to be reduced is finite (respectively NaN) or not. [backward_is_nan] replaces the two previous functions [backward_is_nan] and [backward_is_not_nan]. Implements the backward propagation [is_finite ~positive:false] that corresponds to !\is_finite(f).
Showing
- src/kernel_services/abstract_interp/float_interval.ml 21 additions, 16 deletionssrc/kernel_services/abstract_interp/float_interval.ml
- src/kernel_services/abstract_interp/float_interval_sig.mli 2 additions, 3 deletionssrc/kernel_services/abstract_interp/float_interval_sig.mli
- src/plugins/value/legacy/eval_terms.ml 4 additions, 6 deletionssrc/plugins/value/legacy/eval_terms.ml
- src/plugins/value/values/cvalue_forward.ml 2 additions, 2 deletionssrc/plugins/value/values/cvalue_forward.ml
Loading
Please register or sign in to comment