You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Consecutive assignments to fields of the same message should be realizable with fewer checks:
Check Available_Space once
Check Valid_Next once
The assignments could be collected into a new object ("delta message aggregate"). It has to be checked that the set fields are a valid sub-path of the message. For the calculation of the required size, Message.size must consider message sub-paths.
Note: Field_Condition has to be checked on certain fields in case a condition could be violated. Field_Condition is not yet checked and adding of such checks is not part of this ticket, but will be done in #1121.
The text was updated successfully, but these errors were encountered:
treiher
added
generator
Related to generator package (SPARK code generation)
model
Related to model package (e.g., model verification)
labels
Jul 27, 2022
Consecutive assignments to fields of the same message should be realizable with fewer checks:
Available_Space
onceValid_Next
onceThe assignments could be collected into a new object ("delta message aggregate"). It has to be checked that the set fields are a valid sub-path of the message. For the calculation of the required size,
Message.size
must consider message sub-paths.Note:
Field_Condition
has to be checked on certain fields in case a condition could be violated.Field_Condition
is not yet checked and adding of such checks is not part of this ticket, but will be done in #1121.The text was updated successfully, but these errors were encountered: