Set but not used after call warnings

[treiher]

In certain instances, GNATprove shows warnings of the form warning: "X" is set by "Y" but not used after the call for calls into the generated SPARK code. These warnings have no effect on the soundness and can be suppressed using a pragma:

   pragma Warnings (Off, """X"" is set by ""Y"" but not used after the call");
   --  Y (X, Z);
   pragma Warnings (On, """X"" is set by ""Y"" but not used after the call");

The warnings cannot be suppressed in the generated code because of a limitation of GNATprove. This will probably change in Community 2022/Pro 22.0.