search

goblint / analyzer

Static analysis framework for C
https://goblint.in.tum.de
MIT License
160 stars 72 forks source link

Add support for Elina #1533

Open McTsts opened 4 days ago

McTsts commented 4 days ago

This is work in progress support for elina

michael-schwarz commented 4 days ago

Ideally, one would like to be able to dynamically switch between Apron and Elina. Is this planned?

McTsts commented 4 days ago

Ideally, one would like to be able to dynamically switch between Apron and Elina. Is this planned?

Yes, it's planned

sim642 commented 4 days ago

Ideally, one would like to be able to dynamically switch between Apron and Elina. Is this planned?

I think the cleanest way would be not to even have them exclusive. Just how ApronDomain induces the apron analysis and AffineEqualityDomain induces the affeq analysis, etc, some ElinaDomain could induce the elina analysis. (And elina could simply be an optional dependency then).

There seems to be some overriding of Elina domain functions here, which would be very natural to do then without impacting existing apron analysis at all. ElinaDomain could just redefine some functions in whatever ways it wants before wrapping it in a RelationAnalysis.