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.
[ Parent
| on HN ]
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...