Path: csiph.com!weretis.net!feeder6.news.weretis.net!news.misty.com!news.iecc.com!.POSTED.news.iecc.com!nerds-end From: Keith Thompson Newsgroups: comp.compilers Subject: Re: C arithmetic, was Software proofs, was Are there different Date: Sun, 05 Feb 2023 16:14:57 -0800 Organization: None to speak of Sender: johnl@iecc.com Approved: comp.compilers@iecc.com Message-ID: <23-02-025@comp.compilers> References: <23-01-092@comp.compilers> <23-02-003@comp.compilers> <23-02-019@comp.compilers> MIME-Version: 1.0 Content-Type: text/plain Injection-Info: gal.iecc.com; posting-host="news.iecc.com:2001:470:1f07:1126:0:676f:7373:6970"; logging-data="272"; mail-complaints-to="abuse@iecc.com" Keywords: C, arithmetic Posted-Date: 05 Feb 2023 21:00:59 EST X-submission-address: compilers@iecc.com X-moderator-address: compilers-request@iecc.com X-FAQ-and-archives: http://compilers.iecc.com Xref: csiph.com comp.compilers:3368 [...] > [The history of formal description of programming languages is not > encouraging. Back in the 1970s the ANSI PL/I standard was defined in > terms of formal operations on trees, but even so it had bugs/errors. > Also, per your comment on addition, in a lot of cases the practical > definition turns into whatever the underlying machine's instruction > does. Until recently the C standard was deliberately unclear about > whether arithmetic was ones- or twos-complement. -John] The C standard still doesn't mandate two's-complement. The 1990 edition of the C standard was vague about integer representations, though it did impose some requirements. It required a "pure binary" representation, and it required, for example, a value that is within the range of both int and unsigned int to have the same representation in both. That excluded some of the more exotic possibilites. (It mentioned 2's complement a few times, but only as an example.) The 1999 standard explicitly required one of three representations: sign and magnitude, two's complement, or one's complement. It also explicitly permitted padding bits (bits that don't contribute to the value, and that can either be ignored or create trap representations). The 2011 standard corrected the spelling of "ones' complement", but otherwise didn't change anything significant. (The 2017 edition was a minor update.) The upcoming 2023 standard mandates two's complement. And it requires INT_MIN to be exactly -INT_MAX-1; previously INT_MIN could be equal to -INT_MAX, and -INT_MAX-1 could be a trap representation. It still permits padding bits and trap representations. Note that twos's complement *representation* doesn't imply two's complement *behavior* on overflow. Signed integer overflow still has undefined behavior. -- Keith Thompson (The_Other_Keith) Keith.S.Thompson+u@gmail.com Working, but not speaking, for XCOM Labs void Void(void) { Void(); } /* The recursive call of the void */