Re:Checked C
by ZiiS on Wednesday December 21, 2022 @08:07PM
(#34088468)
You simply have go treat that as always unsound.
[ Parent
| on HN ]
Re:Checked C
by 95014_refugee on Wednesday December 21, 2022 @11:50PM
(#34089944)
This is essentially the status quo, and it's not helpful. Better is possible.
> This is essentially the status quo, and it's not helpful. Better is possible.
It is helpful, since if you address all of the complaints, then your code will be proven to be free of the issues that the sound static analyzer can detect. In theory, you can produce C code that is proven to be memory safe by doing that, which effectively makes it semi-formally verified code. Unlike other methods of doing semi-formal verification, this method is actually usable by an average programmer.
Would you explain to me how that is the status quo? How would you do better?