Length restriction for nested message not considered

[treiher]

Currently, two different bounds are stored in a context:

• The byte range (Buffer_First, Buffer_Last) of the memory used for the message.
• The bit range (First, Last) defining the beginning and end of the message.

While the bit range is fixed when parsing a message, Last is changed during the creation of a message. Last can be increased as long as it does not exceed Buffer_Last (converted to bit). This is sufficient if only one message is considered. But as soon as the length is restricted by an underlying message, a hard limit for Last is needed which is possibly lower then Buffer_Last.

The following cases must be considered:

• Length of contained message is defined by containing message (e.g., IPv4, UDP)
• Length of contained message is undefined, but must be in certain bounds (e.g., Ethernet II, DHCP, ICMP)

Related issues:

• Length of contained message should only be settable to correct value
  • Should be checked by the update function (Generate update functions for refinements #72)
• Length should not be required for setting opaque field when message length is defined by containing message

Requires:

• Determining maximum length of field
  • Maximum length is defined by First and Last of context
• Negative testing
  • Will be added in Negative testing for generated SPARK code #359