Closed michael-schwarz closed 1 month ago
Could it just be that ValueContexts
is used somewhere where it shouldn't be? That does call D.top
after all.
It is (by necessity) used by all analyses.
But it doesn't have to be D.top
for all of them. I guess some analysis simply doesn't have a top
and a different element would work instead. Those analyses might have context (startstate ())
something different from D.top ()
, so startcontext
probably should be too for them.
It seems that #1427 causes calls to
top ()
where these are unsupported (most likely when creating initial value-based contexts that are then discarded)We lose 32 points in SV-COMP here, all these tasks are related to setjmp/longjmp somehow.