[SystemSafety] Subversive C programs for mockery of static analysis tools ... on a bad day ; -)
Roderick Chapman
roderick.chapman at googlemail.com
Sat Dec 1 10:39:51 CET 2018
On 30/11/2018 13:11, Olwen Morgan wrote:
> Feel free to translate any of my programs into SPARK Ada if possible
> and throw them at the SPARK verification tools.
Hardly worth even trying... your examples so far use expressions with
side-effects. These are illegal in SPARK and trivially rejected by the
SPARK toolset.
I agree with your informal definition of "break" by the way - basically
the toolset says all is well for property X, but property X is obviously
not true when the program is compiled and run. Therefore "broken" =
"unsound" = "false negative" in the way the terms are normally used.
- Rod
More information about the systemsafety
mailing list