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.
Cheers,
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
where
G gets a different value.
Pascal
To report this email as spam click here
<https://www.mailcontrol.com/sr/wQw0zmjPoHdJTZGyOCrrhg==>.
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