public inbox for gcc@gcc.gnu.org
 help / color / mirror / Atom feed
From: Michael Matz <matz@suse.de>
To: "Uecker, Martin" <Martin.Uecker@med.uni-goettingen.de>
Cc: "alx.manpages@gmail.com" <alx.manpages@gmail.com>,
	 "gcc@gcc.gnu.org" <gcc@gcc.gnu.org>,
	 "linux-man@vger.kernel.org" <linux-man@vger.kernel.org>,
	 "joseph@codesourcery.com" <joseph@codesourcery.com>,
	 "schwarze@usta.de" <schwarze@usta.de>,
	"wg14@soasis.org" <wg14@soasis.org>
Subject: Re: [PATCH] Various pages: SYNOPSIS: Use VLA syntax in function parameters
Date: Tue, 29 Nov 2022 15:44:02 +0000 (UTC)	[thread overview]
Message-ID: <alpine.LSU.2.20.2211291519160.24878@wotan.suse.de> (raw)
In-Reply-To: <5ccbf8ed11bd542477980f58aa277bf4335f1281.camel@med.uni-goettingen.de>

[-- Attachment #1: Type: text/plain, Size: 2427 bytes --]

Hey,

On Tue, 29 Nov 2022, Uecker, Martin wrote:

> It does not require any changes on how arrays are represented.
> 
> As part of VM-types the size becomes part of the type and this
> can be used for static or dynamic analysis, e.g. you can 
> - today - get a run-time bounds violation with the sanitizer:
> 
> void foo(int n, char (*buf)[n])
> {
>   (*buf)[n] = 1;
> }

This can already statically analyzed as being wrong, no need for dynamic 
checking.  What I mean is the checking of the claimed contract.  Above you 
assure for the function body that buf has n elements.  This is also a 
pre-condition for calling this function and _that_ can't be checked in all 
cases because:

  void foo (int n, char (*buf)[n]) { (*buf)[n-1] = 1; }
  void callfoo(char * buf) { foo(10, buf); }

buf doesn't have a known size.  And a pre-condition that can't be checked 
is no pre-condition at all, as only then it can become a guarantee for the 
body.

The compiler has no choice than to trust the user that the pre-condition 
for calling foo is fulfilled.  I can see how being able to just check half 
of the contract might be useful, but if it doesn't give full checking then 
any proposal for syntax should be even more obviously orthogonal than the 
current one.

> For
> 
> void foo(int n, char buf[n]);
> 
> it semantically has no meaning according to the C standard,
> but a compiler could still warn. 

Hmm?  Warn about what in this decl?

> It could also warn for
> 
> void foo(int n, char buf[n]);
> 
> int main()
> {
>     char buf[9];
>     foo(buf);
> }

You mean if you write 'foo(10,buf)' (the above, as is, is simply a syntax 
error for non-matching number of args).  Or was it a mispaste and you mean 
the one from the godbolt link, i.e.:

void foo(char buf[10]){ buf[9] = 1; }
int main()
{
    char buf[9];
    foo(buf);
}

?  If so, yeah, we warn already.  I don't think this is an argument for 
(or against) introducing new syntax.

...

> But in general: This feature is useful not only for documentation
> but also for analysis.

Which feature we're talking about now?  The ones you used all work today, 
as you demonstrated.  I thought we would be talking about that ".whatever" 
syntax to refer to arbitrary parameters, even following ones?  I think a 
disrupting syntax change like that should have a higher bar than "in some 
cases, depending on circumstance, we might even be able to warn".


Ciao,
Michael.

  reply	other threads:[~2022-11-29 15:44 UTC|newest]

Thread overview: 69+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
     [not found] <20220826210710.35237-1-alx.manpages@gmail.com>
     [not found] ` <Ywn7jMtB5ppSW0PB@asta-kit.de>
     [not found]   ` <89d79095-d1cd-ab2b-00e4-caa31126751e@gmail.com>
     [not found]     ` <YwoXTGD8ljB8Gg6s@asta-kit.de>
     [not found]       ` <e29de088-ae10-bbc8-0bfd-90bbb63aaf06@gmail.com>
     [not found]         ` <5ba53bad-019e-8a94-d61e-85b2f13223a9@gmail.com>
     [not found]           ` <CACqA6+mfaj6Viw+LVOG=nE350gQhCwVKXRzycVru5Oi4EJzgTg@mail.gmail.com>
     [not found]             ` <491a930d-47eb-7c86-c0c4-25eef4ac0be0@gmail.com>
2022-09-02 21:57               ` Alejandro Colomar
2022-09-03 12:47                 ` Martin Uecker
2022-09-03 13:29                   ` Ingo Schwarze
2022-09-03 15:08                     ` Alejandro Colomar
2022-09-03 13:41                   ` Alejandro Colomar
2022-09-03 14:35                     ` Martin Uecker
2022-09-03 14:59                       ` Alejandro Colomar
2022-09-03 15:31                         ` Martin Uecker
2022-09-03 20:02                           ` Alejandro Colomar
2022-09-05 14:31                             ` Alejandro Colomar
2022-11-10  0:06                           ` Alejandro Colomar
2022-11-10  0:09                             ` Alejandro Colomar
2022-11-10  1:33                             ` Joseph Myers
2022-11-10  1:39                               ` Joseph Myers
2022-11-10  6:21                                 ` Martin Uecker
2022-11-10 10:09                                   ` Alejandro Colomar
2022-11-10 23:19                                   ` Joseph Myers
2022-11-10 23:28                                     ` Alejandro Colomar
2022-11-11 19:52                                     ` Martin Uecker
2022-11-12  1:09                                       ` Joseph Myers
2022-11-12  7:24                                         ` Martin Uecker
2022-11-12 12:34                                     ` Alejandro Colomar
2022-11-12 12:46                                       ` Alejandro Colomar
2022-11-12 13:03                                       ` Joseph Myers
2022-11-12 13:40                                         ` Alejandro Colomar
2022-11-12 13:58                                           ` Alejandro Colomar
2022-11-12 14:54                                           ` Joseph Myers
2022-11-12 15:35                                             ` Alejandro Colomar
2022-11-12 17:02                                               ` Joseph Myers
2022-11-12 17:08                                                 ` Alejandro Colomar
2022-11-12 15:56                                             ` Martin Uecker
2022-11-13 13:19                                               ` Alejandro Colomar
2022-11-13 13:33                                                 ` Alejandro Colomar
2022-11-13 14:02                                                   ` Alejandro Colomar
2022-11-13 14:58                                                     ` Martin Uecker
2022-11-13 15:15                                                       ` Alejandro Colomar
2022-11-13 15:32                                                         ` Martin Uecker
2022-11-13 16:25                                                           ` Alejandro Colomar
2022-11-13 16:28                                                         ` Alejandro Colomar
2022-11-13 16:31                                                           ` Alejandro Colomar
2022-11-13 16:34                                                             ` Alejandro Colomar
2022-11-13 16:56                                                               ` Alejandro Colomar
2022-11-13 19:05                                                                 ` Alejandro Colomar
2022-11-14 18:13                                                           ` Joseph Myers
2022-11-28 22:59                                                             ` Alex Colomar
2022-11-28 23:18                                                       ` Alex Colomar
2022-11-29  0:05                                                         ` Joseph Myers
2022-11-29 14:58                                                         ` Michael Matz
2022-11-29 15:17                                                           ` Uecker, Martin
2022-11-29 15:44                                                             ` Michael Matz [this message]
2022-11-29 16:58                                                               ` Uecker, Martin
2022-11-29 17:28                                                                 ` Alex Colomar
2022-11-29 16:49                                                           ` Joseph Myers
2022-11-29 16:53                                                             ` Jonathan Wakely
2022-11-29 17:00                                                               ` Martin Uecker
2022-11-29 17:19                                                                 ` Alex Colomar
2022-11-29 17:29                                                                   ` Alex Colomar
2022-12-03 21:03                                                                     ` Alejandro Colomar
2022-12-03 21:13                                                                       ` Andrew Pinski
2022-12-03 21:15                                                                       ` Martin Uecker
2022-12-03 21:18                                                                         ` Alejandro Colomar
2022-12-06  2:08                                                                       ` Joseph Myers
2022-11-14 17:52                                                 ` Joseph Myers
2022-11-14 17:57                                                   ` Alejandro Colomar
2022-11-14 18:26                                                     ` Joseph Myers
2022-11-28 23:02                                                       ` Alex Colomar
2022-11-10  9:40                             ` G. Branden Robinson
2022-11-10 10:59                               ` Alejandro Colomar
2022-11-10 22:25                                 ` G. Branden Robinson

Reply instructions:

You may reply publicly to this message via plain-text email
using any one of the following methods:

* Save the following mbox file, import it into your mail client,
  and reply-to-all from there: mbox

  Avoid top-posting and favor interleaved quoting:
  https://en.wikipedia.org/wiki/Posting_style#Interleaved_style

* Reply using the --to, --cc, and --in-reply-to
  switches of git-send-email(1):

  git send-email \
    --in-reply-to=alpine.LSU.2.20.2211291519160.24878@wotan.suse.de \
    --to=matz@suse.de \
    --cc=Martin.Uecker@med.uni-goettingen.de \
    --cc=alx.manpages@gmail.com \
    --cc=gcc@gcc.gnu.org \
    --cc=joseph@codesourcery.com \
    --cc=linux-man@vger.kernel.org \
    --cc=schwarze@usta.de \
    --cc=wg14@soasis.org \
    /path/to/YOUR_REPLY

  https://kernel.org/pub/software/scm/git/docs/git-send-email.html

* If your mail client supports setting the In-Reply-To header
  via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for read-only IMAP folder(s) and NNTP newsgroup(s).