[pjmlp]

Depends on which dynamic memory you are talking about.

Ada can manage dynamic stacks, strings and arrays on its own.

For example, Ada has what one could call type safe VLAs, instead of corrupting the stack like C, you get an exception and can redo the call with a smaller size, for example.

As for explicit heap types and Ada.Unchecked_Deallocation, yes if we are speaking about Ada 83.

Ada 95 introduced controlled types, which via Initialize, Adjust, and Finalize, provide the basis of RAII like features in Ada.

Here is an example on how to implement smart pointers with controlled types,

https://www.adacore.com/gems/gem-97-reference-counting-in-ad...

There is also the possiblity to wrap heap allocation primitives with safe interfaces exposed via storage pools, like on this tutorial https://blog.adacore.com/header-storage-pools

Finally thanks to SPARK, nowadays integrated into Ada 2012[0], you can also have formal proofs that it is safe to release heap memory.

In top of all this, Ada is in the process of integrating affine types as well.

[0] - Supported in PTC and GNAT, remaining Ada compilers have a mix of Ada 95 - 2012 features, see https://news.ycombinator.com/item?id=27603292

[touisteur]

That said, I still use valgrind because we have to integrate C libraries sometimes (libpcl is my favorite culprit, only because I'm trying , and there's still possibility to blow the stack (yeah you can use gnatstack to get a good idea of your maximum stack size, but it's doesn't cover the whole Ada featureset and stack canaries - fstack-check don't catch everything.

edit Also massif, call/cachegrind and hellgrind have saved our bacon many, many times.

Even more interesting is writing your own tools with valgrind. Here https://github.com/AdaCore/gnatcoverage/tree/master/tools/gn... is the code of a branch-trace adapter for valgrind (outputs all branches taken/not-taken in 'qemu' format). Very useful if you can run a pintool or Intel Processor Trace just for that.

And if you keep digging, the angr symbolic execution toolkit use (used?) VEX as an intermediate representation. end of edit

Ada doesn't catch uninitialized variables by default (although warnings are getting better). You can either go Spark 'bronze level' (dataflow proof, every variable is initialized) or use 'pragma Initialize_Scalars' combined with -gnatVa.

Some of these techniques described in that now old blog post full of links https://blog.adacore.com/running-american-fuzzy-lop-on-your-... (shameless plug) where one can infer that even proof of absence of runtime errors isn't a panacea and fuzzing still has its use even on fully-proved SPARK code.