goblint
Investigate possible performance gain by switching from Apron To Elina
ELINA also supports backward compatibility with APRON so that existing analyzers using APRON can benefit from ELINA with minimal changes.
from http://elina.ethz.ch/
Their benchmark numbers looking very promising, might be worth trying this out if we ever have time!
This assumes we first abstract our apron analysis away from Apron. This is partially supposed to be done in #592, but AFAIK that still keeps Apron.Environment and Apron.Var in the common interface. To be truly abstract and generic, that needs to be abstracted away as well. Then it should be possible to fairly easily plug in Elina or even Bddapron.
Supposedly, ELINA can act as a drop-in replacement for Apron, so it might not be necessary to make changes at all... I have not investigated this in detail, however.
I looked at Elina's OCaml package: https://ocaml.org/p/elina/1.3.2/doc/Elina_oct/index.html. Actually you're right about that: it depends on Apron and uses Apron types for most things. All it really does it provide two additional Apron managers. So it should be quite doable to just define two more managers, although the doubly-conditional build of that will complicate things a bit.
I assumed that a drop-in replacement would actually be a replacement of the entire library, just with the same interface under a different name (and backed by different implementations), rather than something depending on Apron and extending it.
Bddapron will still require more abstraction, since it has additional variable and expression types for logic.