Box manager funptr incomplete

[alexjung]

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]

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]

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]

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