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

[Olwen Morgan]

On 30/11/2018 11:30, Roderick Chapman wrote:

<snip>

>
> I too have fun breaking other people's verifiers, but breaking C tools 
> is far too easy. Please try to break SPARK - you'll find it more of a 
> challenge. Please report anything you find either here, or to 
> spark at adacore.com ...
>
Of course, it all depends on what you mean by "breaking" and what 
constitutes an attempt at it. Essentially the aim is to write a program 
that satisfies a tool's language subset requirements and elicits from a 
verifier results that are inconsistent with those produced by the 
program when it is compiled the user's chosen compiler.

Feel free to translate any of my programs into SPARK Ada if possible and 
throw them at the SPARK verification tools. I'd be intrigued to know 
what an Ada analogue of cimplex-d-0008.c throws up. I've not yet 
succeeded in thinking up verifier-breaking C programs that would satisfy 
subset requirements analogous to those of SPARK and I've never written a 
program in my own ultra-strict coding style that has broken a verifier.

Broadly-speaking, the stricter the C subset you use, the trickier it is 
to come up with things that would break a verifier but not trigger a 
subset warning. OTOH, C verifiers are more varied than the SPARK tools 
and writing different programs that break different tools helps users to 
see what the differences in tool capability really are.

Olwen