Widening/narrowing for recursions

[jumormt]

Thank you for open-sourcing this project. I'm curious about Crab's approach to handling recursions. From what I've observed, it identifies all widening points on the call graph and inlines the callee's logic, albeit with widening (but without narrowing) at these specific points. Could you confirm if my understanding aligns with Crab's recursion-handling strategy? I appreciate your time and insights.

[caballa]

Yes, your understanding is correct. The narrowing should be implemented but it wasn't for simplicity.
But note that it must apply widening both at the entry and the exit of the function.
The details are explained here in the Bourdoncle's paper https://link.springer.com/chapter/10.1007/BFb0039704