C and C++. Ada is used less for new projects, but existing projects aren't switched over - many projects have long lifespans going over a decade or more.
Oh hellz no! Most of the systems ADA is used for tend to be realtime stuff. The moment you utter the words "Garbage Collection" you throw your realtime guarantees down the toilet.
Hardly the same thing though. Astrée is a static analyzer used to help prove avionics code written in C, it's not used in any onboard avionics systems. So its lack of real-time processing is not important.
If you're writing real-time avionics software, your choices are really only Ada, C and C++. Most companies I know of, including Airbus, are using C. Typically, avionics software has to be qualified to DO-178B/ED-12B standards which specifies certain development, testing and proofing requirements. Software verification tools like Astrée are also governed by DO-178B/ED-12B, though they are subject to a lighter verification process.