-
Notifications
You must be signed in to change notification settings - Fork 6
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Checksum support in SPARK #276
Comments
The current design (#222) allows to specify checksums which depend fields following a checksum field. This is required for example for ICMP messages, where all fields must be set before the checksum function could be called. The generated SPARK code only allows to set fields in order of their occurrence. If any previously set field is changed, all subsequent fields would be invalidated. In case of ICMP this would mean that at first all fields of a ICMP would need to be set, before the checksum function can be used. If the result of the checksum function is used to set the checksum field, all subsequent field would be invalidated and must be set again. Solutions
|
The changes would be quite big. My optimistic estimate would be 5-8 person days just for the relevant parts of #107 with a high risk of finding unforeseen problems. |
Then we should go for option 2 and validate that the structure of the message really does not depend on the checksum field (which should normally be the case as the checksum is set to 0 and filled in later in most protocols). |
Cf. #240, #222
The text was updated successfully, but these errors were encountered: