Hi John,
thanks to your suggestion of Frama-C, I've had a lot more luck with reducing
wrong code bugs. I have noticed a few sorts of errors that Frama-C doesn't
seem to flag though. I was curious if other people have encountered these, and
what, if any workarounds can be used:
1) Signed overflow
for(char c = 1; c; c++) ;
2) Invalid union accesses
union { char c; short s; } u;
u.s = 1;
u.c = 0;
printf("%d\n", u.s);
3) Aliased access to unions
union { char c; short s; } u;
char *c = &u.c;
short *s = &u.s;
*c = 1;
*s = 2;
printf("%d\n", u.s);
Also, I've been using the frama-c from
creduce/scripts/test1_wrong_code_framac.sh and two of the options don't seem to
exist on the latest (Fluorine) release:
-val-signed-overflow-alarms and -precise-unions . If anybody knows their
current equivalents, that would be most helpful!
Thanks again for a great tool,
Dara
----- Original Message -----
From: John Regehr <[email protected]>
To: Dara Hazeghi <[email protected]>
Cc: "[email protected]" <[email protected]>
Sent: Wednesday, April 17, 2013 3:03 PM
Subject: Re: [creduce-dev] wrong-code reduction process
Hi Dara, please try Frama-C as your undefined behavior checker, it is
much faster than KCC.
If you cannot get Frama-C to work, sometimes problems can be avoided
using weaker tools such as Valgrind or Clang's undefined behavior sanitizer.
John
On 04/17/2013 03:44 PM, Dara Hazeghi wrote:
> Hello,
>
> I've been using c-reduce quite extensively to reduce testcases for C compiler
> crash bugs, and it's been invaluable. However I also have a substantial
> collection of what I believe to be wrong code bugs that I'm trying to reduce.
>
> I've tried using c-reduce for those as well, and I'm running into
> difficulties detecting undefined/unspecified behavior during the reduction
> process. Based on the c-reduce paper, I gather you found kcc and frama-c to
> be sufficient for that task. I've just given kcc a whirl and it seemed to be
> prohibitively slow for non-trivial testcases. I was wondering if there was a
> special way you used kcc to avoid this slowness, or what other tool(s) I
> might use to keep the reduction process both sound and reasonably fast. Many
> thanks,
>
> Dara
>
