[M3commit] CVS Update: cm3
Tony Hosking
hosking at cs.purdue.edu
Tue Jul 6 00:42:20 CEST 2010
Your C compiler will be silent about this code unless you ask it to warn you.
On 5 Jul 2010, at 17:46, Jay K wrote:
> Meeting the language spec is inadequate.
What?
> It is a "quality of implementation" thing.
> Do you want your C compiler to be silent about this code? No.
Why not?
> Or do you want it to try a little harder and point out bugs in your code?
Those are C bugs because C says nothing about variable initialisation.
> 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