> Are you sure? No, I just picked it from the ENS web page (https://www.astree.ens.fr https://www.astree.ens.fr) but it may have not been updated for a while.

> Are you sure? No, I just picked it from the ENS web page (https://www.astree.ens.fr https://www.astree.ens.fr) but it may have not been updated for a while. As I understand it there's been improvement on dynamic allocation with separation logic in general, TBC what Astrée supports (I've no first hand experience). For recursion, it's a similar problem as for loops as I understand it: to handle it fully automatically the analyzer would have to prove recursion terminates and find and prove induction invariant. But safety critical code tend to forbid it anyway so it may not be a big limitation for most Astrée customers.