Are you sure? Around 2019, they seem to have overcome that limitation, since they removed mention of it from their website. A friend who pointed it out to me had found it on an old webpage from before then. I wonder if you found that the same way rather than trying it.
I had planned to look into that when I was using the free trial.
> To do better, a fully automatic sound analyzer would have to derive the relevant loop invariants and the associated induction proofs automatically, not to have to make any guess on the number of iterations. As far as I know this is still a research topic. Or alternatively, enforce a known, small enough bounds for any loop.
I plan to look into this when I try using sound static analyzers, since if they cannot do induction proofs on loops to prove loop correctness, it would either invalidate their claims of soundness, or at the very least limit the scope of such claims. I know that frama-c’s Eva is specifically documented as not being able to do this.
No, I just picked it from the ENS web page (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.
I'm definitely not an expert but look into SA a bit out of curiosity. Sound analysis normally comes with significant restrictions. For example Astrée does not support dynamic memory allocation nor recursion (not too bad for embedded). There's likely more.
Let's consider the case of an iteration, with a number of loops unknown at compile/analysis time. What an unsound SA will typically do is unroll the loop a fixed number of times (5 by default for CC/ClangSA from memory). Obviously this could miss bugs if less than the actual number of loops.
To do better, a fully automatic sound analyzer would have to derive the relevant loop invariants and the associated induction proofs automatically, not to have to make any guess on the number of iterations. As far as I know this is still a research topic. Or alternatively, enforce a known, small enough bounds for any loop.
In general, either the sound SA must be able to derive quite complex proofs for the characteristics to enforce (research topic), or it must enforce simplicity to make the problem manageable automatically.
An alternative is a tool like frama-C that can kick the ball back to a human, to do the correctness proof manually using a proof assistant for automatic verification, if automation fails. And that can be a hard job.
The more constrained the application, the more realistic sound analysis should be. I don't know where a filesystem like OpenZFS sits here. Best of luck in any case!