Thomas Haas

I don't think there is an issue for litmus tests. At best it is a reminder that for actual Linux-code, treating RCU primitives via .cat without inlining their implementation may...

Performance-wise, this PR seems to give a slight degradation (from 170s to 200s on BBQ, subject to fluctuations). Memory-wise, I haven't checked the difference. It would be good to compare...

On what branch do you have that code?

Due to the recent update to mem2reg, we get a lot of warnings regarding pontentially uninitialized variables. My best bet is that the alias analysis has to be conservative on...

I haven't checked Dartagnan on your patch, but I would be surprised if the patch really changed much. Since the initializing loop has dynamic bounds (cause `count` is dynamic), I...

IIRC, the old algorithms were just unsound in those cases and that is why they were "more precise".

In the `Acyclicity` axiom when doing top-down propagation.

No, that one is correct. I believe it only is called when doing the active set computation. The issue is in both the `knowledgeClosure` functions, which use the must-set of...

As a short follow-up: We definitely need to avoid `ITE` for all language level compilation targets, because those certainly do not have such instructions.

You are right, I forgot to mention this. Both solutions 1 and 2 have problems with final conditions and liveness. I think the final condition problem can be circumvented by...