[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [csmith-dev] Checksum, different options

Hi Paulo,

Pascal's suggestions are all excellent.

The problem that you now face is testcase reduction. You can approach this by hand (and I recommend that you do this for the first few bugs) but there are also partially automated solutions:


The key is that you need to run a tool like Pascal's or Chucky's inside the Delta test script. Otherwise, undefined behavior is almost always added by Delta.

The Delta test scripts that I personally use have gotten pretty baroque, unfortunately. They look for a lot of compiler warnings, run Valgrind, and as a last resort run a more expensive tool like KCC/Frama-C.


On 09/12/2011 07:40 AM, Paulo J. Matos wrote:
Thanks for your analysis on the file I sent. I will take a look at it
now. By the way? Is the analysis you made to check definedness something
I can to on my end? Is it a special option to frama-c? Is this similar
to C-semantics (http://code.google.com/p/c-semantics/)?

Will keep you up-to-date.


Paulo Matos

On 12/09/11 14:14, Pascal Cuoq wrote:
> I attach the program. Even if it doesn't confirm it's defined for my
arch, at least (I suspect) if it's not defined for standard arch, it's
not defined for mine either.

The program seems defined for usual ILP32 architectures. It seems
you will have to investigate.

After determining which global causes the difference in checksums (let's
assume it's int G),
I like to replace in the program the regexp: /[*] block id: \([0-9]*\)
by: printf("block: %u, G: %d\n", \1, G);

Usually, if you are lucky, this does not perturb compilation enough to
hide the bug,
and it suffices to determine where the execution traces diverge and/or
G gets a different value.


To report this email as spam click here

Member of the CSR plc group of companies. CSR plc registered in England
and Wales, registered number 4187346, registered office Churchill House,
Cambridge Business Park, Cowley Road, Cambridge, CB4 0WZ, United Kingdom
More information can be found at www.csr.com. Follow CSR on Twitter at
http://twitter.com/CSR_PLC and read our blog at www.csr.com/blog