[SystemSafety] Subversive C programs for mockery of static analysis tools ... on a bad day ; -)

[Roderick Chapman]

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