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

Compilation fails when comparing field value with field size #479

Closed
treiher opened this issue Oct 27, 2020 · 0 comments · Fixed by #481
Closed

Compilation fails when comparing field value with field size #479

treiher opened this issue Oct 27, 2020 · 0 comments · Fixed by #481
Assignees
@treiher
Labels
bug generator Related to generator package (SPARK code generation)
Projects
RecordFlux 0.5

Comments

@treiher
Copy link
Collaborator

treiher commented Oct 27, 2020 

package Test is

   type T is mod 2**8;

   type M is
      message
         A : T;
         B : Opaque
            with Size => 8
            then null
               if A = B'Size;
      end message;

end Test;
Compile
   [Ada]          rflx-test.ads
   [Ada]          rflx-test-generic_m.adb
rflx-test-generic_m.adb:38:64: invalid operand types for operator "="
rflx-test-generic_m.adb:38:64: left operand has type "U64" defined at rflx-rflx_generic_types.ads:37, instance at rflx-test-generic_m.ads:5
rflx-test-generic_m.adb:38:64: right operand has type "Bit_Length" defined at rflx-rflx_generic_types.ads:13, instance at rflx-test-generic_m.ads:5
rflx-test-generic_m.adb:66:58: invalid operand types for operator "="
rflx-test-generic_m.adb:66:58: left operand has type "U64" defined at rflx-rflx_generic_types.ads:37, instance at rflx-test-generic_m.ads:5
rflx-test-generic_m.adb:66:58: right operand has type "Bit_Length" defined at rflx-rflx_generic_types.ads:13, instance at rflx-test-generic_m.ads:5
rflx-test-generic_m.adb:115:62: invalid operand types for operator "="
rflx-test-generic_m.adb:115:62: left operand has type "U64" defined at rflx-rflx_generic_types.ads:37, instance at rflx-test-generic_m.ads:5
rflx-test-generic_m.adb:115:62: right operand has type "Bit_Length" defined at rflx-rflx_generic_types.ads:13, instance at rflx-test-generic_m.ads:5
rflx-test-generic_m.adb:324:60: invalid operand types for operator "="
rflx-test-generic_m.adb:324:60: left operand has type "U64" defined at rflx-rflx_generic_types.ads:37, instance at rflx-test-generic_m.ads:5
rflx-test-generic_m.adb:324:60: right operand has type "Bit_Length" defined at rflx-rflx_generic_types.ads:13, instance at rflx-test-generic_m.ads:5
rflx-test-generic_m.adb:329:60: invalid operand types for operator "="
rflx-test-generic_m.adb:329:60: left operand has type "U64" defined at rflx-rflx_generic_types.ads:37, instance at rflx-test-generic_m.ads:5
rflx-test-generic_m.adb:329:60: right operand has type "Bit_Length" defined at rflx-rflx_generic_types.ads:13, instance at rflx-test-generic_m.ads:5
gprbuild: *** compilation phase failed
@treiher treiher added bug generator Related to generator package (SPARK code generation) labels Oct 27, 2020
@treiher treiher added this to To do in RecordFlux 0.5 via automation Oct 27, 2020
@treiher treiher moved this from To do to In progress in RecordFlux 0.5 Oct 28, 2020
@treiher treiher self-assigned this Oct 28, 2020
@treiher treiher moved this from In progress to Done in RecordFlux 0.5 Oct 28, 2020
treiher added a commit that referenced this issue Oct 28, 2020
@treiher
Fix type conflicts in generated code caused by size attribute
e3ad738 
Ref. #479
@treiher treiher mentioned this issue Oct 28, 2020
Merged
treiher added a commit that referenced this issue Oct 28, 2020
@treiher
Adapt proof configuration
9c5fa9a 
Ref. #479
RecordFlux 0.5 automation moved this from Done to Merged Oct 28, 2020
treiher added a commit that referenced this issue Oct 28, 2020
@treiher
Fix type conflicts in generated code caused by size attribute
ce3f11e 
Ref. #479
treiher added a commit that referenced this issue Oct 28, 2020
@treiher
Adapt proof configuration
b64ae9f 
Ref. #479
@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
bug 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 479, 480: Fix issues related to size attribute AdaCore/RecordFlux
1 participant
@treiher