This is a great achievement in making formal methods accessible in pragmatic terms - something that actually works and can be used by normal humans.
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."
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.
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."