Question about Spark_IO

Question about Spark_IO

[Peter C. Chapin]

I'm doing something like this to close a file using Spark_IO

    Spark_IO.Close(Input, Input_Status);
    if Input_Status /= Spark_IO.Ok then ...

The Examiner says there is a flow error with the first line because the 
assignment to Input is "ineffective." This is because it is an 'in out' 
parameter and nothing is being done with the returned value.

My understanding is that Close puts the file handle it has been given 
into an invalid state so that any further use of it will result in an 
error. Thus it is not correct to do anything with that value after Close 
returns.

Is this a case where it is appropriate to suppress the flow error with 
an '--# accept flow_message...' annotation or is there some better way 
to handle this situation?

Thanks!

Peter

Re: Question about Spark_IO

[Phil Thornley]

In article <Cf2dnRYegbnckR_S4p2dnAA@giganews.com>, PChapin@vtc.vsc.edu 
says...
> 
> I'm doing something like this to close a file using Spark_IO
> 
>     Spark_IO.Close(Input, Input_Status);
>     if Input_Status /= Spark_IO.Ok then ...
> 
> The Examiner says there is a flow error with the first line because the 
> assignment to Input is "ineffective." This is because it is an 'in out' 
> parameter and nothing is being done with the returned value.
> 
> My understanding is that Close puts the file handle it has been given 
> into an invalid state so that any further use of it will result in an 
> error. Thus it is not correct to do anything with that value after Close 
> returns.
> 
> Is this a case where it is appropriate to suppress the flow error with 
> an '--# accept flow_message...' annotation or is there some better way 
> to handle this situation?

Yes, that's exactly what I would do here.  The File parameter can't be 
changed to 'in' mode - to remove the flow error - as there would be a 
compilation error in the body of Close.

Note that the flow relation on Close doesn't represent the actual flow 
in the procedure and is clearly the closest model that makes any sense.
(It says that the File parameter is set to a constant value - the 
invalid state perhaps - but in the code this setting is conditional on 
the input value of File, so there is actually a self-dependency.)

Cheers,

Phil

Re: Question about Spark_IO

[Yannick Duchêne (Hibou57)]

Le Mon, 09 Apr 2012 00:07:48 +0200, Peter C. Chapin <PChapin@vtc.vsc.edu>  
a écrit:

> I'm doing something like this to close a file using Spark_IO
>
>     Spark_IO.Close(Input, Input_Status);
>     if Input_Status /= Spark_IO.Ok then ...
>
> The Examiner says there is a flow error with the first line because the  
> assignment to Input is "ineffective." This is because it is an 'in out'  
> parameter and nothing is being done with the returned value.
May be SPARK should have a notion of final state. This could be explicit,  
which would be cleaner than locally disabling control flow.

-- 
“Syntactic sugar causes cancer of the semi-colons.” [1]
“Structured Programming supports the law of the excluded muddle.” [1]
[1]: Epigrams on Programming — Alan J. — P. Yale University