Re: Finding out parameters which are not written

Re: Finding out parameters which are not written

[Robert Dewar]

>Gerhard Radatz <gerhard.radatz@aut.alcatel.at> writes:
<< Does anyone know about a tool which can detect such situations as the
   following:
  
        procedure xxx (result: out INTEGER) is
           begin
             if <<condition>> then
                 result := 0;
                end if;
           end;
  
   Obviously, this proc is erroneous and result will not be written if
   <<condition>> is FALSE.
   However, my Ada-Compiler (DEC-ADA for VMS) does not detect this problem,
   because result is written "at least once" in the body of xxx.
  
   Is there any tool which can provide help ??? >>


Using the standard version of GNAT with -Wuninitialized and -O2, we get

xxx.adb: In function `xxx':
xxx.adb:1: warning: `result' might be used uninitialized in this function

Not very localized, but better than not getting a warning at all!

Finding out parameters which are not written

[Gerhard Radatz]

Does anyone know about a tool which can detect such situations as the
following:

	procedure xxx (result: out INTEGER) is
        begin
	     if <<condition>> then
	         result := 0;
             end if;
        end;

Obviously, this proc is erroneous and result will not be written if
<<condition>> is FALSE.
However, my Ada-Compiler (DEC-ADA for VMS) does not detect this problem,
because result is written "at least once" in the body of xxx.

Is there any tool which can provide help ???

Re: Finding out parameters which are not written

[Gerhard Radatz]

Gerhard Radatz wrote:
> 
> Does anyone know about a tool which can detect such situations as the
> following:
> 
>         procedure xxx (result: out INTEGER) is
>         begin
>              if <<condition>> then
>                  result := 0;
>              end if;
>         end;
> 
> Obviously, this proc is erroneous and result will not be written if
> <<condition>> is FALSE.
> However, my Ada-Compiler (DEC-ADA for VMS) does not detect this problem,
> because result is written "at least once" in the body of xxx.
> 
> Is there any tool which can provide help ???

I admit that it is very difficult to find such potential problems at
compile time. Therefore, I'm rather looking for such a thing like an
expert system which can examine complex code, evaluate every possible
flow of control and at least give some hints.

Surely its best to code-read to be able to find out unwritten
parameters, but in projects consisting of a few hundred packages with a
few 100.000 lines of code, this is lots of work.

Re: Finding out parameters which are not written

[Robert A Duff]

In article <33F07EA1.51D1@aut.alcatel.at>,
Gerhard Radatz  <gerhard.radatz@aut.alcatel.at> wrote:
>Gerhard Radatz wrote:
>> 
>> Does anyone know about a tool which can detect such situations as the
>> following:
>> 
>>         procedure xxx (result: out INTEGER) is
>>         begin
>>              if <<condition>> then
>>                  result := 0;
>>              end if;
>>         end;
>> 
>> Obviously, this proc is erroneous and result will not be written if
>> <<condition>> is FALSE.

>I admit that it is very difficult to find such potential problems at
>compile time. ...

It doesn't seem so hard to me.  The compiler can just check whether
every path through the function assigns to every 'out' parameter of a
scalar type.  If not, warn -- it's almost certainly a bug.  (For
composite types, it's not formally erroneous, and not necessarily a
bug.)  There's no practical reason to worry about the fact that
<<condition>> might be always True (which of course the compiler can't
know, in general).

GNAT does exactly this sort of analysis for function returns -- it makes
sure that every path through the function ends with a return statement,
or the raise of an exception (and it has some mechanism for marking
procedures that always raise an exception).  I don't know if GNAT does
something similar for scalar 'out' parameters, but it could.

Of course, none of this solves the more general problem of uninitialized
objects -- that really requires run-time checks.

- Bob

Re: Finding out parameters which are not written

[Matthew Heaney]

In article <EEtC87.9CC@world.std.com>, bobduff@world.std.com (Robert A
Duff) wrote:

>Of course, none of this solves the more general problem of uninitialized
>objects -- that really requires run-time checks.

Does the safety annex apply here?  Can the Normalize_Scalars pragma apply
to subprogram parameters, too?

--------------------------------------------------------------------
Matthew Heaney
Software Development Consultant
<mailto:matthew_heaney@acm.org>
(818) 985-1271

Re: Finding out parameters which are not written

[Larry Kilgallen]

In article <33F02867.322D@aut.alcatel.at>, Gerhard Radatz <gerhard.radatz@aut.alcatel.at> writes:
> Does anyone know about a tool which can detect such situations as the
> following:
> 
> 	procedure xxx (result: out INTEGER) is
>         begin
> 	     if <<condition>> then
> 	         result := 0;
>              end if;
>         end;
> 
> Obviously, this proc is erroneous and result will not be written if
> <<condition>> is FALSE.
> However, my Ada-Compiler (DEC-ADA for VMS) does not detect this problem,
> because result is written "at least once" in the body of xxx.
> 
> Is there any tool which can provide help ???

