Ah, a parser doesn't have to he recursive to blow the stack. Several layers of calls with lots of temporary arrays of large discriminated-record variables blew

Ah, a parser doesn't have to he recursive to blow the stack. Several layers of calls with lots of temporary arrays of large discriminated-record variables blew in my face, because of a misunderstanding about the size of some objects and not enough stack space reserved :-\. I wasn't thinking of asking the SPARK examiner/prover to prove stack size, more for gnatstack itself to support the full SPARK subset with precision. IIRC gnatstack used mostly -fstack-usage reports with a thick layer of post-processing, which can probably be improved with a layer of abstract interpretation handwave :-). I'll have to check the current state of affairs before I complain any more.