Add ./configure option to suppress overflow warnings

[jmct]

This addresses part of the concerns in issue #39. Namely, if we know the overflow is sound, then we can choose to skip printing to stderr when the sound overflow occurs.

The implementation is straightforward:

• We added an option to ./configure: -no-warn-overflow

• When enabled, this adds -DNO_WARN_OVERFLOW to extra_elina_options

• The printing to stderr in elina_poly/opt_pk/vector.c:570 is now under a CPP macro that checks whether -DNO_WARN_OVERFLOW is defined.

[jmct]

One thing that I'm not sure about is whether all the occurrences of ELINA_EXC_OVERFLOW are sound in the same way.

[GgnDpSngh]

Hi Jose,

Thanks for the update. Whenever there is an overflow our implementation tries to handle it in a sound way by setting the exception flag. This is detected in the calling method which sets the corresponding polyhedron to Top.

There has been recent work (https://dl.acm.org/citation.cfm?doid=3238147.3240464) that tested ELINA's soundness guarantees on challenging inputs. Many of these inputs generate test cases where one observes overflows and helped us fix issues. Ofcourse, there can be control paths that we may have missed and if you observe any unsoundness, let me know.

Cheers, Gagandeep Singh