[M3commit] CVS Update: cm3
Jay K
jay.krell at cornell.edu
Mon Jul 5 23:46:49 CEST 2010
Meeting the language spec is inadequate.
It is a "quality of implementation" thing.
Do you want your C compiler to be silent about this code? No.
Or do you want it to try a little harder and point out bugs in your code? Even where it meets the language spec? Yes.
Maybe meeting the language spec is more meaningful for Modula-3 than for C, but still inadequate.
Now, compiler can't in general be a "correct program proofer", but it can and does catch a few things and that is a good thing not to be avoided.
- Jay
----------------------------------------
> From: hosking at cs.purdue.edu
> Date: Mon, 5 Jul 2010 17:40:50 -0400
> To: jay.krell at cornell.edu
> CC: m3commit at elegosoft.com
> Subject: Re: [M3commit] CVS Update: cm3
>
> But the front-end should be OK with the first. It is "correct" because whatever value is in a when F1 is called is legal for a. Why should the backend give a warning? The semantics of Modula-3 allow any legal bit-value for a variable as its initial value. You will force an initialising assignment when none is required by the language spec.
>
> On 5 Jul 2010, at 17:36, Jay K wrote:
>
> >
> > unsigned F1()
> > {
> > unsigned a;
> > return a;
> > }
> >
> > should generate a warning.
> >
> > unsigned F1()
> >
> > {
> >
> > unsigned a = 0;
> >
> > return a;
> >
> > }
> >
> >
> > is much preferred.
> >
> > Just because the front end is ok with the first, doesn't make it correct.
> >
> > - Jay
> >
> > ----------------------------------------
> >> Subject: Re: [M3commit] CVS Update: cm3
> >> From: hosking at cs.purdue.edu
> >> Date: Mon, 5 Jul 2010 17:34:51 -0400
> >> CC: m3commit at elegosoft.com
> >> To: jay.krell at cornell.edu
> >>
> >> Huh?
> >>
> >> On 5 Jul 2010, at 17:15, Jay K wrote:
> >>
> >>>
> >>> At least some of these were Word.T. "valid" is still "random" and the code is unpredictable, at least by a quick read, even if type safe.
> >>> Type safe is just a minimum bar, one that should always be exceeded, even if the compiler is completely unable to validate it.
> >>>
> >>> That is, the compiler guarantees are from sufficient relative to correctness.
> >>>
> >>> - Jay
> >>>
> >>> ----------------------------------------
> >>>> From: hosking at cs.purdue.edu
> >>>> Date: Mon, 5 Jul 2010 16:50:00 -0400
> >>>> To: jay.krell at cornell.edu
> >>>> CC: m3commit at elegosoft.com
> >>>> Subject: Re: [M3commit] CVS Update: cm3
> >>>>
> >>>> But we've been this route before. Modula-3 ensures every variable is initialised with a valid value. I don't see how your adding an initialiser makes it more obviously correct.
> >>>>
> >>>> On 5 Jul 2010, at 16:45, Jay K wrote:
> >>>>
> >>>>>
> >>>>> I will maybe see about doing better here.
> >>>>> Initializing locals doesn't seem like such a bad change though.
> >>>>> I like the code to be "obviously correct" by a quick read by a human.
> >>>>>
> >>>>> - Jay
> >>>>>
> >>>>> ----------------------------------------
> >>>>>> From: hosking at cs.purdue.edu
> >>>>>> Date: Mon, 5 Jul 2010 14:31:01 -0400
> >>>>>> To: jkrell at elego.de
> >>>>>> CC: m3commit at elegosoft.com
> >>>>>> Subject: Re: [M3commit] CVS Update: cm3
> >>>>>>
> >>>>>> Jay, I am perplexed that we are adding things to Modula-3 source because of compiler backend brokenness just to avoid back-end warnings. Better to fix the backend so that RAISE is noreturn. This should not be difficult to do.
> >>>>>>
> >>>>>> On 5 Jul 2010, at 15:22, Jay Krell wrote:
> >>>>>>
> >>>>>>> CVSROOT: /usr/cvs
> >>>>>>> Changes by: jkrell at birch. 10/07/05 15:22:28
> >>>>>>>
> >>>>>>> Modified files:
> >>>>>>> cm3/m3-tools/cvsup/suplib/src/text_cm3/: SupMiscText.m3
> >>>>>>>
> >>>>>>> Log message:
> >>>>>>> ../src/text_cm3/SupMiscText.m3: In function 'SupMisc__DecodeWS':
> >>>>>>> ../src/text_cm3/SupMiscText.m3:211: warning: 'M3_Bkn9rd_ch' may be used uninitialized in this function
> >>>>>>> ../src/text_cm3/SupMiscText.m3:211: note: 'M3_Bkn9rd_ch' was declared here
> >>>>>>>
> >>>>>>> because raising an exception isn't currently "noreturn"
> >>>>>>> so initialize it to 0
> >>>>>>
> >>>>>
> >>>>
> >>>
> >>
> >
>
More information about the M3commit
mailing list