search

eth-sri / ELINA

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

Box manager funptr incomplete #13

Open alexjung opened 6 years ago

alexjung commented 6 years ago

I tried to port some simple examples from APRON to ELINA. This worked for simple linear expressions but resulted in a segmentation fault for t-expressions, which I think are required to perform e.g. multiplication on two intervals.
I could pinpoint the problem to the file elina_box_internal.c where the funptr array is only partly filled with the corresponding function pointers. Obviously accessing the index ELINA_FUNID_ASSIGN_TEXPR_ARRAY had to result in a segmentation fault as for this index there is no function assigned/implemented.
Are you planning to implement those "missing" functions? And if yes do you have a roadmap for this? Thanks in advance!

GgnDpSngh commented 6 years ago

Hi Alex,

Thanks for your feedback. The Box domain in ELINA currently supports less functionality than Octagon and Polyhedra domain. We have added support for ASSIGN_TEXPR_ARRAY required by your analysis. Let us know if your analysis requires any other unsupported operators.

Cheers, Gagan

alexjung commented 6 years ago

Hi Gagan,

thank you very much for implementing this so quickly! You only missed an #include "elina_texpr0.h" in elina_box.h as the elina_texpr_0_t type is used in the elina_box_assign_texpr_array() function. I'll let you know if we need any other operators. At the moment it looks like we will be switching to the octagons domain because for that there is also the python interface.

Cheers, Alex

GgnDpSngh commented 6 years ago

Hi Alex,

Thanks for pointing out the dependency on "elina_texpr0.h" in "elina_box.h". It has been fixed now. Let us know if you encounter any other issues with ELINA.

Cheers, Gagan