>> There are C-compilers available for PICmicros that are "bug-free".

> Hmm, even allowing for the quote marks this is a dangerous assertion.

The reason I put these quote marks there is because nothing can be 100%
guarranteed.  I have been using a C compiler for PICs now for a few
years, and haven't yet had problems with the generated code.  The only
times I have to check the generated code during developement, is when
I need correct timing.

> Proving the correctness of anything as complicated as a compiler is a
> daunting undertaking.  If any supplier of a Pic 'C' compiler is
> prepared to prove its correctness, I would be very interested in
> hearing it.

http://www.riksnett.no/cc5x

If you choose to look at it, you will see that it supports a
C-subset that is directly related to the capabilities of a PICmicro.


-Dag