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.
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.