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

[David Crocker]

Olwyn, where can I find the source file cimplex-d-0008.c ? Google
doesn't appear to have heard of it.

David Crocker, Escher Technologies Ltd.
http://www.eschertech.com
Tel. +44 (0)20 8144 3265 or +44 (0)7977 211486

On 30/11/2018 13:11, Olwen Morgan wrote:
>
> 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
>
> _______________________________________________
> The System Safety Mailing List
> systemsafety at TechFak.Uni-Bielefeld.DE
> Manage your subscription:
> https://lists.techfak.uni-bielefeld.de/mailman/listinfo/systemsafety