|
|
|
|
|
|
by onox
1977 days ago
|
|
|
C libraries/applications like these, which have many memory and logic bugs, should be written in SPARK. It can fully prove that your code is correct. The latest version of the SPARK tools can also handle ownership of pointers [1] (scroll down a little to the ownership_transfer.adb example) So RIIS it is! ;) [1] https://learn.adacore.com/courses/intro-to-spark/chapters/01... |
|
|