Re:ZZ is a modern formally provable dialect of C
by Nursie on Wednesday February 05, 2020 @09:07AM
(#22246765)
There's the third sort of allocation that's often used in embedded systems - preallocated buffers, which are neither stack nor heap but set up by the .bss section of the executable.
These allow you to have very predictable memory usage.
Re:ZZ is a modern formally provable dialect of C
by a3p on Wednesday February 05, 2020 @02:07PM
(#22250023)
the standard library does not allocate any heap memory, but heap modelling will be added to the prover eventually.
note that there are convenience tools to deal with heap-free targets (microcontrollers) such as tail variants (statically enforced flexible arrays):
https://github.com/aep/zz#metaprogramming-or-templates-tail-...
Re:ZZ is a modern formally provable dialect of C
by pjmlp on Wednesday February 05, 2020 @09:09AM
(#22246778)
Unless it has changed, SPARK also forbids dynamic allocation.
Re:ZZ is a modern formally provable dialect of C
by yannickmoy on Thursday February 06, 2020 @03:21AM
(#22254409)
It has changed: https://blog.adacore.com/pointer-based-data-structures-in-sp...
Would be nice to have an actual microcontroller example.
> The standard library is fully stack based and heap allocation is strongly discouraged
:/ - I can see why this is done, as it's hard, so banning it to make the problem tractable works. But it's also quite inconvenient. On the other hand, "MISRA C:2004, 20.4 - Dynamic heap memory allocation shall not be used."