Missing SPARK_Mode in generic Write procedures in tests

[jklmnn]

Multiple tests implement a generic Write_Data procedure to be used in generic set procedures for opaque fields:

procedure Write_Data (Buffer : out RFLX_Builtin_Types.Bytes) is                                                      
begin                                                                                                                
   Buffer := Data (Data'First .. Data'First + Buffer'Length - 1);                                                    
end Write_Data;

The assignment to Buffer cannot be proven since its length depends on the call and it has no precondition.
The quick fix would be to enable SPARK_Mode and check for the length (and e.g. use a default value to initialize if the check fails).
To actually prove the length the length of Buffer has to be a precondition to Set_* and Set_Bounded_* procedures.

[treiher]

We should not just apply the quick fix. The generated SPARK code should be adapted so that the Set_* and Set_Bounded_* procedures can be used in a secure and sensible way.

[jklmnn]

@treiher can you please take a look at the failing check? I can't reproduce the issue locally (also I don't understand why it would fail there).

[treiher]

I already observed that issue on the develop branch yesterday. I will look into it.

[treiher]

The issue seems to be gone (on develop as well as on this branch). After re-running the tests other issues are found which seem to be related to your changes:

rflx-ipv4-tests.adb:320:07: medium: precondition might fail, cannot prove Field_Length (Ctx, F_Payload) mod 8 = 0

[jklmnn]

Fixed by #295.