-
Notifications
You must be signed in to change notification settings - Fork 6
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Fix missing type conversion in generated code for appending to sequence
Ref. #965
- Loading branch information
Showing
32 changed files
with
6,104 additions
and
70 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,13 @@ | ||
| input: | ||
| Channel: | ||
| - 1 0 2 0 3 | ||
| output: | ||
| - Channel | ||
| sequence: | | ||
| Write Channel: 1 0 2 0 3 | ||
| State: Start | ||
| State: Process | ||
| Read Channel: 5 0 5 1 0 2 0 3 | ||
| State: Reply | ||
| # ISSUE: Componolit/RecordFlux#691 | ||
| # prove: |
65 changes: 65 additions & 0 deletions
65
tests/integration/session_sequence_append/generated/rflx-rflx_arithmetic.adb
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,65 @@ | ||
| pragma Style_Checks ("N3aAbcdefhiIklnOprStux"); | ||
|
|
||
| package body RFLX.RFLX_Arithmetic with | ||
| SPARK_Mode | ||
| is | ||
|
|
||
| function Shift_Left (Value : U64; Amount : Natural) return U64 with | ||
| Import, | ||
| Convention => Intrinsic, | ||
| Global => null; | ||
|
|
||
| function Shift_Right (Value : U64; Amount : Natural) return U64 with | ||
| Import, | ||
| Convention => Intrinsic, | ||
| Global => null; | ||
|
|
||
| function Shift_Add (V : U64; | ||
| Data : U64; | ||
| Amount : Natural; | ||
| Bits : Natural) return U64 | ||
| is | ||
| pragma Unreferenced (Bits); | ||
| begin | ||
| return Shift_Left (V, Amount) + Data; | ||
| end Shift_Add; | ||
|
|
||
| function Right_Shift (V : U64; Amount : Natural; Size : Natural) return U64 | ||
| is | ||
| pragma Unreferenced (Size); | ||
| begin | ||
| return Shift_Right (V, Amount); | ||
| end Right_Shift; | ||
|
|
||
| function Left_Shift (V : U64; Amount : Natural; Size : Natural) return U64 | ||
| is | ||
| pragma Unreferenced (Size); | ||
| Result : constant U64 := Shift_Left (V, Amount); | ||
| begin | ||
| return Result; | ||
| end Left_Shift; | ||
|
|
||
| function Mask_Lower (V : U64; Mask, Bits : Natural) return U64 | ||
| is | ||
| Result : constant U64 := Shift_Left (Shift_Right (V, Mask), Mask); | ||
| begin | ||
| pragma Assert | ||
| (if Bits < U64'Size then Result <= 2 ** Bits - 2 ** Mask | ||
| elsif Mask < U64'Size then Result <= U64'Last - 2 ** Mask + 1); | ||
| return Result; | ||
| end Mask_Lower; | ||
|
|
||
| function Mask_Upper (V : U64; Mask : Natural) return U64 | ||
| is | ||
| begin | ||
| return V and (2 ** Mask - 1); | ||
| end Mask_Upper; | ||
|
|
||
| function Add (A : U64; B : U64; Total_Bits, Lower_Bits : Natural) return U64 | ||
| is | ||
| pragma Unreferenced (Total_Bits, Lower_Bits); | ||
| begin | ||
| return A + B; | ||
| end Add; | ||
|
|
||
| end RFLX.RFLX_Arithmetic; |
85 changes: 85 additions & 0 deletions
85
tests/integration/session_sequence_append/generated/rflx-rflx_arithmetic.ads
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,85 @@ | ||
| pragma Style_Checks ("N3aAbcdefhiIklnOprStux"); | ||
|
|
||
| package RFLX.RFLX_Arithmetic with | ||
| SPARK_Mode | ||
| is | ||
|
|
||
| type U64 is mod 2**64 with | ||
| Annotate => (GNATprove, No_Wrap_Around); | ||
|
|
||
| -- Express that V contains at most Bits non-zero bits, in the least | ||
| -- significant part (the rest is zero). | ||
| pragma Warnings (Off, "postcondition does not mention function result"); | ||
| function Fits_Into (V : U64; Bits : Natural) return Boolean | ||
| is (if Bits < U64'Size then V < 2 ** Bits) | ||
| with Post => True; | ||
|
|
||
| -- Express that V contains (U64'Size - Bits) leading zero bits, then (Bits - | ||
| -- Lower) bits of data, then Lower bits of zeros. | ||
| -- |- (U64'Size - bits) -|- (Bits-Lower) -|- Lower -| | ||
| -- |000000000000000000000|xxxxxxxxxxxxxxxx|000000000| | ||
| function Fits_Into_Upper (V : U64; Bits, Lower : Natural) return Boolean | ||
| is (if Bits < U64'Size then V <= 2 ** Bits - 2 ** Lower | ||
| elsif Lower > 0 and then Lower < U64'Size then V <= U64'Last - 2 ** Lower + 1) | ||
| with Pre => Bits <= U64'Size and then Lower <= Bits, | ||
| Post => True; | ||
| pragma Warnings (On, "postcondition does not mention function result"); | ||
|
|
||
| -- V is assumed to contain Bits bits of data. Add the Amount bits contained | ||
| -- in Data by shifting V to the left and adding Data. The result contains | ||
| -- (Bits + Amount) bits of data. | ||
| function Shift_Add (V : U64; | ||
| Data : U64; | ||
| Amount : Natural; | ||
| Bits : Natural) return U64 | ||
| with Pre => | ||
| Bits < U64'Size | ||
| and then Amount < U64'Size | ||
| and then Fits_Into (V, Bits) | ||
| and then U64'Size - Amount >= Bits | ||
| and then Fits_Into (Data, Amount), | ||
| Post => Fits_Into (Shift_Add'Result, Bits + Amount); | ||
|
|
||
| -- Wrapper of Shift_Right that expresses the operation in terms of | ||
| -- Fits_Into. | ||
| function Right_Shift (V : U64; Amount : Natural; Size : Natural) return U64 with | ||
| Pre => | ||
| Size <= U64'Size | ||
| and then Fits_Into (V, Size) | ||
| and then Amount <= Size | ||
| and then Size - Amount < U64'Size, | ||
| Post => Fits_Into (Right_Shift'Result, Size - Amount); | ||
|
|
||
| -- Wrapper of Shift_Left that expresses the operation in terms of | ||
| -- Fits_Into/Fits_Into_Upper. | ||
| function Left_Shift (V : U64; Amount : Natural; Size : Natural) return U64 with | ||
| Pre => | ||
| Size < U64'Size | ||
| and then Amount < U64'Size | ||
| and then Fits_Into (V, Size) | ||
| and then Size + Amount < U64'Size, | ||
| Post => Fits_Into_Upper (Left_Shift'Result, Size + Amount, Amount); | ||
|
|
||
| -- V is assumed to have Bits bits of data. Set the lower bits of V to zero. | ||
| function Mask_Lower (V : U64; Mask, Bits : Natural) return U64 | ||
| with Pre => Bits <= U64'Size and then Fits_Into (V, Bits) and then Mask <= Bits and then Mask >= 1, | ||
| Post => Fits_Into_Upper (Mask_Lower'Result, Bits, Mask); | ||
|
|
||
| -- Set the upper bits of V to zero. | ||
| function Mask_Upper (V : U64; Mask : Natural) return U64 | ||
| with Pre => Mask < U64'Size, | ||
| Post => Fits_Into (Mask_Upper'Result, Mask); | ||
|
|
||
| -- Add A and B in the special case where A only uses the upper bits and B | ||
| -- only the lower bits. | ||
| function Add (A : U64; B : U64; Total_Bits, Lower_Bits : Natural) return U64 | ||
| with Pre => | ||
| Total_Bits <= U64'Size | ||
| and then Lower_Bits <= Total_Bits | ||
| and then (if Total_Bits = U64'Size then Lower_Bits /= U64'Size) | ||
| and then Fits_Into_Upper (A, Total_Bits, Lower_Bits) | ||
| and then Fits_Into (B, Lower_Bits), | ||
| Post => Add'Result = A + B and Fits_Into (Add'Result, Total_Bits), | ||
| Global => null; | ||
|
|
||
| end RFLX.RFLX_Arithmetic; |
Oops, something went wrong.