AdaCore Blog

GNAT Community 2020 is here!

by Nicolas Setton

We are happy to announce that the GNAT Community 2020 release is now available via https://www.adacore.com/download. Here are some release highlights:

GNAT compiler toolchain

The 2020 compiler includes tightening and enforcing of Ada rules, performance enhancements, and support for some Ada 202x features - watch this space for further news on this.

The compiler back-end has been upgraded to GCC 9 on all platforms except Mac OS - see below for further information about this exception.

ASIS is no longer supported, and we encourage you to switch to Libadalang for all your code intelligence needs. GNAT Community 2019 remains available for legacy support of ASIS.

RISC-V 64-bits

This year we have added a toolchain for RISC-V 64-bits hosted on Linux - you can try it out on boards like the HiFive Unleashed - and we include the emulator for this platform as well.

IDE

This release includes GNAT Studio, the evolution of GPS, our multi-language IDE for Ada, SPARK, C, C++ and Python. Notable features are:

  • A Completely new engine for Ada/SPARK navigation, implemented via a language server based on Libadalang. This means, in particular, that navigation works without requiring you to compile the codebase first.
  • Improved overall performance in the editors, the omnisearch, and the debugger.

  • Several UI enhancements, especially the contextual menus which have been reorganized.

Libadalang

Libadalang, a library for parsing and semantic analysis of Ada code, has made a lot of progress in the past year. In this GNAT Community release, you'll find:

  • A new app framework that allows you to scaffold your Libadalang project - see this blog post for more information.
  • The Python-facing API is now compatible with Python 3..

  • Support of Aggregate Projects has been added.

SPARK

For those looking to take their Ada programs to the next level, GNAT Community includes a complete SPARK toolchain now including the Lemma library (doc).

Toolchain and development environment enhancements are:

  • New SPARK submenus and key shortcuts in GNAT Studio.

  • Parallel analysis of subprograms.

  • Automatic target configuration for GNAT runtimes.

Proving engine enhancements are:

  • Support for infinite precision arithmetic in Ada.Numerics.Big_Numbers.Big_Integers/Big_Reals (doc).

  • Support for partially initialized data in proof (doc).

  • Detection of memory leaks by proof.

  • Dead code detected by proof warnings.

  • Improved floating-point support in Alt-Ergo prover.

SPARK language enhancements are:

  • Support for local borrowers as part of pointer support through ownership. 

  • Many fixes in the new pointer support based on ownership.

  • Detection of wrap-around on modular arithmetic with annotation No_Wrap_Around (doc).

  • Support for forward goto.

  • Support for raise expressions (doc).

  • Detection of unsafe use of Unchecked_Conversion (doc).

  • New annotation Might_Not_Return on procedures (doc).

  • Volatility refinement aspects supported for types (doc).

  • Allow SPARK_Mode Off inside subprograms.

  • Support for volatile variables to prevent compiler optimizations (doc).

Support for Visual Studio Code

If you are using Visual Studio Code, we have written a prototype extension for Ada and SPARK as part of our work on the Ada Language Server: you can find it on the Visual Studio Marketplace.

Notes on Mac OS

Mac OS is becoming harder to maintain, especially the latest versions, which require code signing for binaries. For the GNAT Community 2020 release we decided not to codesign and notarize the binaries, so you'll have to circumvent the protections: see the README for the specific instructions. We have also removed support for the ARM cross compiler hosted on this platform.

Posted in

About Nicolas Setton

Nico joined AdaCore in 2001 as an engineer, and has worked on many interesting things since. Now managing the IDE circle and Product Manager of GNAT Community.