search

AdaCore / RecordFlux

Formal specification and generation of verifiable binary parsers, message generators and protocol state machines
Apache License 2.0
104 stars 6 forks source link

Mathematical expression for first and last of integer types does not support parentheses to ensure the order of operations #1290

Closed dalybrown closed 11 months ago

dalybrown commented 1 year ago

When defining the lower and upper bound of an integer, sometimes you want to use parentheses to establish the order of operations. When checking the specification, the following error occurs:

model: error: last of "XXX" contains variable

To work around this, I just do the math offline and sub in the values. However, those magic numbers without comments make it more difficult to reason about the specification. Also, often times interface documents for binary protocols define ranges as mathematical expressions and I find it nice to verbatim put those in my specifications.

It would be nice to support parentheses in mathematical expressions.

dalybrown commented 1 year ago

Actually ... I think I misunderstood the level RecordFlux works at and the use of the Opaque type. I was trying to define all my fields in RecordFlux! I have a better understanding now the gist of it, so I'm not sure if this is relevant or not anymore.

treiher commented 11 months ago

Apologies for the delayed response. The error message is not caused by the parentheses, but by the presence of what appears to be a variable. The bounds of an integer declaration must not contain any variable. The reason for this is that the integer bounds must be defined statically to be able to verify their correct use in messages or sessions. Also, there is no notion of variables or constant values at the package level in RecordFlux.