Hello...
There is still a problem with C++ and C
About Escher C++ Verifier, read carefully:
"Escher C Verifier enables the development of formally-verifiable
software in a subset of C (based on MISRA-C 2012)."
Read here:
http://www.eschertech.com/products/index.php
So it verifies just a "subset" of C, so that's not good for C++
because for other applications that are not a subset of C , it can
not do for example Run-time checks, so we are again into
this problem again, so read the following carefully:
I think that Delphi and FreePascal like ADA come with range checking and
Run-time checks that catch conversion from negative signed to unsigned ,
and catch out-of-bounds indices of dynamic and static arrays and catch
arithmetic overflow etc. and you can also dynamically catch this
exception of ERangeError etc.
But C++ and C don't have range checking etc. so that's not good in C++
and C because it is not good for safety-critical systems.
You can carefully read the following, it is very important:
https://critical.eschertech.com/2010/07/07/run-time-checks-are-they-worth-it/
Thank you,
Amine Moulay Ramdane.