search

eth-sri / ELINA

ELINA: ETH LIbrary for Numerical Analysis
http://elina.ethz.ch/
Other
129 stars 54 forks source link

Various minor bugfixes #30

Closed Cu3PO42 closed 6 years ago

Cu3PO42 commented 6 years ago

While trying to understand and document the API, I have found a few minor bugs in the library. Except for a small remark on elina_interval_abs, I believe I have fixed them.

elina_interval_abs

When the source interval contains 0 in its interior, i.e., inf < 0 < sup, the result is [0, sup] rather than [0, max(-inf, sup)]. The operation elina_scalar_max(a->sup, b->inf, b->sup) in line 115 should negate the infimum.

Empty intervals are also not handled correctly. For example the interval [1, -1] would be mapped to [0, 1]. Is this intended? Is the precondition that the interval is not empty assumed?

elina_interval_magnitude

When the source interval contains 0 in its interior, i.e., inf < 0 < sup, the result of this operation is always sup. The operation elina_scalar_max(a, b->inf, b->sup) in line 368 should negate the infimum.

elina_rat_set_int

This method does not set the passed value at all. It simply stores ∞.

eval_elina_cstlincons0

Constraint 0 != 0 is classified incorrectly. It is never satisfiable, but "may be satisfied" is returned. I changed sgn == 0 ? 2 : 1 to sgn == 0 ? 0 : 1 to fix this.

elina_generic_meet_quasilinearize_lincons_array

In line 180, the function pointer to copy is called incorrectly. It is missing manager as a first argument.

GgnDpSngh commented 6 years ago

Hi Tobias,

Thanks for spotting the bugs and suggesting the fixes. They look fine to me and I will merge them. For "elina_interval_abs", it is always called in the library after checking if the input is non-bottom.

Cheers, Gagan