Planes Without Heaps

I ran across something interesting while reading up on abstract interpretation. I was prompted by a redditor comment that the approach in "Symbolic Disassembly" was an abstract interpretation technique. Patrick Cousot's team has a static analyzer for C code that they've applied to software in the Airbus A340 and A380:

The development of ASTRÉE started from scratch in Nov. 2001. Two years later, the main applications have been the static analysis of synchronous, time-triggered, real-time, safety critical, embedded software written or automatically generated in the C programming language. ASTRÉE has achieved the following two unprecedented results:

• A340-300 In Nov. 2003, ASTRÉE was able to prove completely automatically the absence of any RTE in the primary flight control software of the Airbus A340 fly-by-wire system, a program of 132,000 lines of C analyzed in 1h20 on a 2.8 GHz 32-bit PC using 300 Mb of memory (and 50mn on a 64-bit AMD Athlon™ 64 using 580 Mb of memory).


• A380 From Jan. 2004 on, ASTRÉE was extended to analyze the electric flight control codes then in development and test for the A380 series. The operational application by Airbus France at the end of 2004 was just in time before the A380 maiden flight on Wednesday, 27 April, 2005.

The analyzer has its limits, so by extension does the tested code: "ASTRÉE analyzes structured C programs, with complex memory usages, but without dynamic memory allocation and recursion." Of course we don't know from this whether there is other code run in the Airbus 340 or 380 that does use dynamic memory allocation, but presumably the 132,000 lines of C are an important and interesting part of the system. So, it's a largish useful program that doesn't use the heap.

Do you remember the last time you wrote a program with no dynamic memory allocation (in a language that doesn't do it as a matter of course)?