Such a tool could not handle the case where <<condition>> depended on
some input determined outside the scope of the current compilation. A
static analysis that only works for the simple cases would seem to be
unattractive since those are precisely the cases where humans can best
spot the error.

Consider a long series of conditional tests each depending on different
arcane input.  If no condition results in setting the output, it would
seem that cannot be determined at compile time.  Run time detection is
a different matter, of course.

Larry Kilgallen

Re: Finding out parameters which are not written

[Fergus Henderson]

kilgallen@eisner.decus.org (Larry Kilgallen) writes:

>Gerhard Radatz <gerhard.radatz@aut.alcatel.at> writes:
>> Does anyone know about a tool which can detect such situations as the
>> following:
>> 
>> 	procedure xxx (result: out INTEGER) is
>>         begin
>> 	     if <<condition>> then
>> 	         result := 0;
>>              end if;
>>         end;
>> 
>> Obviously, this proc is erroneous and result will not be written if
>> <<condition>> is FALSE.
>> However, my Ada-Compiler (DEC-ADA for VMS) does not detect this problem,
>> because result is written "at least once" in the body of xxx.
>> 
>> Is there any tool which can provide help ???
>
>Such a tool could not [...]

I would just like to point out that such a tool _can_ work, and is
indeed very useful for detecting errors.  I know this because I wrote
just such a tool -- we call it a mode checker -- as part of the Mercury
compiler.  Mode checking is in fact an integral feature of the Mercury
language.  I and the rest of the Mercury group have used it for
developing well over 100 thousand lines of Mercury code.  Mode checking
works very well in our experience.

>Such a tool could not handle the case where <<condition>> depended on
>some input determined outside the scope of the current compilation.  A
>static analysis that only works for the simple cases would seem to be
>unattractive since those are precisely the cases where humans can best
>spot the error.

The idea is that the tool and the programmers cooperate to achieve the
desired effect.  Static analysis alone is either limited or limiting,
but static analysis in combination with some runtime checking works
extremely well.

The tool should only allow programs which it can prove will have no mode
errors.   So for the code above, since it cannot prove that <<condition>>
will always succeed, it would report an error.

The programmer will then rewrite the code as

 	     if <<condition>> then
 	         result := 0;
	     else
		 raise Some_Appropriate_Exception;
             end if;

which _will_ be accepted by the tool.

>Consider a long series of conditional tests each depending on different
>arcane input.  If no condition results in setting the output, it would
>seem that cannot be determined at compile time.  Run time detection is
>a different matter, of course.

Such cases where the program depends on complex assertions (such as the
assertion that at least one of "a long series of conditional tests each
depending on different arcane input" will succeed) are exactly the
sorts of cases which programmers often get wrong, or which easily get
broken during maintentance.  Hence it is extremely useful to include
runtime error detection for these cases.  During the development of the
Mercury compiler, it has often been the case that sanity checks of this
nature which we added only to satisfy the mode checker have later
failed for some obscure test case.  Adding the sanity checks ensures
that the bug is caught (rather than the program just producing bogus
results) and makes it much easier to debug.

So, to summarize:
	1.  Mode checking does work well in practice.
	2.  Mode checking has two benefits for program reliability:
	    - the immediate benefit is the static detection of a significant
	      class of errors;
	    - the other benefit is that it strongly encourages
	      programmers to include code to perform runtime checking
	      of complex (and hence error-prone) assertions that cannot
	      be verified by static analysis.

--
Fergus Henderson <fjh@cs.mu.oz.au>   |  "I have always known that the pursuit
WWW: <http://www.cs.mu.oz.au/~fjh>   |  of excellence is a lethal habit"
PGP: finger fjh@128.250.37.3         |     -- the last words of T. S. Garp.

Re: Finding out parameters which are not written

[Stuart Palin]

fjh@mundook.cs.mu.OZ.AU (Fergus Henderson) wrote:
>kilgallen@eisner.decus.org (Larry Kilgallen) writes:
>
>>Gerhard Radatz <gerhard.radatz@aut.alcatel.at> writes:
>>> Does anyone know about a tool which can detect such situations as the
>>> following:
>>> 
>>> 	procedure xxx (result: out INTEGER) is
>>>         begin
>>> 	     if <<condition>> then
>>> 	         result := 0;
>>>              end if;
>>>         end;
[snipping]

Sorry to quote this 3rd generation message (I did not see the first 
message and it appears to have expired).

Try looking at the SPARK tool from Praxis Critical Systems; they have a 
web page at http://www.praxis-cs.co.uk/spark/spark.htm

--
Stuart Palin
Consultant Engineer
Flight Systems Division (Rochester)
GEC Marconi Avionics Ltd