Skip to content
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.

Sign up for GitHub

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

Jump to bottom

Setting array field with size defined by message size #486

Closed
treiher opened this issue Nov 3, 2020 · 0 comments · Fixed by #493
Closed

Setting array field with size defined by message size #486

treiher opened this issue Nov 3, 2020 · 0 comments · Fixed by #493
Assignees
@treiher
Labels
generator Related to generator package (SPARK code generation)
Projects
RecordFlux 0.5

Comments

@treiher
Copy link
Collaborator

treiher commented Nov 3, 2020 •
edited
Loading

The current SPARK code does not allow setting an array field which length is defined by the message bounds. This is for example required in DHCP:

   type Options is array of Option;

   type Message is
      message
         [...]
         Options : Options
            with Size => Message'Last - Magic_Cookie'Last;
      end message;

Switch_To_Options expects Field_Size (Ctx, F_Options) > 0, which is not the case, as the size is just updated after setting the field.
@treiher treiher added the generator Related to generator package (SPARK code generation) label Nov 3, 2020
@treiher treiher added this to To do in RecordFlux 0.5 via automation Nov 3, 2020
@treiher treiher self-assigned this Nov 4, 2020
@treiher treiher moved this from To do to In progress in RecordFlux 0.5 Nov 4, 2020
@treiher treiher changed the title Setting array field with length defined by message bounds Setting array field with size defined by message size Nov 4, 2020
treiher added a commit that referenced this issue Nov 6, 2020
@treiher
Prevent changes of usable range of buffer
b2a77fd 
- Consider size restrictions of refined fields
- Allow setting array fields with size defined by message size

Ref. #356, #486
treiher added a commit that referenced this issue Nov 10, 2020
@treiher
Prevent changes of usable range of buffer
588e666 
- Consider size restrictions of refined fields
- Allow setting array fields with size defined by message size

Ref. #356, #486
@treiher treiher moved this from In progress to Done in RecordFlux 0.5 Nov 10, 2020
treiher added a commit that referenced this issue Nov 10, 2020
@treiher
Prevent changes to usable range of buffer
ce2bdb2 
- Consider size restrictions of refined fields
- Allow setting array fields with size defined by message size

Ref. #356, #486
@treiher treiher mentioned this issue Nov 10, 2020
Merged
treiher added a commit that referenced this issue Nov 11, 2020
@treiher
Prevent changes to usable range of buffer
1fbe776 
- Consider size restrictions of refined fields
- Allow setting array fields with size defined by message size

Ref. #356, #486
treiher added a commit that referenced this issue Nov 16, 2020
@treiher
Prevent changes to usable range of buffer
1b34aa7 
- Consider size restrictions of refined fields
- Allow setting array fields with size defined by message size

Ref. #356, #486
RecordFlux 0.5 automation moved this from Done to Merged Nov 17, 2020
treiher added a commit that referenced this issue Nov 17, 2020
@treiher
Prevent changes to usable range of buffer
2694ebd 
- Consider size restrictions of refined fields
- Allow setting array fields with size defined by message size

Ref. #356, #486
@treiher treiher mentioned this issue Aug 4, 2021
Closed
9 tasks
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@treiher treiher

Labels
generator Related to generator package (SPARK code generation)
Projects
No open projects
RecordFlux 0.5
  
Merged
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Issue 356, 486: Prevent changes to usable range of buffer AdaCore/RecordFlux
1 participant
@treiher