SPARK initialization by flow call graph

General
1

I have a procedure Wait_For_Transfer_Complete with an out parameter
Transfer_Complete : out Boolean;

If I add Transfer_Complete := False; to the beginning of the Wait_For_Transfer_Complete procedure then all is well.

If I instead add Transfer_Complete := False before the one return within Wait_For_Transfer_Complete then I get might not be initialized from SPARK flow analysis (not proving). If I try relaxed_initialization then it says can’t be applied to elementary type.

After the return there is a procedure Flag_Status whose case statement always overwrites Transfer_Complete from a volatile register. So it is always initialized.

I wondered if it was volatile registers causing an issue and so tried initializing it to False at the beginning of Flag_Status with no change. It hardly matters as I can just initialize a byte/boolean twice on the happy path but can anyone explain this?

2

I think I forgot that flow analysis doesn’t analyse bodies so I need some kind of annotation to say Flag_Status writes/initializes it’s out parameter.