Issue 1048: Use signed integers for storage

[kanigsson]

Closes #1048

This commit proves with wavefront except for one check:

rflx-in_ipv4_tests.adb:186:13: medium: precondition might fail, cannot prove RFLX_Types.To_Length (Available_Space (Ctx, F_Payload)) >= Length
  186 |            Set_Payload (UDP_Datagram_Context, 18);
      |            ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

[kanigsson]

BTW, sorry for the missing cleanup (e.g. black, mypy etc) and random commit message. This is meant as a basis for discussion. I will cleanup if we want this.

[kanigsson]

In particular the name change of Terminating into Always_Return makes the patch fail for all older tools. This was an issue only for the old SPARK version, now updated.

[kanigsson]

Also fixes #974