Prev: Structural unification (pattern matching) in Ada [was: Re: S-expression I/O in Ada]
Next: SPARK POGS: List the rules used by the Simplifier
From: Warren on 13 Aug 2010 10:20
This week I've been busy porting last year's C++
version of my midi library over to Ada (now that I'm
using AVR-Ada). As part of that effort, the Ada
compiler has discovered a few errors that were
lurking still in the C++ Arduino code.

In C++ I had defined:

/*
* MC_CTL_CHG Control values :
*/
#define MC_CTL_ALLS_OFF 0x78 // All sounds off (120)
#define MC_CTL_RESET_C 0x79 // Reset controller
#define MC_CTL_LOCAL_C 0x80 // Local on/off
#define MC_CTL_ALLN_OFF 0x81 // All notes off
#define MC_CTL_OMNI_OFF 0x82 // Omni off request
#define MC_CTL_OMNI_ON 0x83 // Omni on request
#define MC_CTL_MONO_ON 0x84 // Mono on == POLY OFF
#define MC_CTL_MONO_OFF 0x85 // Mono off == POLY ON

But in Ada, when I declared:

type Control_Type is new Unsigned_8 range 0..127;

and then coded:

case Control is
when MC_CTL_ALLS_OFF => -- ok
...
when MC_CTL_LOCAL_C => -- oops
...

it immediately identified the value MC_CTL_LOCAL_C
(and others) as not fitting into the Control_Type's
valid range. In C++ a glaring error had gone
unnoticed:

#define MC_CTL_ALLS_OFF 0x78 // All sounds off (120)
#define MC_CTL_RESET_C 0x79 // Reset controller
#define MC_CTL_LOCAL_C 0x7A <==== not 0x80
#define MC_CTL_ALLN_OFF 0x7B <==== not 0x81..

Non commands in midi should not have had bit 7 set.
So as it was coded, those control messages would
never have been processed in the C++ lib.

I'm always smiling when I convert code from C/C++ to
Ada. In code of any significant size, Ada always
discovers problems that went unnoticed in C/C++.

Warren
From: Yannick Duchêne (Hibou57) on 13 Aug 2010 11:06
Le Fri, 13 Aug 2010 16:20:16 +0200, Warren <ve3wwg(a)gmail.com> a écrit:
> it immediately identified the value MC_CTL_LOCAL_C
> (and others) as not fitting into the Control_Type's
> valid range. In C++ a glaring error had gone
> unnoticed:
> [...]
> I'm always smiling when I convert code from C/C++ to
> Ada. In code of any significant size, Ada always
> discovers problems that went unnoticed in C/C++.

Makes me think about a recent case where I though “A C/C++ compiler would
have never caught it”. This was with AdaDep, a tool from AdaLog (by J.P.
Rosen). Since the last revision of Ada, ASIS has also evolved and added a
new item in the Asis.Element_Kinds enumeration (this item is
An_Expression_Path). Immediately caught by Ada in AdaDep which was not
compiling anymore, and the same in another other little application of
mine.

This indeed help to feel at rest when you see such missing/oversight
immediately caught.


--
There is even better than a pragma Assert: a SPARK --# check.
--# check C and WhoKnowWhat and YouKnowWho;
--# assert Ada;
-- i.e. forget about previous premises which leads to conclusion
-- and start with new conclusion as premise.
From: Anh Vo on 13 Aug 2010 12:53
On Aug 13, 7:20 am, Warren <ve3...(a)gmail.com> wrote:

> it immediately identified the value MC_CTL_LOCAL_C
> (and others) as not fitting into the Control_Type's
> valid range. In C++ a glaring error had gone
> unnoticed:
[...]
> I'm always smiling when I convert code from C/C++ to
> Ada. In code of any significant size, Ada always
> discovers problems that went unnoticed in C/C++.
>

I am smiling, too, since I am not surprised at all. When someone asks
me what difference between computer languages especially between Ada
and C/C++, I tell him Ada has 75% check at compile time and 25% and
runtime while C/C++ in reverse.

Anh Vo
 | 
Pages: 1
Prev: Structural unification (pattern matching) in Ada [was: Re: S-expression I/O in Ada]
Next: SPARK POGS: List the rules used by the Simplifier