From Newsgroup: comp.lang.c

Keith Thompson <Keith.S.Thompson+u@gmail.com> writes:

David Brown <david.brown@hesbynett.no> writes:

[...]

I think the semantics of this "loops can be assumed to terminate"
are clearly defined in the standard. [...]

I disagree that the semantics are clearly defined. N3220 6.8.6.1p4
is specified in terms of what an implementation may "assume", not in
terms of the semantics of the program.

It isn't obvious that the semantics of "may be assumed to terminate"
is even well defined by the text of the C standard; it certainly is
not clearly defined.

One can conclude that this
means that the program has undefined behavior if the assumption is
violated, but that's not directly stated. I don't know how many C programmers know the standard well enough to reach that conclusion.
I'm not even 100% sure it's accurate.

The permission was added in C11 with little fanfare. It's not
mentioned in the list of major changes in the C11 Foreword.
The cases where it applies may be rarer than I had assumed, but
it at least has the potential to break existing code that was well
defined in C99.

The rationale is to provide more opportunities for optimization,
but it's not at all clear (at least to me) that it's particularly
successful. If cases where it can cause problems are rare, then
presumably cases where it's actually useful are rare. (That may
be an oversimplification.)

If someone is counting votes my vote is to remove this rule from
the C standard. If there were a compiler option to act as though
this rule were not in force I would always use that option. It's
worse than useless.
--- Synchronet 3.22a-Linux NewsLink 1.2

From Newsgroup: comp.lang.c

cross@spitfire.i.gajendra.net (Dan Cross) writes:

In article <86mrwd7c49.fsf@linuxsc.com>,
Tim Rentsch <tr.17687@z991.linuxsc.com> wrote:

cross@spitfire.i.gajendra.net (Dan Cross) writes:

[...]

"Undefined Behavior", in C, in the manner usually discussed in
this newsgroup, was introduced with the first standard.

The term but not the concept, which was there since the
early days of C -- at least since K&R in 1978, and very
likely earlier (I haven't reviewed any of the earlier
descriptions of the language).

[...] not really. I've read K&R, both editions, and the
first really doesn't define a concept that gives such supreme
latitude to the compiler. [...]

I didn't say any term was defined, only that such a
concept is present in the writing.
--- Synchronet 3.22a-Linux NewsLink 1.2

From Newsgroup: comp.lang.c

cross@spitfire.i.gajendra.net (Dan Cross) writes:

In article <86ldcm82ql.fsf@linuxsc.com>,
Tim Rentsch <tr.17687@z991.linuxsc.com> wrote:

cross@spitfire.i.gajendra.net (Dan Cross) writes:

In article <86tsrc8d0b.fsf@linuxsc.com>,
Tim Rentsch <tr.17687@z991.linuxsc.com> wrote:
[...]

The C standard doesn't need to say that, for example, a
function x() other than main(), whose name is never referenced,
will never be called. If someone wants to establish that x() could
be called, there needs to be a chain of reasoning going through the
semantic descriptions given in the C standard, to show that a call
to x() could occur.

Actually, no, a reference to a function is not necessary. A
couple of years ago, a well-publicized issue in a C++ compiler a
couple of years ago was something along the lines of this:
[...]

This is comp.lang.c. My comments were only about C, and not
about C++. But of course you already knew that.

I see you did not read the other messages in the (sub)thread,
but ok, here it is again, in C:

```
term% cat what.c
#include <stdio.h>
int main(void) { for (unsigned int k = 0; k != 1; k += 2); return 0; }
void hello(void) { printf("Hello, World!\n"); }
term% clang --version | sed 1q
clang version 22.1.6
term% clang -Wall -pedantic -pedantic-errors -O1 -std=c23 -o what what.c what.c:2:58: warning: for loop has empty body [-Wempty-body]
2 | int main(void) { for (unsigned int k = 0; k != 1; k += 2); return 0; }
| ^
what.c:2:58: note: put the semicolon on a separate line to silence [...]
1 warning generated.
term% ./what
Hello, World!
term%
```

This is a childish argument.
--- Synchronet 3.22a-Linux NewsLink 1.2

From Newsgroup: comp.lang.c

antispam@fricas.org (Waldek Hebisch) writes:

Tim Rentsch <tr.17687@z991.linuxsc.com> wrote:

antispam@fricas.org (Waldek Hebisch) writes:

[...]

I think that lawyerish style of current C standard is mostly
inertia,

I wouldn't use a term like lawyerish to describe the text in the
ISO C standard. Can you explain what quality you mean to ascribe
to "lawyerish" writing in the C standard without using any term
related to lawyering or legal documents?

Sorry no, I can not. My point is that you need to treat
C standard almost like legal document and I can not explain
this without using proper terminology.

and making standard more mathematical would improve it.

Could you elaborate on that statement? In what ways would giving
a more mathematical treatment of C semantics improve the quality
of the ISO C document? How would doing that advance the stated
purposes or goals of the C standard?

There are many aspect of mathematical treatment. One is care
about terminology, namely that terms are either reasonably
clearly marked as "primitve" (and assumed to be understood
by readers) or are precisely defined. Related is that
words can be taken as written, without needing to look at
intent or similar legal style arguments. You may think that
C standard already posseses such properties, but recent
example, that is definition of expression nicely illustrates
current problems. With mathematical treatment expression
would be part of C program derived from corresponding
grammar rule and that would resolve the problem. In the
past in this group there were several discussions about
various parts of C standard, and there were cases were
standard wording looked genuinly confusing. I am not
prepared to dig into those discussions, but my impression
was that in some cases mathematical treatment would make
things clearer.

But giving formal semantic in the standard would mean
significantly bigger change.

Due to the nature of C, I believe it is effectively impossible to
give a formal mathematical definition of the semantics of C. Do
you think such a thing is feasible or practicable? If so can you
explain the reasoning behind your thinking?

I think that this is possible given dedicated team of qualified
people doing the work. I do not know if it is practically
possible to assemble needed team. I already mentioned axiomatic
semantics. There is C grammar and we need to assign semantics
to various production rules. We do this assigning precondtions
and postcondtions to the rules. In much simpler cases this
was done. C is bigger language and rules are more complicated,
but that for me looks like quantitive problem, that is there is
more work and result will be bigger. Clearly, this would
require buy-in from the standard body. Namely, formalization
is likely to uncover many unclear places in C standard and
ensuring that formalization matches the standard would require
resolution by the standard body. It is quite possible that
standard body would refuse to cooperate. To explain this more,
let me mention past discussion about Extended Pascal in a
different forum. I was looking at types of constants, but in
specific case rules looked contradictory, so I asked a
question. One response was from former commitee member (this
was several years after Pascal standard was ratified), he
basicaly said that type of constants does not matter. Which
was mostly true, but my reason for asking the question was
that validity of programs depended on types of constants.
Something similar may happen during formalization:
formalization may discover unclear places in C standard
which C commitee considers irrelevant in practice and
refuses to clarify.

BTW: Authors of some tools already need and have formal
semantics for language rather close to C. Namely,
Comp-Cert compiler is matching conditions in source
code with machine code and for that it needs reasonably
good aproximation to formal semantics of language implemented
by C compiler (more precisely gcc). Microsoft developed
formal checking tools and that too needs formal semantics.
But since goals are different neither give semantics of
standard C.

A disappointing response. You can't explain what you mean.
The properties ascribed to a mathematical writing might
just as well be met by more clearly written English. About
defining a formal semantics, all you really say is you think
it is possible, under some not very well defined conditions.
All in all not too compelling.
--- Synchronet 3.22a-Linux NewsLink 1.2