Jeffrey Yasskin <jyasskin_at_[hidden]> writes:

| On Tue, Aug 27, 2013 at 10:28 AM, Xavier Leroy <Xavier.Leroy_at_[hidden]> wrote:
| > On 27/08/13 17:48, Jeffrey Yasskin wrote:
| >>> - As a semanticist, I think it would be challenging to formalize, for
| >>> the general reasons given above.
| >>
| >> How do you model std::less<T*>, which already requires this total but
| >> unspecified order?
| >
| > No one tried, as far as I know. We (as a community) are still a long
| > way from formalizing the complete semantics of a "big" language like
| > C++, but an even longer way from formalizing specs for its standard
| > library...
| >
| > There are plausible ways to formalize this total order at the source
| > language level. But, as Gabriel wrote, the difficulty is to ensure
| > that your source-level semantics is not making predictions that the
| > compiler could invalidate later.
| >
| > In other words: at the end of the day, your pointers are just bit
| > patterns that the hardware compares as if they were integers. If you
| > could chase this hardware ordering of pointers back every compilation
| > pass, it should be the case that the source-level ordering you obtain
| > is one of those allowed by your source-level semantics. Proving this
| > kind of properties sounds very challenging to me.
|
| Mhmm. It sounds like you probably can't model the
| implementation-defined conversion to intptr_t yet either? Since
| T*->intptr_t->T* has to be an identity map, and intptr_t is totally
| ordered.

I forgot to add: See section 3.2 of Chapter 5 at

  http://compcert.inria.fr/man/manual005.html#language-reference
  

|
| If that's the case, it sounds like making operator< on T* a total
| order would reduce the fraction of C++ that's currently formalizable
| but wouldn't make it any harder to formalize the whole language?
| _______________________________________________
| ub mailing list
| ub_at_[hidden]
| http://www.open-std.org/mailman/listinfo/ub