4 ms·
> Ada is memory safe if you don’t use dynamic memory (never call free). Take a look at https://docs.adacore.com/live/wave/spark2014/html/spark2014_ug/en/source
by johnisgood 5y ago
> Ada is memory safe if you don’t use dynamic memory (never call free).
Take a look at https://docs.adacore.com/live/wave/spark2014/html/spark2014_ug/en/source/access.html#deallocation https://docs.adacore.com/live/wave/spark2014/html/spark2014_....
You can prove the absence of memory leaks, too. :)
- pitaj 5y agoLeaks are permitted in rust, and are not a memory safety concern. I don't think that's what he was talking about.
- johnisgood 5y agoI just added that as an extra. The point is that you can have memory safety even if you do free. It may not have been the case with Ada (without SPARK) in the past.
- johnisgood 5y agoI would also like to add these: > Values of such an access type can be deallocated safely. GNATprove generates verification conditions to ensure that no memory can be leaked. So... you can deallocate safely AND verify that no memory is leaked. Is it not wonderful? - https://docs.adacore.com/live/wave/spark2014/html/spark2014_ug/en/source/access.html#pointer-support-and-dynamic-memory-management https://docs.adacore.com/live/wave/spark2014/html/spark2014_... - https://docs.adacore.com/live/wave/spark2014/html/spark2014_ug/en/usage_scenarios.html#prove-absence-of-run-time-errors-aorte https://docs.adacore.com/live/wave/spark2014/html/spark2014_... > SPARK builds on the strengths of Ada to provide even more guarantees statically rather than dynamically. As summarized in the following table, Ada provides strict syntax and strong typing at compile time plus dynamic checking of run-time errors and program contracts. SPARK allows such checking to be performed statically. In addition, it enforces the use of a safer language subset and detects data flow errors statically.