signed is undefined and has been since 1992 (in GCC)

[Gabriel Dos Reis]

Robert Dewar <dewar@adacore.com> writes:

| Gabriel Dos Reis wrote:
| 
| >  C is
| > trustworthy (and preferred over SML for that curcial part of the proof
| > checker) because the mapping of the C code to the generated assembly
| > code is straighforward and amenable to inspection.
| 
| This kind of traceability is of course vital for such applications, but
| it is by no means unique to C,

Nobody claims it is unique to C.  You're after the wrong target.

| and there is a big difference between saying
| that C is an assembly language, and that the mapping of C to assembly
| language is transparent.

Oh, you denied any connection in previous message.

-- Gaby