diff --git a/Makefile b/Makefile index 4ca6184a5..7d77ea6e7 100644 --- a/Makefile +++ b/Makefile @@ -332,7 +332,7 @@ test_property: $(RFLX) $(PYTEST) tests/property test_tools: $(RFLX) - $(PYTEST) --cov=tools --cov-branch --cov-fail-under=43.6 --cov-report=term-missing:skip-covered tests/tools + $(PYTEST) --cov=tools --cov-branch --cov-fail-under=60.0 --cov-report=term-missing:skip-covered tests/tools test_ide: $(RFLX) $(PYTEST) tests/ide diff --git a/tests/compilation/generator_test.py b/tests/compilation/generator_test.py new file mode 100644 index 000000000..e708a975f --- /dev/null +++ b/tests/compilation/generator_test.py @@ -0,0 +1,11 @@ +from pathlib import Path + +import pytest + +from tests.unit.generator.generator_test import GENERATOR_TEST_CASES, TC +from tests.utils import assert_compilable_code + + +@pytest.mark.parametrize("tc", GENERATOR_TEST_CASES) +def test_compilability(tc: TC, tmp_path: Path) -> None: + assert_compilable_code(tc.model(), tc.integration(), tmp_path) diff --git a/tests/data/generator/generated/boolean_variable/rflx-p-message.adb b/tests/data/generator/generated/boolean_variable/rflx-p-message.adb new file mode 100644 index 000000000..90b0b121b --- /dev/null +++ b/tests/data/generator/generated/boolean_variable/rflx-p-message.adb @@ -0,0 +1,291 @@ +------------------------------------------------------------------------------ +-- -- +-- Generated by RecordFlux -- +-- -- +-- Copyright (C) AdaCore GmbH -- +-- -- +-- SPDX-License-Identifier: Apache-2.0 -- +-- -- +------------------------------------------------------------------------------ + +pragma Ada_2012; +pragma Style_Checks ("N3aAbCdefhiIklnOprStux"); +pragma Warnings (Off, "redundant conversion"); +with RFLX.RFLX_Types.Operations; + +package body RFLX.P.Message with + SPARK_Mode +is + + pragma Unevaluated_Use_Of_Old (Allow); + + procedure Initialize (Ctx : out Context; Buffer : in out RFLX_Types.Bytes_Ptr; Written_Last : RFLX_Types.Bit_Length := 0) is + begin + Initialize (Ctx, Buffer, RFLX_Types.To_First_Bit_Index (Buffer'First), RFLX_Types.To_Last_Bit_Index (Buffer'Last), Written_Last); + end Initialize; + + procedure Initialize (Ctx : out Context; Buffer : in out RFLX_Types.Bytes_Ptr; First : RFLX_Types.Bit_Index; Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length := 0) is + Buffer_First : constant RFLX_Types.Index := Buffer'First; + Buffer_Last : constant RFLX_Types.Index := Buffer'Last; + begin + Ctx := (Buffer_First, Buffer_Last, First, Last, First - 1, (if Written_Last = 0 then First - 1 else Written_Last), Buffer, (F_A => (State => S_Invalid, others => <>), others => <>)); + Buffer := null; + end Initialize; + + procedure Reset (Ctx : in out Context) is + begin + Reset (Ctx, RFLX_Types.To_First_Bit_Index (Ctx.Buffer'First), RFLX_Types.To_Last_Bit_Index (Ctx.Buffer'Last)); + end Reset; + + procedure Reset (Ctx : in out Context; First : RFLX_Types.Bit_Index; Last : RFLX_Types.Bit_Length) is + begin + Ctx := (Ctx.Buffer_First, Ctx.Buffer_Last, First, Last, First - 1, First - 1, Ctx.Buffer, (F_A => (State => S_Invalid, others => <>), others => <>)); + end Reset; + + procedure Take_Buffer (Ctx : in out Context; Buffer : out RFLX_Types.Bytes_Ptr) is + begin + Buffer := Ctx.Buffer; + Ctx.Buffer := null; + end Take_Buffer; + + procedure Copy (Ctx : Context; Buffer : out RFLX_Types.Bytes) is + begin + if Buffer'Length > 0 then + Buffer := Ctx.Buffer.all (RFLX_Types.To_Index (Ctx.First) .. RFLX_Types.To_Index (Ctx.Verified_Last)); + else + Buffer := Ctx.Buffer.all (1 .. 0); + end if; + end Copy; + + procedure Generic_Read (Ctx : Context) is + begin + Read (Ctx.Buffer.all (RFLX_Types.To_Index (Ctx.First) .. RFLX_Types.To_Index (Ctx.Verified_Last))); + end Generic_Read; + + procedure Generic_Write (Ctx : in out Context; Offset : RFLX_Types.Length := 0) is + Length : RFLX_Types.Length; + begin + Reset (Ctx, RFLX_Types.To_First_Bit_Index (Ctx.Buffer_First), RFLX_Types.To_Last_Bit_Index (Ctx.Buffer_Last)); + Write (Ctx.Buffer.all (Ctx.Buffer'First + RFLX_Types.Index (Offset + 1) - 1 .. Ctx.Buffer'Last), Length, Ctx.Buffer'Length, Offset); + pragma Assert (Length <= Ctx.Buffer.all'Length, "Length <= Buffer'Length is not ensured by postcondition of ""Write"""); + Ctx.Written_Last := RFLX_Types.Bit_Index'Max (Ctx.Written_Last, RFLX_Types.To_Last_Bit_Index (RFLX_Types.Length (Ctx.Buffer_First) + Offset + Length - 1)); + end Generic_Write; + + procedure Data (Ctx : Context; Data : out RFLX_Types.Bytes) is + begin + Data := Ctx.Buffer.all (RFLX_Types.To_Index (Ctx.First) .. RFLX_Types.To_Index (Ctx.Verified_Last)); + end Data; + + function Invalid_Successor (Ctx : Context; Fld : Field) return Boolean is + ((case Fld is + when F_A => + Invalid (Ctx.Cursors (F_B)), + when F_B => + True)); + + function Sufficient_Buffer_Length (Ctx : Context; Fld : Field) return Boolean is + (Ctx.Buffer /= null + and Field_First (Ctx, Fld) + Field_Size (Ctx, Fld) < RFLX_Types.Bit_Length'Last + and Ctx.First <= Field_First (Ctx, Fld) + and Field_First (Ctx, Fld) + Field_Size (Ctx, Fld) - 1 <= Ctx.Written_Last) + with + Pre => + RFLX.P.Message.Has_Buffer (Ctx) + and RFLX.P.Message.Valid_Next (Ctx, Fld); + + procedure Reset_Dependent_Fields (Ctx : in out Context; Fld : Field) with + Pre => + RFLX.P.Message.Valid_Next (Ctx, Fld), + Post => + Valid_Next (Ctx, Fld) + and Ctx.Buffer_First = Ctx.Buffer_First'Old + and Ctx.Buffer_Last = Ctx.Buffer_Last'Old + and Ctx.First = Ctx.First'Old + and Ctx.Last = Ctx.Last'Old + and Has_Buffer (Ctx) = Has_Buffer (Ctx)'Old + and Field_First (Ctx, Fld) = Field_First (Ctx, Fld)'Old + and Field_Size (Ctx, Fld) = Field_Size (Ctx, Fld)'Old + and (for all F in Field => + (if F < Fld then Ctx.Cursors (F) = Ctx.Cursors'Old (F) else Invalid (Ctx, F))) + is + begin + for Fld_Loop in reverse Fld .. Field'Last loop + pragma Loop_Invariant (Field_First (Ctx, Fld) = Field_First (Ctx, Fld)'Loop_Entry + and Field_Size (Ctx, Fld) = Field_Size (Ctx, Fld)'Loop_Entry); + pragma Loop_Invariant ((for all F in Field => + (if F <= Fld_Loop then Ctx.Cursors (F) = Ctx.Cursors'Loop_Entry (F) else Invalid (Ctx, F)))); + Ctx.Cursors (Fld_Loop) := (State => S_Invalid, others => <>); + end loop; + end Reset_Dependent_Fields; + + function Get (Ctx : Context; Fld : Field) return RFLX_Types.Base_Integer with + Pre => + RFLX.P.Message.Has_Buffer (Ctx) + and then RFLX.P.Message.Valid_Next (Ctx, Fld) + and then RFLX.P.Message.Sufficient_Buffer_Length (Ctx, Fld) + is + First : constant RFLX_Types.Bit_Index := Field_First (Ctx, Fld); + Last : constant RFLX_Types.Bit_Index := Field_Last (Ctx, Fld); + Buffer_First : constant RFLX_Types.Index := RFLX_Types.To_Index (First); + Buffer_Last : constant RFLX_Types.Index := RFLX_Types.To_Index (Last); + Offset : constant RFLX_Types.Offset := RFLX_Types.Offset ((RFLX_Types.Byte'Size - Last mod RFLX_Types.Byte'Size) mod RFLX_Types.Byte'Size); + Size : constant Positive := (case Fld is + when F_A => + 1, + when F_B => + 7); + Byte_Order : constant RFLX_Types.Byte_Order := RFLX_Types.High_Order_First; + begin + return RFLX_Types.Operations.Extract (Ctx.Buffer.all, Buffer_First, Buffer_Last, Offset, Size, Byte_Order); + end Get; + + procedure Verify (Ctx : in out Context; Fld : Field) is + Value : RFLX_Types.Base_Integer; + begin + if + Invalid (Ctx.Cursors (Fld)) + and then Valid_Next (Ctx, Fld) + then + if Sufficient_Buffer_Length (Ctx, Fld) then + Value := Get (Ctx, Fld); + if + Valid_Value (Fld, Value) + and then Field_Condition (Ctx, Fld, Value) + then + pragma Assert ((if Fld = F_B then Field_Last (Ctx, Fld) mod RFLX_Types.Byte'Size = 0)); + pragma Assert ((((Field_Last (Ctx, Fld) + RFLX_Types.Byte'Size - 1) / RFLX_Types.Byte'Size) * RFLX_Types.Byte'Size) mod RFLX_Types.Byte'Size = 0); + Ctx.Verified_Last := ((Field_Last (Ctx, Fld) + RFLX_Types.Byte'Size - 1) / RFLX_Types.Byte'Size) * RFLX_Types.Byte'Size; + pragma Assert (Field_Last (Ctx, Fld) <= Ctx.Verified_Last); + Ctx.Cursors (Fld) := (State => S_Valid, First => Field_First (Ctx, Fld), Last => Field_Last (Ctx, Fld), Value => Value); + else + Ctx.Cursors (Fld) := (others => <>); + end if; + else + Ctx.Cursors (Fld) := (State => S_Incomplete, others => <>); + end if; + end if; + end Verify; + + procedure Verify_Message (Ctx : in out Context) is + begin + for F in Field loop + pragma Loop_Invariant (Has_Buffer (Ctx) + and Ctx.Buffer_First = Ctx.Buffer_First'Loop_Entry + and Ctx.Buffer_Last = Ctx.Buffer_Last'Loop_Entry + and Ctx.First = Ctx.First'Loop_Entry + and Ctx.Last = Ctx.Last'Loop_Entry); + Verify (Ctx, F); + end loop; + end Verify_Message; + + procedure Set (Ctx : in out Context; Fld : Field; Val : RFLX_Types.Base_Integer; Size : RFLX_Types.Bit_Length; State_Valid : Boolean; Buffer_First : out RFLX_Types.Index; Buffer_Last : out RFLX_Types.Index; Offset : out RFLX_Types.Offset) with + Pre => + RFLX.P.Message.Has_Buffer (Ctx) + and then RFLX.P.Message.Valid_Next (Ctx, Fld) + and then RFLX.P.Message.Valid_Value (Fld, Val) + and then RFLX.P.Message.Valid_Size (Ctx, Fld, Size) + and then Size <= RFLX.P.Message.Available_Space (Ctx, Fld) + and then State_Valid, + Post => + Valid_Next (Ctx, Fld) + and then Invalid_Successor (Ctx, Fld) + and then Buffer_First = RFLX_Types.To_Index (Field_First (Ctx, Fld)) + and then Buffer_Last = RFLX_Types.To_Index (Field_First (Ctx, Fld) + Size - 1) + and then Offset = RFLX_Types.Offset ((RFLX_Types.Byte'Size - (Field_First (Ctx, Fld) + Size - 1) mod RFLX_Types.Byte'Size) mod RFLX_Types.Byte'Size) + and then Ctx.Buffer_First = Ctx.Buffer_First'Old + and then Ctx.Buffer_Last = Ctx.Buffer_Last'Old + and then Ctx.First = Ctx.First'Old + and then Ctx.Last = Ctx.Last'Old + and then Ctx.Buffer_First = Ctx.Buffer_First'Old + and then Ctx.Buffer_Last = Ctx.Buffer_Last'Old + and then Ctx.First = Ctx.First'Old + and then Ctx.Last = Ctx.Last'Old + and then Has_Buffer (Ctx) = Has_Buffer (Ctx)'Old + and then Field_First (Ctx, Fld) = Field_First (Ctx, Fld)'Old + and then Sufficient_Space (Ctx, Fld) + and then (if State_Valid and Size > 0 then Valid (Ctx, Fld) else Well_Formed (Ctx, Fld)) + and then (Ctx.Cursors (Fld).Value = Val + and then (if Fld in F_B and then Well_Formed_Message (Ctx) then Message_Last (Ctx) = Field_Last (Ctx, Fld))) + and then (for all F in Field => + (if F < Fld then Ctx.Cursors (F) = Ctx.Cursors'Old (F))) + is + First : RFLX_Types.Bit_Index; + Last : RFLX_Types.Bit_Length; + begin + Reset_Dependent_Fields (Ctx, Fld); + First := Field_First (Ctx, Fld); + Last := Field_First (Ctx, Fld) + Size - 1; + Offset := RFLX_Types.Offset ((RFLX_Types.Byte'Size - Last mod RFLX_Types.Byte'Size) mod RFLX_Types.Byte'Size); + Buffer_First := RFLX_Types.To_Index (First); + Buffer_Last := RFLX_Types.To_Index (Last); + pragma Assert ((((Last + RFLX_Types.Byte'Size - 1) / RFLX_Types.Byte'Size) * RFLX_Types.Byte'Size) mod RFLX_Types.Byte'Size = 0); + pragma Warnings (Off, "attribute Update is an obsolescent feature"); + Ctx := Ctx'Update (Verified_Last => ((Last + RFLX_Types.Byte'Size - 1) / RFLX_Types.Byte'Size) * RFLX_Types.Byte'Size, Written_Last => ((Last + RFLX_Types.Byte'Size - 1) / RFLX_Types.Byte'Size) * RFLX_Types.Byte'Size); + pragma Warnings (On, "attribute Update is an obsolescent feature"); + if State_Valid then + Ctx.Cursors (Fld) := (State => S_Valid, First => First, Last => Last, Value => Val); + else + Ctx.Cursors (Fld) := (State => S_Well_Formed, First => First, Last => Last, Value => Val); + end if; + pragma Assert (Last = (Field_First (Ctx, Fld) + Size) - 1); + end Set; + + procedure Set_Scalar (Ctx : in out Context; Fld : Field; Val : RFLX_Types.Base_Integer) with + Pre => + not Ctx'Constrained + and then RFLX.P.Message.Has_Buffer (Ctx) + and then RFLX.P.Message.Valid_Next (Ctx, Fld) + and then Fld in F_A | F_B + and then RFLX.P.Message.Valid_Value (Fld, Val) + and then RFLX.P.Message.Valid_Size (Ctx, Fld, RFLX.P.Message.Field_Size (Ctx, Fld)) + and then RFLX.P.Message.Available_Space (Ctx, Fld) >= RFLX.P.Message.Field_Size (Ctx, Fld) + and then RFLX.P.Message.Field_Size (Ctx, Fld) in 1 .. RFLX_Types.Base_Integer'Size + and then RFLX_Types.Fits_Into (Val, Natural (RFLX.P.Message.Field_Size (Ctx, Fld))), + Post => + Has_Buffer (Ctx) + and Valid (Ctx, Fld) + and Invalid_Successor (Ctx, Fld) + and (Ctx.Cursors (Fld).Value = Val + and then (if Fld in F_B and then Well_Formed_Message (Ctx) then Message_Last (Ctx) = Field_Last (Ctx, Fld))) + and (for all F in Field => + (if F < Fld then Ctx.Cursors (F) = Ctx.Cursors'Old (F))) + and Ctx.Buffer_First = Ctx.Buffer_First'Old + and Ctx.Buffer_Last = Ctx.Buffer_Last'Old + and Ctx.First = Ctx.First'Old + and Ctx.Last = Ctx.Last'Old + and Has_Buffer (Ctx) = Has_Buffer (Ctx)'Old + and Field_First (Ctx, Fld) = Field_First (Ctx, Fld)'Old + is + Buffer_First, Buffer_Last : RFLX_Types.Index; + Offset : RFLX_Types.Offset; + Size : constant RFLX_Types.Bit_Length := Field_Size (Ctx, Fld); + begin + Set (Ctx, Fld, Val, Size, True, Buffer_First, Buffer_Last, Offset); + RFLX_Types.Lemma_Size (Val, Positive (Size)); + RFLX_Types.Operations.Insert (Val, Ctx.Buffer.all, Buffer_First, Buffer_Last, Offset, Positive (Size), RFLX_Types.High_Order_First); + end Set_Scalar; + + procedure Set_A (Ctx : in out Context; Val : Boolean) is + begin + Set_Scalar (Ctx, F_A, To_Base_Integer (Val)); + end Set_A; + + procedure Set_B (Ctx : in out Context; Val : RFLX.P.T) is + begin + Set_Scalar (Ctx, F_B, RFLX.P.To_Base_Integer (Val)); + end Set_B; + + procedure To_Structure (Ctx : Context; Struct : out Structure) is + begin + Struct.A := Get_A (Ctx); + Struct.B := Get_B (Ctx); + end To_Structure; + + procedure To_Context (Struct : Structure; Ctx : in out Context) is + begin + Reset (Ctx); + Set_A (Ctx, Struct.A); + Set_B (Ctx, Struct.B); + end To_Context; + +end RFLX.P.Message; diff --git a/tests/data/generator/generated/boolean_variable/rflx-p-message.ads b/tests/data/generator/generated/boolean_variable/rflx-p-message.ads new file mode 100644 index 000000000..aacf14f3c --- /dev/null +++ b/tests/data/generator/generated/boolean_variable/rflx-p-message.ads @@ -0,0 +1,794 @@ +------------------------------------------------------------------------------ +-- -- +-- Generated by RecordFlux -- +-- -- +-- Copyright (C) AdaCore GmbH -- +-- -- +-- SPDX-License-Identifier: Apache-2.0 -- +-- -- +------------------------------------------------------------------------------ + +pragma Ada_2012; +pragma Style_Checks ("N3aAbCdefhiIklnOprStux"); +pragma Warnings (Off, "redundant conversion"); +with RFLX.RFLX_Types; +with RFLX.RFLX_Builtin_Types; +with RFLX.RFLX_Builtin_Types.Conversions; +use RFLX.RFLX_Builtin_Types.Conversions; + +package RFLX.P.Message with + SPARK_Mode, + Always_Terminates +is + + pragma Warnings (Off, "use clause for type ""Base_Integer"" * has no effect"); + + pragma Warnings (Off, "use clause for type ""Bytes"" * has no effect"); + + pragma Warnings (Off, """BASE_INTEGER"" is already use-visible through previous use_type_clause"); + + pragma Warnings (Off, """LENGTH"" is already use-visible through previous use_type_clause"); + + use type RFLX_Types.Bytes_Ptr; + + use type RFLX_Types.Length; + + use type RFLX_Types.Index; + + use type RFLX_Types.Bit_Index; + + use type RFLX_Types.Base_Integer; + + use type RFLX_Types.Offset; + + pragma Warnings (On, """LENGTH"" is already use-visible through previous use_type_clause"); + + pragma Warnings (On, """BASE_INTEGER"" is already use-visible through previous use_type_clause"); + + pragma Warnings (On, "use clause for type ""Base_Integer"" * has no effect"); + + pragma Warnings (On, "use clause for type ""Bytes"" * has no effect"); + + pragma Unevaluated_Use_Of_Old (Allow); + + type Virtual_Field is (F_Initial, F_A, F_B, F_Final); + + subtype Field is Virtual_Field range F_A .. F_B; + + type Field_Cursor is private; + + type Field_Cursors is private; + + type Context (Buffer_First, Buffer_Last : RFLX_Types.Index := RFLX_Types.Index'First; First : RFLX_Types.Bit_Index := RFLX_Types.Bit_Index'First; Last : RFLX_Types.Bit_Length := RFLX_Types.Bit_Length'First) is private with + Default_Initial_Condition => + RFLX_Types.To_Index (First) >= Buffer_First + and RFLX_Types.To_Index (Last) <= Buffer_Last + and Buffer_Last < RFLX_Types.Index'Last + and First <= Last + 1 + and Last < RFLX_Types.Bit_Index'Last + and First rem RFLX_Types.Byte'Size = 1 + and Last rem RFLX_Types.Byte'Size = 0; + + procedure Initialize (Ctx : out Context; Buffer : in out RFLX_Types.Bytes_Ptr; Written_Last : RFLX_Types.Bit_Length := 0) with + Pre => + not Ctx'Constrained + and then Buffer /= null + and then Buffer'Length > 0 + and then Buffer'Last < RFLX_Types.Index'Last + and then (Written_Last = 0 + or (Written_Last >= RFLX_Types.To_First_Bit_Index (Buffer'First) - 1 + and Written_Last <= RFLX_Types.To_Last_Bit_Index (Buffer'Last))) + and then Written_Last mod RFLX_Types.Byte'Size = 0, + Post => + Has_Buffer (Ctx) + and Buffer = null + and Ctx.Buffer_First = Buffer'First'Old + and Ctx.Buffer_Last = Buffer'Last'Old + and Ctx.First = RFLX_Types.To_First_Bit_Index (Ctx.Buffer_First) + and Ctx.Last = RFLX_Types.To_Last_Bit_Index (Ctx.Buffer_Last) + and Initialized (Ctx), + Depends => + (Ctx => (Buffer, Written_Last), Buffer => null); + + procedure Initialize (Ctx : out Context; Buffer : in out RFLX_Types.Bytes_Ptr; First : RFLX_Types.Bit_Index; Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length := 0) with + Pre => + not Ctx'Constrained + and then Buffer /= null + and then Buffer'Length > 0 + and then Buffer'Last < RFLX_Types.Index'Last + and then RFLX_Types.To_Index (First) >= Buffer'First + and then RFLX_Types.To_Index (Last) <= Buffer'Last + and then First <= Last + 1 + and then Last < RFLX_Types.Bit_Index'Last + and then First rem RFLX_Types.Byte'Size = 1 + and then Last rem RFLX_Types.Byte'Size = 0 + and then (Written_Last = 0 + or (Written_Last >= First - 1 + and Written_Last <= Last)) + and then Written_Last rem RFLX_Types.Byte'Size = 0, + Post => + Buffer = null + and Has_Buffer (Ctx) + and Ctx.Buffer_First = Buffer'First'Old + and Ctx.Buffer_Last = Buffer'Last'Old + and Ctx.First = First + and Ctx.Last = Last + and Initialized (Ctx), + Depends => + (Ctx => (Buffer, First, Last, Written_Last), Buffer => null); + + pragma Warnings (Off, "postcondition does not mention function result"); + + function Initialized (Ctx : Context) return Boolean with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); + + procedure Reset (Ctx : in out Context) with + Pre => + not Ctx'Constrained + and RFLX.P.Message.Has_Buffer (Ctx), + Post => + Has_Buffer (Ctx) + and Ctx.Buffer_First = Ctx.Buffer_First'Old + and Ctx.Buffer_Last = Ctx.Buffer_Last'Old + and Ctx.First = RFLX_Types.To_First_Bit_Index (Ctx.Buffer_First) + and Ctx.Last = RFLX_Types.To_Last_Bit_Index (Ctx.Buffer_Last) + and Initialized (Ctx); + + procedure Reset (Ctx : in out Context; First : RFLX_Types.Bit_Index; Last : RFLX_Types.Bit_Length) with + Pre => + not Ctx'Constrained + and RFLX.P.Message.Has_Buffer (Ctx) + and RFLX_Types.To_Index (First) >= Ctx.Buffer_First + and RFLX_Types.To_Index (Last) <= Ctx.Buffer_Last + and First <= Last + 1 + and Last < RFLX_Types.Bit_Length'Last + and First rem RFLX_Types.Byte'Size = 1 + and Last rem RFLX_Types.Byte'Size = 0, + Post => + Has_Buffer (Ctx) + and Ctx.Buffer_First = Ctx.Buffer_First'Old + and Ctx.Buffer_Last = Ctx.Buffer_Last'Old + and Ctx.First = First + and Ctx.Last = Last + and Initialized (Ctx); + + procedure Take_Buffer (Ctx : in out Context; Buffer : out RFLX_Types.Bytes_Ptr) with + Pre => + RFLX.P.Message.Has_Buffer (Ctx), + Post => + not Has_Buffer (Ctx) + and Buffer /= null + and Ctx.Buffer_First = Buffer'First + and Ctx.Buffer_Last = Buffer'Last + and Ctx.Buffer_First = Ctx.Buffer_First'Old + and Ctx.Buffer_Last = Ctx.Buffer_Last'Old + and Ctx.First = Ctx.First'Old + and Ctx.Last = Ctx.Last'Old + and Context_Cursors (Ctx) = Context_Cursors (Ctx)'Old, + Depends => + (Ctx => Ctx, Buffer => Ctx); + + procedure Copy (Ctx : Context; Buffer : out RFLX_Types.Bytes) with + Pre => + RFLX.P.Message.Has_Buffer (Ctx) + and then RFLX.P.Message.Well_Formed_Message (Ctx) + and then RFLX.P.Message.Byte_Size (Ctx) = Buffer'Length; + + function Read (Ctx : Context) return RFLX_Types.Bytes with + Ghost, + Pre => + RFLX.P.Message.Has_Buffer (Ctx) + and then RFLX.P.Message.Well_Formed_Message (Ctx); + + pragma Warnings (Off, "formal parameter ""*"" is not referenced"); + + pragma Warnings (Off, "unused variable ""*"""); + + function Always_Valid (Buffer : RFLX_Types.Bytes) return Boolean is + (True); + + pragma Warnings (On, "unused variable ""*"""); + + pragma Warnings (On, "formal parameter ""*"" is not referenced"); + + generic + with procedure Read (Buffer : RFLX_Types.Bytes); + with function Pre (Buffer : RFLX_Types.Bytes) return Boolean is Always_Valid; + procedure Generic_Read (Ctx : Context) with + Pre => + RFLX.P.Message.Has_Buffer (Ctx) + and then RFLX.P.Message.Well_Formed_Message (Ctx) + and then Pre (Read (Ctx)); + + pragma Warnings (Off, "formal parameter ""*"" is not referenced"); + + pragma Warnings (Off, "unused variable ""*"""); + + function Always_Valid (Context_Buffer_Length : RFLX_Types.Length; Offset : RFLX_Types.Length) return Boolean is + (True); + + pragma Warnings (On, "unused variable ""*"""); + + pragma Warnings (On, "formal parameter ""*"" is not referenced"); + + generic + with procedure Write (Buffer : out RFLX_Types.Bytes; Length : out RFLX_Types.Length; Context_Buffer_Length : RFLX_Types.Length; Offset : RFLX_Types.Length); + with function Pre (Context_Buffer_Length : RFLX_Types.Length; Offset : RFLX_Types.Length) return Boolean is Always_Valid; + procedure Generic_Write (Ctx : in out Context; Offset : RFLX_Types.Length := 0) with + Pre => + not Ctx'Constrained + and then RFLX.P.Message.Has_Buffer (Ctx) + and then Offset < RFLX.P.Message.Buffer_Length (Ctx) + and then Pre (RFLX.P.Message.Buffer_Length (Ctx), Offset), + Post => + Has_Buffer (Ctx) + and Ctx.Buffer_First = Ctx.Buffer_First'Old + and Ctx.Buffer_Last = Ctx.Buffer_Last'Old + and Ctx.First = RFLX_Types.To_First_Bit_Index (Ctx.Buffer_First) + and Initialized (Ctx); + + function Has_Buffer (Ctx : Context) return Boolean; + + function Buffer_Length (Ctx : Context) return RFLX_Types.Length with + Pre => + RFLX.P.Message.Has_Buffer (Ctx); + + function Size (Ctx : Context) return RFLX_Types.Bit_Length with + Post => + Size'Result rem RFLX_Types.Byte'Size = 0; + + function Byte_Size (Ctx : Context) return RFLX_Types.Length; + + function Message_Last (Ctx : Context) return RFLX_Types.Bit_Length with + Pre => + RFLX.P.Message.Has_Buffer (Ctx) + and then RFLX.P.Message.Well_Formed_Message (Ctx); + + function Written_Last (Ctx : Context) return RFLX_Types.Bit_Length; + + procedure Data (Ctx : Context; Data : out RFLX_Types.Bytes) with + Pre => + RFLX.P.Message.Has_Buffer (Ctx) + and then RFLX.P.Message.Well_Formed_Message (Ctx) + and then Data'Length = RFLX.P.Message.Byte_Size (Ctx); + + pragma Warnings (Off, "postcondition does not mention function result"); + + function Valid_Value (Fld : Field; Val : RFLX_Types.Base_Integer) return Boolean with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); + + pragma Warnings (Off, "postcondition does not mention function result"); + + function Field_Condition (Ctx : Context; Fld : Field; Val : RFLX_Types.Base_Integer) return Boolean with + Pre => + RFLX.P.Message.Has_Buffer (Ctx) + and then RFLX.P.Message.Valid_Value (Fld, Val) + and then RFLX.P.Message.Valid_Next (Ctx, Fld) + and then RFLX.P.Message.Sufficient_Space (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); + + function Field_Size (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Length with + Pre => + RFLX.P.Message.Valid_Next (Ctx, Fld); + + pragma Warnings (Off, "postcondition does not mention function result"); + + function Field_First (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with + Pre => + RFLX.P.Message.Valid_Next (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); + + function Field_Last (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Length with + Pre => + RFLX.P.Message.Valid_Next (Ctx, Fld) + and then RFLX.P.Message.Sufficient_Space (Ctx, Fld); + + function Valid_Next (Ctx : Context; Fld : Field) return Boolean; + + function Available_Space (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Length with + Pre => + RFLX.P.Message.Valid_Next (Ctx, Fld); + + function Sufficient_Space (Ctx : Context; Fld : Field) return Boolean with + Pre => + RFLX.P.Message.Valid_Next (Ctx, Fld); + + procedure Verify (Ctx : in out Context; Fld : Field) with + Pre => + RFLX.P.Message.Has_Buffer (Ctx), + Post => + Has_Buffer (Ctx) + and Ctx.Buffer_First = Ctx.Buffer_First'Old + and Ctx.Buffer_Last = Ctx.Buffer_Last'Old + and Ctx.First = Ctx.First'Old + and Ctx.Last = Ctx.Last'Old; + + procedure Verify_Message (Ctx : in out Context) with + Pre => + RFLX.P.Message.Has_Buffer (Ctx), + Post => + Has_Buffer (Ctx) + and Ctx.Buffer_First = Ctx.Buffer_First'Old + and Ctx.Buffer_Last = Ctx.Buffer_Last'Old + and Ctx.First = Ctx.First'Old + and Ctx.Last = Ctx.Last'Old; + + function Present (Ctx : Context; Fld : Field) return Boolean; + + function Well_Formed (Ctx : Context; Fld : Field) return Boolean; + + function Valid (Ctx : Context; Fld : Field) return Boolean with + Post => + (if Valid'Result then Well_Formed (Ctx, Fld) and Present (Ctx, Fld)); + + function Incomplete (Ctx : Context; Fld : Field) return Boolean; + + function Invalid (Ctx : Context; Fld : Field) return Boolean; + + function Well_Formed_Message (Ctx : Context) return Boolean with + Pre => + RFLX.P.Message.Has_Buffer (Ctx); + + function Valid_Message (Ctx : Context) return Boolean with + Pre => + RFLX.P.Message.Has_Buffer (Ctx); + + pragma Warnings (Off, "postcondition does not mention function result"); + + function Incomplete_Message (Ctx : Context) return Boolean with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); + + pragma Warnings (Off, "precondition is always False"); + + function Get_A (Ctx : Context) return Boolean with + Pre => + RFLX.P.Message.Valid (Ctx, RFLX.P.Message.F_A); + + function Get_B (Ctx : Context) return RFLX.P.T with + Pre => + RFLX.P.Message.Valid (Ctx, RFLX.P.Message.F_B); + + pragma Warnings (On, "precondition is always False"); + + pragma Warnings (Off, "postcondition does not mention function result"); + + function Valid_Length (Ctx : Context; Fld : Field; Length : RFLX_Types.Length) return Boolean with + Pre => + RFLX.P.Message.Valid_Next (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); + + pragma Warnings (Off, "aspect ""*"" not enforced on inlined subprogram ""*"""); + + procedure Set_A (Ctx : in out Context; Val : Boolean) with + Inline_Always, + Pre => + not Ctx'Constrained + and then RFLX.P.Message.Has_Buffer (Ctx) + and then RFLX.P.Message.Valid_Next (Ctx, RFLX.P.Message.F_A) + and then Valid_Boolean (To_Base_Integer (Val)) + and then RFLX.P.Message.Available_Space (Ctx, RFLX.P.Message.F_A) >= RFLX.P.Message.Field_Size (Ctx, RFLX.P.Message.F_A) + and then RFLX.P.Message.Field_Condition (Ctx, RFLX.P.Message.F_A, To_Base_Integer (Val)), + Post => + Has_Buffer (Ctx) + and Valid (Ctx, F_A) + and Get_A (Ctx) = Val + and Invalid (Ctx, F_B) + and Valid_Next (Ctx, F_B) + and Ctx.Buffer_First = Ctx.Buffer_First'Old + and Ctx.Buffer_Last = Ctx.Buffer_Last'Old + and Ctx.First = Ctx.First'Old + and Ctx.Last = Ctx.Last'Old + and Valid_Next (Ctx, F_A) = Valid_Next (Ctx, F_A)'Old + and Field_First (Ctx, F_A) = Field_First (Ctx, F_A)'Old; + + procedure Set_B (Ctx : in out Context; Val : RFLX.P.T) with + Inline_Always, + Pre => + not Ctx'Constrained + and then RFLX.P.Message.Has_Buffer (Ctx) + and then RFLX.P.Message.Valid_Next (Ctx, RFLX.P.Message.F_B) + and then RFLX.P.Valid_T (RFLX.P.To_Base_Integer (Val)) + and then RFLX.P.Message.Available_Space (Ctx, RFLX.P.Message.F_B) >= RFLX.P.Message.Field_Size (Ctx, RFLX.P.Message.F_B) + and then RFLX.P.Message.Field_Condition (Ctx, RFLX.P.Message.F_B, RFLX.P.To_Base_Integer (Val)), + Post => + Has_Buffer (Ctx) + and Valid (Ctx, F_B) + and Get_B (Ctx) = Val + and (if Well_Formed_Message (Ctx) then Message_Last (Ctx) = Field_Last (Ctx, F_B)) + and Ctx.Buffer_First = Ctx.Buffer_First'Old + and Ctx.Buffer_Last = Ctx.Buffer_Last'Old + and Ctx.First = Ctx.First'Old + and Ctx.Last = Ctx.Last'Old + and Valid_Next (Ctx, F_B) = Valid_Next (Ctx, F_B)'Old + and Get_A (Ctx) = Get_A (Ctx)'Old + and Field_First (Ctx, F_B) = Field_First (Ctx, F_B)'Old + and (for all F in Field range F_A .. F_A => + Context_Cursors_Index (Context_Cursors (Ctx), F) = Context_Cursors_Index (Context_Cursors (Ctx)'Old, F)); + + pragma Warnings (On, "aspect ""*"" not enforced on inlined subprogram ""*"""); + + function Context_Cursor (Ctx : Context; Fld : Field) return Field_Cursor with + Annotate => + (GNATprove, Inline_For_Proof), + Ghost; + + function Context_Cursors (Ctx : Context) return Field_Cursors with + Annotate => + (GNATprove, Inline_For_Proof), + Ghost; + + function Context_Cursors_Index (Cursors : Field_Cursors; Fld : Field) return Field_Cursor with + Annotate => + (GNATprove, Inline_For_Proof), + Ghost; + + type Structure is + record + A : Boolean; + B : RFLX.P.T; + end record; + + function Valid_Structure (Struct : Structure) return Boolean; + + procedure To_Structure (Ctx : Context; Struct : out Structure) with + Pre => + RFLX.P.Message.Has_Buffer (Ctx) + and then RFLX.P.Message.Well_Formed_Message (Ctx), + Post => + Valid_Structure (Struct); + + function Sufficient_Buffer_Length (Ctx : Context; Unused_Struct : Structure) return Boolean; + + procedure To_Context (Struct : Structure; Ctx : in out Context) with + Pre => + not Ctx'Constrained + and then RFLX.P.Message.Has_Buffer (Ctx) + and then RFLX.P.Message.Valid_Structure (Struct) + and then RFLX.P.Message.Sufficient_Buffer_Length (Ctx, Struct), + Post => + Has_Buffer (Ctx) + and Well_Formed_Message (Ctx) + and Ctx.Buffer_First = Ctx.Buffer_First'Old + and Ctx.Buffer_Last = Ctx.Buffer_Last'Old; + + function Field_Size_A (Struct : Structure) return RFLX_Types.Bit_Length with + Pre => + Valid_Structure (Struct); + + function Field_Size_B (Struct : Structure) return RFLX_Types.Bit_Length with + Pre => + Valid_Structure (Struct); + +private + + type Cursor_State is (S_Valid, S_Well_Formed, S_Invalid, S_Incomplete); + + type Field_Cursor is + record + State : Cursor_State := S_Invalid; + First : RFLX_Types.Bit_Index := RFLX_Types.Bit_Index'First; + Last : RFLX_Types.Bit_Length := RFLX_Types.Bit_Length'First; + Value : RFLX_Types.Base_Integer := 0; + end record; + + type Field_Cursors is array (Virtual_Field) of Field_Cursor; + + function Well_Formed (Cursor : Field_Cursor) return Boolean is + (Cursor.State = S_Valid + or Cursor.State = S_Well_Formed); + + function Valid (Cursor : Field_Cursor) return Boolean is + (Cursor.State = S_Valid); + + function Invalid (Cursor : Field_Cursor) return Boolean is + (Cursor.State = S_Invalid + or Cursor.State = S_Incomplete); + + pragma Warnings (Off, "postcondition does not mention function result"); + + function Cursors_Invariant (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length) return Boolean is + ((for all F in Field => + (if + Well_Formed (Cursors (F)) + then + Cursors (F).First >= First + and Cursors (F).Last <= Verified_Last + and Cursors (F).First <= Cursors (F).Last + 1 + and Valid_Value (F, Cursors (F).Value)))) + with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); + + pragma Warnings (Off, "formal parameter ""*"" is not referenced"); + + pragma Warnings (Off, "postcondition does not mention function result"); + + pragma Warnings (Off, "unused variable ""*"""); + + function Valid_Predecessors_Invariant (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr) return Boolean is + ((if Well_Formed (Cursors (F_A)) then True) + and then (if Well_Formed (Cursors (F_B)) then Valid (Cursors (F_A)))) + with + Pre => + Cursors_Invariant (Cursors, First, Verified_Last), + Post => + True; + + pragma Warnings (On, "formal parameter ""*"" is not referenced"); + + pragma Warnings (On, "postcondition does not mention function result"); + + pragma Warnings (On, "unused variable ""*"""); + + pragma Warnings (Off, "postcondition does not mention function result"); + + function Valid_Next_Internal (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr; Fld : Field) return Boolean is + ((case Fld is + when F_A => + True, + when F_B => + (Valid (Cursors (F_A)) + and then True))) + with + Pre => + Cursors_Invariant (Cursors, First, Verified_Last) + and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); + + pragma Warnings (Off, "unused variable ""*"""); + + pragma Warnings (Off, "formal parameter ""*"" is not referenced"); + + function Field_Size_Internal (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr; Fld : Field) return RFLX_Types.Bit_Length'Base is + ((case Fld is + when F_A => + 1, + when F_B => + 7)) + with + Pre => + Cursors_Invariant (Cursors, First, Verified_Last) + and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer) + and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, Fld); + + pragma Warnings (On, "unused variable ""*"""); + + pragma Warnings (On, "formal parameter ""*"" is not referenced"); + + pragma Warnings (Off, "postcondition does not mention function result"); + + pragma Warnings (Off, "unused variable ""*"""); + + pragma Warnings (Off, "no recursive call visible"); + + pragma Warnings (Off, "formal parameter ""*"" is not referenced"); + + function Field_First_Internal (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr; Fld : Field) return RFLX_Types.Bit_Index'Base is + ((case Fld is + when F_A => + First, + when F_B => + First + 1)) + with + Pre => + Cursors_Invariant (Cursors, First, Verified_Last) + and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer) + and then Valid_Next_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, Fld), + Post => + True, + Subprogram_Variant => + (Decreases => + Fld); + + pragma Warnings (On, "postcondition does not mention function result"); + + pragma Warnings (On, "unused variable ""*"""); + + pragma Warnings (On, "no recursive call visible"); + + pragma Warnings (On, "formal parameter ""*"" is not referenced"); + + pragma Warnings (Off, """Buffer"" is not modified, could be of access constant type"); + + pragma Warnings (Off, "postcondition does not mention function result"); + + function Valid_Context (Buffer_First, Buffer_Last : RFLX_Types.Index; First : RFLX_Types.Bit_Index; Last : RFLX_Types.Bit_Length; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr; Cursors : Field_Cursors) return Boolean is + ((if Buffer /= null then Buffer'First = Buffer_First and Buffer'Last = Buffer_Last) + and then (RFLX_Types.To_Index (First) >= Buffer_First + and RFLX_Types.To_Index (Last) <= Buffer_Last + and Buffer_Last < RFLX_Types.Index'Last + and First <= Last + 1 + and Last < RFLX_Types.Bit_Index'Last + and First rem RFLX_Types.Byte'Size = 1 + and Last rem RFLX_Types.Byte'Size = 0) + and then First - 1 <= Verified_Last + and then First - 1 <= Written_Last + and then Verified_Last <= Written_Last + and then Written_Last <= Last + and then First rem RFLX_Types.Byte'Size = 1 + and then Last rem RFLX_Types.Byte'Size = 0 + and then Verified_Last rem RFLX_Types.Byte'Size = 0 + and then Written_Last rem RFLX_Types.Byte'Size = 0 + and then Cursors_Invariant (Cursors, First, Verified_Last) + and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer) + and then ((if Invalid (Cursors (F_A)) then Invalid (Cursors (F_B)))) + and then ((if + Well_Formed (Cursors (F_A)) + then + (Cursors (F_A).Last - Cursors (F_A).First + 1 = 1 + and then Cursors (F_A).First = First)) + and then (if + Well_Formed (Cursors (F_B)) + then + (Cursors (F_B).Last - Cursors (F_B).First + 1 = 7 + and then Cursors (F_B).First = Cursors (F_A).Last + 1)))) + with + Post => + True; + + pragma Warnings (On, """Buffer"" is not modified, could be of access constant type"); + + pragma Warnings (On, "postcondition does not mention function result"); + + type Context (Buffer_First, Buffer_Last : RFLX_Types.Index := RFLX_Types.Index'First; First : RFLX_Types.Bit_Index := RFLX_Types.Bit_Index'First; Last : RFLX_Types.Bit_Length := RFLX_Types.Bit_Length'First) is + record + Verified_Last : RFLX_Types.Bit_Length := First - 1; + Written_Last : RFLX_Types.Bit_Length := First - 1; + Buffer : RFLX_Types.Bytes_Ptr := null; + Cursors : Field_Cursors := (others => <>); + end record with + Dynamic_Predicate => + Valid_Context (Context.Buffer_First, Context.Buffer_Last, Context.First, Context.Last, Context.Verified_Last, Context.Written_Last, Context.Buffer, Context.Cursors); + + function Initialized (Ctx : Context) return Boolean is + (Ctx.Verified_Last = Ctx.First - 1 + and then Valid_Next (Ctx, F_A) + and then RFLX.P.Message.Field_First (Ctx, RFLX.P.Message.F_A) rem RFLX_Types.Byte'Size = 1 + and then Available_Space (Ctx, F_A) = Ctx.Last - Ctx.First + 1 + and then (for all F in Field => + Invalid (Ctx, F))); + + function Read (Ctx : Context) return RFLX_Types.Bytes is + (Ctx.Buffer.all (RFLX_Types.To_Index (Ctx.First) .. RFLX_Types.To_Index (Ctx.Verified_Last))); + + function Has_Buffer (Ctx : Context) return Boolean is + (Ctx.Buffer /= null); + + function Buffer_Length (Ctx : Context) return RFLX_Types.Length is + (Ctx.Buffer'Length); + + function Size (Ctx : Context) return RFLX_Types.Bit_Length is + (Ctx.Verified_Last - Ctx.First + 1); + + function Byte_Size (Ctx : Context) return RFLX_Types.Length is + (RFLX_Types.To_Length (Size (Ctx))); + + function Message_Last (Ctx : Context) return RFLX_Types.Bit_Length is + (Ctx.Verified_Last); + + function Written_Last (Ctx : Context) return RFLX_Types.Bit_Length is + (Ctx.Written_Last); + + function Valid_Value (Fld : Field; Val : RFLX_Types.Base_Integer) return Boolean is + ((case Fld is + when F_A => + Valid_Boolean (Val), + when F_B => + RFLX.P.Valid_T (Val))); + + function Field_Condition (Ctx : Context; Fld : Field; Val : RFLX_Types.Base_Integer) return Boolean is + ((case Fld is + when F_A => + True, + when F_B => + RFLX_Types.Base_Integer (Ctx.Cursors (F_A).Value) = RFLX_Types.Base_Integer (To_Base_Integer (True)))); + + function Field_Size (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Length is + (Field_Size_Internal (Ctx.Cursors, Ctx.First, Ctx.Verified_Last, Ctx.Written_Last, Ctx.Buffer, Fld)); + + function Field_First (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index is + (Field_First_Internal (Ctx.Cursors, Ctx.First, Ctx.Verified_Last, Ctx.Written_Last, Ctx.Buffer, Fld)); + + function Field_Last (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Length is + (Field_First (Ctx, Fld) + Field_Size (Ctx, Fld) - 1); + + function Valid_Next (Ctx : Context; Fld : Field) return Boolean is + (Valid_Next_Internal (Ctx.Cursors, Ctx.First, Ctx.Verified_Last, Ctx.Written_Last, Ctx.Buffer, Fld)); + + function Available_Space (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Length is + (Ctx.Last - Field_First (Ctx, Fld) + 1); + + function Sufficient_Space (Ctx : Context; Fld : Field) return Boolean is + (Available_Space (Ctx, Fld) >= Field_Size (Ctx, Fld)); + + function Present (Ctx : Context; Fld : Field) return Boolean is + (Well_Formed (Ctx.Cursors (Fld)) + and then Ctx.Cursors (Fld).First < Ctx.Cursors (Fld).Last + 1); + + function Well_Formed (Ctx : Context; Fld : Field) return Boolean is + (Ctx.Cursors (Fld).State = S_Valid + or Ctx.Cursors (Fld).State = S_Well_Formed); + + function Valid (Ctx : Context; Fld : Field) return Boolean is + (Ctx.Cursors (Fld).State = S_Valid + and then Ctx.Cursors (Fld).First < Ctx.Cursors (Fld).Last + 1); + + function Incomplete (Ctx : Context; Fld : Field) return Boolean is + (Ctx.Cursors (Fld).State = S_Incomplete); + + function Invalid (Ctx : Context; Fld : Field) return Boolean is + (Ctx.Cursors (Fld).State = S_Invalid + or Ctx.Cursors (Fld).State = S_Incomplete); + + function Well_Formed_Message (Ctx : Context) return Boolean is + (Valid (Ctx, F_B) + and then RFLX_Types.Base_Integer (Ctx.Cursors (F_A).Value) = RFLX_Types.Base_Integer (To_Base_Integer (True))); + + function Valid_Message (Ctx : Context) return Boolean is + (Valid (Ctx, F_B) + and then RFLX_Types.Base_Integer (Ctx.Cursors (F_A).Value) = RFLX_Types.Base_Integer (To_Base_Integer (True))); + + function Incomplete_Message (Ctx : Context) return Boolean is + ((for some F in Field => + Incomplete (Ctx, F))); + + function Get_A (Ctx : Context) return Boolean is + (To_Actual (Ctx.Cursors (F_A).Value)); + + function Get_B (Ctx : Context) return RFLX.P.T is + (To_Actual (Ctx.Cursors (F_B).Value)); + + function Valid_Size (Ctx : Context; Fld : Field; Size : RFLX_Types.Bit_Length) return Boolean is + (Size = Field_Size (Ctx, Fld)) + with + Pre => + RFLX.P.Message.Valid_Next (Ctx, Fld); + + function Valid_Length (Ctx : Context; Fld : Field; Length : RFLX_Types.Length) return Boolean is + (Valid_Size (Ctx, Fld, RFLX_Types.To_Bit_Length (Length))); + + function Context_Cursor (Ctx : Context; Fld : Field) return Field_Cursor is + (Ctx.Cursors (Fld)); + + function Context_Cursors (Ctx : Context) return Field_Cursors is + (Ctx.Cursors); + + function Context_Cursors_Index (Cursors : Field_Cursors; Fld : Field) return Field_Cursor is + (Cursors (Fld)); + + function Valid_Structure (Struct : Structure) return Boolean is + (To_Base_Integer (Struct.A) = RFLX_Types.Base_Integer (To_Base_Integer (True))); + + function Sufficient_Buffer_Length (Ctx : Context; Unused_Struct : Structure) return Boolean is + (RFLX_Types.Base_Integer (RFLX_Types.To_Last_Bit_Index (Ctx.Buffer_Last) - RFLX_Types.To_First_Bit_Index (Ctx.Buffer_First) + 1) >= 8); + + function Field_Size_A (Struct : Structure) return RFLX_Types.Bit_Length is + (1); + + function Field_Size_B (Struct : Structure) return RFLX_Types.Bit_Length is + (7); + +end RFLX.P.Message; diff --git a/tests/data/generator/generated/boolean_variable/rflx-p.ads b/tests/data/generator/generated/boolean_variable/rflx-p.ads new file mode 100644 index 000000000..8b3d5040c --- /dev/null +++ b/tests/data/generator/generated/boolean_variable/rflx-p.ads @@ -0,0 +1,38 @@ +------------------------------------------------------------------------------ +-- -- +-- Generated by RecordFlux -- +-- -- +-- Copyright (C) AdaCore GmbH -- +-- -- +-- SPDX-License-Identifier: Apache-2.0 -- +-- -- +------------------------------------------------------------------------------ + +pragma Ada_2012; +pragma Style_Checks ("N3aAbCdefhiIklnOprStux"); +pragma Warnings (Off, "redundant conversion"); +with RFLX.RFLX_Types; + +package RFLX.P with + SPARK_Mode +is + + type T is range 0 .. 127 with + Size => + 7; + + use type RFLX.RFLX_Types.Base_Integer; + + function Valid_T (Val : RFLX.RFLX_Types.Base_Integer) return Boolean is + (Val <= 127); + + function To_Base_Integer (Val : RFLX.P.T) return RFLX.RFLX_Types.Base_Integer is + (RFLX.RFLX_Types.Base_Integer (Val)); + + function To_Actual (Val : RFLX.RFLX_Types.Base_Integer) return RFLX.P.T is + (RFLX.P.T (Val)) + with + Pre => + Valid_T (Val); + +end RFLX.P; diff --git a/tests/data/generator/generated/boolean_variable/rflx-rflx_arithmetic.adb b/tests/data/generator/generated/boolean_variable/rflx-rflx_arithmetic.adb new file mode 100644 index 000000000..a803affe3 --- /dev/null +++ b/tests/data/generator/generated/boolean_variable/rflx-rflx_arithmetic.adb @@ -0,0 +1,87 @@ +------------------------------------------------------------------------------ +-- -- +-- Generated by RecordFlux -- +-- -- +-- Copyright (C) AdaCore GmbH -- +-- -- +-- SPDX-License-Identifier: Apache-2.0 -- +-- -- +------------------------------------------------------------------------------ + +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; + + procedure Lemma_Size (Val : Base_Integer; Size : Positive) is + begin + if Size < Base_Integer'Size then + pragma Assert (Val < 2 ** Size); + pragma Assert (U64 (Val) < 2 ** Size); + pragma Assert (Fits_Into (U64 (Val), Size)); + else + pragma Assert (Size = 63); + pragma Assert (Fits_Into (U64 (Val), Size)); + end if; + end Lemma_Size; + +end RFLX.RFLX_Arithmetic; diff --git a/tests/data/generator/generated/boolean_variable/rflx-rflx_arithmetic.ads b/tests/data/generator/generated/boolean_variable/rflx-rflx_arithmetic.ads new file mode 100644 index 000000000..338c61b66 --- /dev/null +++ b/tests/data/generator/generated/boolean_variable/rflx-rflx_arithmetic.ads @@ -0,0 +1,112 @@ +------------------------------------------------------------------------------ +-- -- +-- Generated by RecordFlux -- +-- -- +-- Copyright (C) AdaCore GmbH -- +-- -- +-- SPDX-License-Identifier: Apache-2.0 -- +-- -- +------------------------------------------------------------------------------ + +pragma Style_Checks ("N3aAbCdefhiIklnOprStux"); +pragma Warnings (Off, """Always_Terminates"" is not a valid aspect identifier"); + +package RFLX.RFLX_Arithmetic with + SPARK_Mode, + Always_Terminates +is + + type U64 is mod 2**64 with + Annotate => (GNATprove, No_Wrap_Around); + + type Base_Integer is range 0 .. 2 ** 63 - 1; + + -- 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; + + function Fits_Into (V : Base_Integer; Bits : Natural) return Boolean + is (if Bits < Base_Integer'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); + + pragma Warnings (Off, "aspect Unreferenced specified for ""Total_Bits"""); + + -- 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; + + pragma Warnings (On, "aspect Unreferenced specified for ""Total_Bits"""); + + procedure Lemma_Size (Val : Base_Integer; Size : Positive) + with Ghost, + Pre => Size in 1 .. 63 and then Fits_Into (Val, Size), + Post => Fits_Into (U64 (Val), Size); + +end RFLX.RFLX_Arithmetic; diff --git a/tests/data/generator/generated/boolean_variable/rflx-rflx_builtin_types-conversions.ads b/tests/data/generator/generated/boolean_variable/rflx-rflx_builtin_types-conversions.ads new file mode 100644 index 000000000..90a9e0583 --- /dev/null +++ b/tests/data/generator/generated/boolean_variable/rflx-rflx_builtin_types-conversions.ads @@ -0,0 +1,73 @@ +------------------------------------------------------------------------------ +-- -- +-- Generated by RecordFlux -- +-- -- +-- Copyright (C) AdaCore GmbH -- +-- -- +-- SPDX-License-Identifier: Apache-2.0 -- +-- -- +------------------------------------------------------------------------------ + +pragma Style_Checks ("N3aAbCdefhiIklnOprStux"); +pragma Warnings (Off, """Always_Terminates"" is not a valid aspect identifier"); + +with RFLX.RFLX_Arithmetic; + +package RFLX.RFLX_Builtin_Types.Conversions with + SPARK_Mode, + Always_Terminates +is + + function Valid_Boolean (Val : RFLX.RFLX_Arithmetic.U64) return Boolean is + (case Val is + when 0 | 1 => + True, + when others => + False); + + function To_U64 (Enum : Boolean) return RFLX.RFLX_Arithmetic.U64 is + (case Enum is + when False => + 0, + when True => + 1); + + function To_Actual (Val : RFLX.RFLX_Arithmetic.U64) return Boolean is + (case Val is + when 0 => + False, + when 1 => + True, + when others => + False) + with + Pre => + Valid_Boolean (Val); + + function Valid_Boolean (Val : RFLX.RFLX_Arithmetic.Base_Integer) return Boolean is + (case Val is + when 0 | 1 => + True, + when others => + False); + + function To_Base_Integer (Enum : Boolean) return RFLX.RFLX_Arithmetic.Base_Integer is + (case Enum is + when False => + 0, + when True => + 1); + + function To_Actual (Val : RFLX.RFLX_Arithmetic.Base_Integer) return Boolean is + (case Val is + when 0 => + False, + when 1 => + True, + when others => + False) + with + Pre => + Valid_Boolean (Val); + +end RFLX.RFLX_Builtin_Types.Conversions; diff --git a/tests/data/generator/generated/boolean_variable/rflx-rflx_builtin_types.ads b/tests/data/generator/generated/boolean_variable/rflx-rflx_builtin_types.ads new file mode 100644 index 000000000..47928632f --- /dev/null +++ b/tests/data/generator/generated/boolean_variable/rflx-rflx_builtin_types.ads @@ -0,0 +1,33 @@ +------------------------------------------------------------------------------ +-- -- +-- Generated by RecordFlux -- +-- -- +-- Copyright (C) AdaCore GmbH -- +-- -- +-- SPDX-License-Identifier: Apache-2.0 -- +-- -- +------------------------------------------------------------------------------ + +pragma Style_Checks ("N3aAbCdefhiIklnOprStux"); +pragma Warnings (Off, """Always_Terminates"" is not a valid aspect identifier"); + +package RFLX.RFLX_Builtin_Types with + SPARK_Mode, + Always_Terminates +is + + type Length is new Natural; + + type Index is new Length range 1 .. Length'Last; + + type Byte is mod 2**8; + + type Bytes is array (Index range <>) of Byte; + + type Bytes_Ptr is access Bytes; + + type Bit_Length is range 0 .. Length'Last * 8; + + type Boolean_Base is mod 2; + +end RFLX.RFLX_Builtin_Types; diff --git a/tests/data/generator/generated/boolean_variable/rflx-rflx_generic_types-generic_operations.adb b/tests/data/generator/generated/boolean_variable/rflx-rflx_generic_types-generic_operations.adb new file mode 100644 index 000000000..0faf2699a --- /dev/null +++ b/tests/data/generator/generated/boolean_variable/rflx-rflx_generic_types-generic_operations.adb @@ -0,0 +1,409 @@ +------------------------------------------------------------------------------ +-- -- +-- Generated by RecordFlux -- +-- -- +-- Copyright (C) AdaCore GmbH -- +-- -- +-- SPDX-License-Identifier: Apache-2.0 -- +-- -- +------------------------------------------------------------------------------ + +pragma Style_Checks ("N3aAbCdefhiIklnOprStux"); + +with RFLX.RFLX_Arithmetic; + +package body RFLX.RFLX_Generic_Types.Generic_Operations with + SPARK_Mode +is + + -- + -- Terminology + -- + -- -----XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX---- Data + -- + -- |-------|-------|-------|-------|-------| Value Bytes + -- 3 LMB 11 19 27 35 RMB 43 + -- + -- |----| |----| + -- LME_Offset RME_Offset + -- + -- |--| |--| + -- LME_Size RME_Size + -- + -- |-------|-------|-------|-------|-------|-------| Data Bytes + -- 0 8 16 24 32 40 + -- LME RME + -- + -- LME: Leftmost Element of Data + -- RME: Rightmost Element of Data + -- + -- LSB: Leftmost Byte of Value + -- RMB: Rightmost Byte of Value + -- + -- LME_Offset: Bits the LME is shifted right relative to first of LME + -- RME_Offset: Bits the RME is shifted left relative to last of RME + -- + -- LME_Size: Number of bits of LME contained in LMB + -- RME_Size: Number of bits of RME contained in RMB + -- + -- LME_Index: Index pointing to LME + -- RME_Index: Index pointing to RME + -- + + use RFLX.RFLX_Arithmetic; + + procedure Get_Index_Offset + (First, Last : Long_Integer; + Off : Offset; + Value_Size : Positive; + RME_Index : out Index; + LME_Index : out Index; + RME_Size : out Natural; + LME_Size : out Natural) + with + Pre => + (Value_Size in 1 .. U64'Size + and then Last >= Long_Integer (Index'First) and then Last <= Long_Integer (Index'Last) + and then First >= Long_Integer (Index'First) and then First <= Long_Integer (Index'Last) + and then Long_Integer ((Natural (Off) + Value_Size - 1) / Byte'Size) < Long_Integer (Last - First + 1)), + Post => + (RME_Index = Index (Last - Long_Integer (Off) / Byte'Size) + and then LME_Index = Index (Last - (Long_Integer (Off) + Long_Integer (Value_Size) - 1) / Byte'Size) + and then RME_Size = Byte'Size - Natural (Off) + and then LME_Size = (Natural (Off) + Value_Size + Byte'Size - 1) mod Byte'Size + 1) + is + begin + RME_Index := Index (Last - Long_Integer (Off) / Byte'Size); + LME_Index := Index (Last - (Long_Integer (Off) + Long_Integer (Value_Size) - 1) / Byte'Size); + RME_Size := Byte'Size - Natural (Off); + LME_Size := (Natural (Off) + Value_Size + Byte'Size - 1) mod Byte'Size + 1; + end Get_Index_Offset; + + function U64_Extract + (Buffer : Bytes; + First : Index; + Last : Index; + Off : Offset; + Value_Size : Positive) return U64 + with + Pre => + (First >= Buffer'First + and then Last <= Buffer'Last + and then Value_Size in 1 .. U64'Size + and then Long_Integer ((Natural (Off) + Value_Size - 1) / Byte'Size) < Buffer (First .. Last)'Length), + Post => + (if Value_Size < U64'Size then U64_Extract'Result < 2**Value_Size) + is + Data : constant Bytes := Buffer (First .. Last); + + RME_Index : Index; + LME_Index : Index; + + RME_Offset : constant Natural := Natural (Off); + RME_Size : Natural; + + LME_Size : Natural; + LME_Offset : Natural; + Result : U64 := 0; + + begin + -- This function simply iterates over all data bytes that contain + -- relevant data, from most significant to least significant, and adds + -- them up in Result, shifting the Result before the addition as needed + -- (see helper function Shift_Add). + + -- We track the number of bits that are contained in Result to bound the + -- current value of Result by 2 ** (number of bits). At the end of the + -- function, the number of bits should be Value_Size. + + -- We start with the most significant byte. In network-byte order this + -- is the rightmost byte. We need to take into account the case where + -- this is the only byte. + + Get_Index_Offset (Long_Integer (Data'First), Long_Integer (Data'Last), Off, Value_Size, RME_Index, LME_Index, RME_Size, LME_Size); + LME_Offset := Byte'Size - LME_Size; + + declare + Tmp : U64 := Mask_Upper (Byte'Pos (Data (LME_Index)), LME_Size); + begin + if RME_Index = LME_Index then + Tmp := Right_Shift (Tmp, RME_Offset, LME_Size); + end if; + Result := Result + Tmp; + end; + + -- If it was the only byte, we are done. + + if RME_Index = LME_Index then + pragma Assert (Result < 2 ** (LME_Size - RME_Offset)); + return Result; + end if; + + pragma Assert (Fits_Into (Result, LME_Size)); + + -- We now iterate over the "inner bytes" excluding the two extreme bytes. + for I in LME_Index + 1 .. RME_Index - 1 loop + Result := + Shift_Add + (Result, + Byte'Pos (Data (I)), + Byte'Size, + Natural (I - LME_Index) * Byte'Size - LME_Offset); + pragma Loop_Invariant + (Fits_Into (Result, Natural (I - LME_Index + 1) * Byte'Size - LME_Offset)); + end loop; + + -- We now add the relevant bits from the last byte. + pragma Assert (RME_Size in 1 .. U64'Size); + pragma Assert (if LME_Index + 1 <= RME_Index - 1 then Fits_Into (Result, Natural (RME_Index - LME_Index) * Byte'Size - LME_Offset)); + pragma Assert (if LME_Index + 1 > RME_Index - 1 then Fits_Into (Result, Natural (RME_Index - LME_Index) * Byte'Size - LME_Offset)); + pragma Assert (Value_Size - RME_Size = Natural (RME_Index - LME_Index) * Byte'Size - LME_Offset); + pragma Assert (Fits_Into (Result, Value_Size - RME_Size)); + declare + Bits_To_Read : constant U64 := + Right_Shift (Byte'Pos (Data (RME_Index)), RME_Offset, Byte'Size); + begin + Result := Shift_Add (Result, Bits_To_Read, RME_Size, Value_Size - RME_Size); + end; + return Result; + end U64_Extract; + + function U64_Extract_LE + (Buffer : Bytes; + First : Index; + Last : Index; + Off : Offset; + Value_Size : Positive) return U64 + with + Pre => + (First >= Buffer'First + and then Last <= Buffer'Last + and then Value_Size in 1 .. U64'Size + and then Long_Integer ((Natural (Off) + Value_Size - 1) / Byte'Size) < Buffer (First .. Last)'Length), + Post => + (if Value_Size < U64'Size then U64_Extract_LE'Result < 2**Value_Size) + is + Data : constant Bytes := Buffer (First .. Last); + + RME_Index : Index; + LME_Index : Index; + + RME_Offset : constant Natural := Natural (Off); + RME_Size : Natural; + + LME_Size : Natural; + Result : U64 := 0; + + begin + -- This function is identical in structure to the U64_Extract function. + -- See the comments there for more details. However, in little endian we + -- traverse the relevant bytes in the opposite order. + + Get_Index_Offset (Long_Integer (Data'First), Long_Integer (Data'Last), Off, Value_Size, RME_Index, LME_Index, RME_Size, LME_Size); + + declare + Tmp : U64 := Byte'Pos (Data (RME_Index)); + begin + if RME_Index = LME_Index then + Tmp := Mask_Upper (Tmp, LME_Size); + end if; + Tmp := + Right_Shift + (Tmp, + RME_Offset, + (if RME_Index = LME_Index then LME_Size else Byte'Size)); + Result := Result + Tmp; + end; + + if RME_Index = LME_Index then + pragma Assert (Fits_Into (Result, Value_Size)); + return Result; + end if; + + pragma Assert (Fits_Into (Result, RME_Size)); + + for I in reverse LME_Index + 1 .. RME_Index - 1 loop + Result := + Shift_Add + (Result, + Byte'Pos (Data (I)), + Byte'Size, + Natural (RME_Index - I) * Byte'Size - RME_Offset); + pragma Loop_Invariant + (Fits_Into (Result, Natural (RME_Index - I + 1) * Byte'Size - RME_Offset)); + end loop; + + pragma Assert (LME_Size < U64'Size); + pragma Assert (if LME_Index + 1 <= RME_Index - 1 then Fits_Into (Result, Natural (RME_Index - LME_Index) * Byte'Size - RME_Offset)); + pragma Assert (if LME_Index + 1 > RME_Index - 1 then Fits_Into (Result, Natural (RME_Index - LME_Index) * Byte'Size - RME_Offset)); + pragma Assert (Value_Size - LME_Size = Natural (RME_Index - LME_Index) * Byte'Size - RME_Offset); + pragma Assert (Fits_Into (Result, Value_Size - LME_Size)); + Result := + Shift_Add (Result, + Mask_Upper (Byte'Pos (Data (LME_Index)), LME_Size), + LME_Size, + Value_Size - LME_Size); + pragma Assert (Fits_Into (Result, Value_Size)); + return Result; + end U64_Extract_LE; + + procedure U64_Insert + (Val : U64; + Buffer : in out Bytes; + First : Index; + Last : Index; + Off : Offset; + Value_Size : Positive; + BO : Byte_Order) + with + Pre => + First >= Buffer'First + and then Last <= Buffer'Last + and then Value_Size <= U64'Size + and then (if Value_Size < U64'Size then Val < 2**Value_Size) + and then Long_Integer (Natural (Off) + Value_Size - 1) / Byte'Size < Buffer (First .. Last)'Length, + Post => + Buffer'First = Buffer'Old'First and Buffer'Last = Buffer'Old'Last + is + RME_Index : Index; + LME_Index : Index; + + RME_Offset : constant Natural := Natural (Off); + RME_Size : Natural; + + LME_Size : Natural; + + RV : U64; + begin + Get_Index_Offset (Long_Integer (First), Long_Integer (Last), Off, Value_Size, RME_Index, LME_Index, RME_Size, LME_Size); + + if RME_Index = LME_Index then + declare + D : constant U64 := Byte'Pos (Buffer (RME_Index)); + pragma Assert (Fits_Into (D, Byte'Size)); + L_Bits : constant U64 := Mask_Lower (D, RME_Offset + Value_Size, Byte'Size); + R_Bits : constant U64 := Mask_Upper (D, RME_Offset); + Bits_To_Add : constant U64 := Left_Shift (Val, RME_Offset, Value_Size); + Result : constant U64 := + Add (L_Bits, Add (Bits_To_Add, R_Bits, RME_Offset + Value_Size, RME_Offset), Byte'Size, RME_Offset + Value_Size); + begin + Buffer (RME_Index) := Byte'Val (Result); + end; + + else + case BO is + when Low_Order_First => + declare + L_Bits : constant U64 := Mask_Lower (Byte'Pos (Buffer (LME_Index)), LME_Size, Byte'Size); + V_Bits : constant U64 := Mask_Upper (Val, LME_Size); + begin + Buffer (LME_Index) := Byte'Val (Add (L_Bits, V_Bits, Byte'Size, LME_Size)); + end; + RV := Right_Shift (Val, LME_Size, Value_Size); + pragma Assert (Fits_Into (RV, Value_Size - LME_Size)); + + for I in LME_Index + 1 .. RME_Index - 1 + loop + Buffer (I) := Byte'Val (RV mod 2**Byte'Size); + RV := Right_Shift (RV, Byte'Size, Value_Size - LME_Size - Natural (I - LME_Index - 1) * Byte'Size); + pragma Loop_Invariant (Fits_Into (RV, Value_Size - LME_Size - Natural (I - LME_Index) * Byte'Size)); + end loop; + + pragma Assert (RME_Size = Value_Size - LME_Size - Natural (RME_Index - LME_Index - 1) * Byte'Size); + pragma Assert (Fits_Into (RV, RME_Size)); + declare + U_Value : constant U64 := Mask_Upper (Byte'Pos (Buffer (RME_Index)), RME_Offset); + R_Value : constant U64 := Left_Shift (RV, RME_Offset, RME_Size); + begin + Buffer (RME_Index) := Byte'Val (Add (R_Value, U_Value, Byte'Size, RME_Offset)); + end; + when High_Order_First => + pragma Assert (LME_Size = Value_Size - RME_Size - Natural (RME_Index - LME_Index - 1) * Byte'Size); + declare + L_Bits : constant U64 := Mask_Upper (Byte'Pos (Buffer (RME_Index)), RME_Offset); + V_Bits : constant U64 := Mask_Upper (Val, RME_Size); + V_Value : constant U64 := Left_Shift (V_Bits, RME_Offset, RME_Size); + begin + Buffer (RME_Index) := Byte'Val (L_Bits + V_Value); + RV := Right_Shift (Val, RME_Size, Value_Size); + end; + + pragma Assert (RME_Size < Value_Size); + pragma Assert (Fits_Into (RV, Value_Size - RME_Size)); + + for I in reverse LME_Index + 1 .. RME_Index - 1 + loop + Buffer (I) := Byte'Val (RV mod 2**Byte'Size); + RV := Right_Shift (RV, Byte'Size, Value_Size - RME_Size - Natural (RME_Index - I - 1) * Byte'Size); + pragma Loop_Invariant (Fits_Into (RV, Value_Size - RME_Size - Natural (RME_Index - I) * Byte'Size)); + end loop; + + pragma Assert (LME_Size = Value_Size - RME_Size - Natural (RME_Index - LME_Index - 1) * Byte'Size); + pragma Assert (Fits_Into (RV, LME_Size)); + declare + U_Value : constant U64 := Mask_Lower (Byte'Pos (Buffer (LME_Index)), LME_Size, Byte'Size); + Sum : U64; + begin + Sum := Add (U_Value, RV, Byte'Size, LME_Size); + Buffer (LME_Index) := Byte'Val (Sum); + end; + end case; + end if; + end U64_Insert; + + function Extract + (Buffer : Bytes; + First : Index; + Last : Index; + Off : Offset; + Size : Positive; + BO : Byte_Order) return U64 + is + begin + if BO = High_Order_First then + return U64_Extract (Buffer, First, Last, Off, Size); + else + return U64_Extract_LE (Buffer, First, Last, Off, Size); + end if; + end Extract; + + function Extract + (Buffer : Bytes; + First : Index; + Last : Index; + Off : Offset; + Size : Positive; + BO : Byte_Order) return Base_Integer + is + begin + return Base_Integer (U64'(Extract (Buffer, First, Last, Off, Size, BO))); + end Extract; + + procedure Insert + (Val : U64; + Buffer : in out Bytes; + First : Index; + Last : Index; + Off : Offset; + Size : Positive; + BO : Byte_Order) + is + begin + U64_Insert (Val, Buffer, First, Last, Off, Size, BO); + end Insert; + + procedure Insert + (Val : Base_Integer; + Buffer : in out Bytes; + First : Index; + Last : Index; + Off : Offset; + Size : Positive; + BO : Byte_Order) + is + begin + Lemma_Size (Val, Size); + Insert (U64 (Val), Buffer, First, Last, Off, Size, BO); + end Insert; + +end RFLX.RFLX_Generic_Types.Generic_Operations; diff --git a/tests/data/generator/generated/boolean_variable/rflx-rflx_generic_types-generic_operations.ads b/tests/data/generator/generated/boolean_variable/rflx-rflx_generic_types-generic_operations.ads new file mode 100644 index 000000000..e82f1e9e6 --- /dev/null +++ b/tests/data/generator/generated/boolean_variable/rflx-rflx_generic_types-generic_operations.ads @@ -0,0 +1,106 @@ +------------------------------------------------------------------------------ +-- -- +-- Generated by RecordFlux -- +-- -- +-- Copyright (C) AdaCore GmbH -- +-- -- +-- SPDX-License-Identifier: Apache-2.0 -- +-- -- +------------------------------------------------------------------------------ + +pragma Style_Checks ("N3aAbCdefhiIklnOprStux"); +pragma Warnings (Off, """Always_Terminates"" is not a valid aspect identifier"); + +with RFLX.RFLX_Generic_Types.Generic_Operators; + +generic + with package Operators is new RFLX.RFLX_Generic_Types.Generic_Operators (<>); +package RFLX.RFLX_Generic_Types.Generic_Operations with + SPARK_Mode, + Always_Terminates +is + use Operators; + + use type U64; + + function Extract + (Buffer : Bytes; + First : Index; + Last : Index; + Off : Offset; + Size : Positive; + BO : Byte_Order) return U64 + with + Pre => + (First >= Buffer'First + and then Last <= Buffer'Last + and then Size in 1 .. U64'Size + and then First <= Last + and then Last - First <= Index'Last - 1 + and then Length ((Offset'Pos (Off) + Size - 1) / Byte'Size) < Length (Last - First + 1) + and then (Offset'Pos (Off) + Size - 1) / Byte'Size <= Natural'Size + and then (Byte'Size - Natural (Offset'Pos (Off) mod Byte'Size)) < Long_Integer'Size - 1), + Post => + (if Size < U64'Size then Extract'Result < 2**Size); + + function Extract + (Buffer : Bytes; + First : Index; + Last : Index; + Off : Offset; + Size : Positive; + BO : Byte_Order) return Base_Integer + with + Pre => + (First >= Buffer'First + and then Last <= Buffer'Last + and then Size in 1 .. 63 + and then First <= Last + and then Last - First <= Index'Last - 1 + and then Length ((Offset'Pos (Off) + Size - 1) / Byte'Size) < Length (Last - First + 1) + and then (Offset'Pos (Off) + Size - 1) / Byte'Size <= Natural'Size + and then (Byte'Size - Natural (Offset'Pos (Off) mod Byte'Size)) < Long_Integer'Size - 1), + Post => + (U64 (Extract'Result) < 2**Size); + + procedure Insert + (Val : U64; + Buffer : in out Bytes; + First : Index; + Last : Index; + Off : Offset; + Size : Positive; + BO : Byte_Order) + with + Pre => + (First >= Buffer'First + and then Last <= Buffer'Last + and then Size in 1 .. U64'Size + and then Fits_Into (Val, Size) + and then First <= Last + and then Last - First <= Index'Last - 1 + and then Length ((Offset'Pos (Off) + Size - 1) / Byte'Size) < Length (Last - First + 1)), + Post => + (Buffer'First = Buffer'Old'First and Buffer'Last = Buffer'Old'Last); + + procedure Insert + (Val : Base_Integer; + Buffer : in out Bytes; + First : Index; + Last : Index; + Off : Offset; + Size : Positive; + BO : Byte_Order) + with + Pre => + (First >= Buffer'First + and then Last <= Buffer'Last + and then Size in 1 .. 63 + and then Fits_Into (Val, Size) + and then First <= Last + and then Last - First <= Index'Last - 1 + and then Length ((Offset'Pos (Off) + Size - 1) / Byte'Size) < Length (Last - First + 1)), + Post => + (Buffer'First = Buffer'Old'First and Buffer'Last = Buffer'Old'Last); + +end RFLX.RFLX_Generic_Types.Generic_Operations; diff --git a/tests/data/generator/generated/boolean_variable/rflx-rflx_generic_types-generic_operators.ads b/tests/data/generator/generated/boolean_variable/rflx-rflx_generic_types-generic_operators.ads new file mode 100644 index 000000000..7e178d4a0 --- /dev/null +++ b/tests/data/generator/generated/boolean_variable/rflx-rflx_generic_types-generic_operators.ads @@ -0,0 +1,39 @@ +------------------------------------------------------------------------------ +-- -- +-- Generated by RecordFlux -- +-- -- +-- Copyright (C) AdaCore GmbH -- +-- -- +-- SPDX-License-Identifier: Apache-2.0 -- +-- -- +------------------------------------------------------------------------------ + +pragma Style_Checks ("N3aAbCdefhiIklnOprStux"); +pragma Warnings (Off, """Always_Terminates"" is not a valid aspect identifier"); + +generic +package RFLX.RFLX_Generic_Types.Generic_Operators with + SPARK_Mode, + Always_Terminates +is + + function "+" (Left : Index; Right : Length) return Index is + (Index (Length (Left) + Right)) + with + Pre => + Length (Left) <= Length'Last - Right; + + function "-" (Left : Index; Right : Index) return Length is + (Length (Left) - Length (Right)) + with + Pre => + Length (Left) >= Length'First + Length (Right); + + function "-" (Left : Index; Right : Length) return Index is + (Index (Length (Left) - Right)) + with + Pre => + Right < Length'Last + and then Length (Left) >= Length (Index'First) + Right; + +end RFLX.RFLX_Generic_Types.Generic_Operators; diff --git a/tests/data/generator/generated/boolean_variable/rflx-rflx_generic_types.ads b/tests/data/generator/generated/boolean_variable/rflx-rflx_generic_types.ads new file mode 100644 index 000000000..c5e6f108f --- /dev/null +++ b/tests/data/generator/generated/boolean_variable/rflx-rflx_generic_types.ads @@ -0,0 +1,107 @@ +------------------------------------------------------------------------------ +-- -- +-- Generated by RecordFlux -- +-- -- +-- Copyright (C) AdaCore GmbH -- +-- -- +-- SPDX-License-Identifier: Apache-2.0 -- +-- -- +------------------------------------------------------------------------------ + +pragma Style_Checks ("N3aAbCdefhiIklnOprStux"); +pragma Warnings (Off, """Always_Terminates"" is not a valid aspect identifier"); + +with Ada.Unchecked_Deallocation; +with RFLX.RFLX_Arithmetic; + +generic + type Custom_Index is range <>; + type Custom_Byte is (<>); + type Custom_Bytes is array (Custom_Index range <>) of Custom_Byte; + type Custom_Bytes_Ptr is access Custom_Bytes; + type Custom_Length is range <>; + type Custom_Bit_Length is range <>; +package RFLX.RFLX_Generic_Types with + SPARK_Mode, + Always_Terminates +is + + subtype Index is Custom_Index; + + subtype Byte is Custom_Byte; + + subtype Bytes is Custom_Bytes; + + subtype Bytes_Ptr is Custom_Bytes_Ptr; + + subtype Length is Custom_Length; + + subtype Bit_Length is Custom_Bit_Length; + + function "+" (Left : Index; Right : Index) return Index is abstract; + + function "-" (Left : Index; Right : Index) return Index is abstract; + + pragma Compile_Time_Error (Index'First /= 1, "Index'First must be 1"); + + pragma Compile_Time_Error (Byte'Size /= 8, "Byte must be of size 8"); + + pragma Compile_Time_Error (Byte'Pos (Byte'Last) - Byte'Pos (Byte'First) + 1 /= 2**Byte'Size, + "Byte must cover entire value range"); + + pragma Compile_Time_Error (Length'First /= 0, "Length'First must be 0"); + + pragma Compile_Time_Error (Length'Pos (Length'Last) /= Index'Pos (Index'Last), + "Length'Last must be equal to Index'Last"); + + pragma Compile_Time_Error (Bit_Length'First /= 0, "Bit_Length'First must be 0"); + + pragma Compile_Time_Error (Bit_Length'Pos (Bit_Length'Last) /= Length'Pos (Length'Last) * 8, + "Bit_Length'Last must be equal to Length'Last * 8"); + + subtype U64 is RFLX.RFLX_Arithmetic.U64; + + subtype Base_Integer is RFLX.RFLX_Arithmetic.Base_Integer; + + subtype Bit_Index is Bit_Length range 1 .. Bit_Length'Last; + + function To_Index (Bit_Idx : Bit_Length) return Index is + (Index (Length ((Bit_Idx - 1) / 8) + 1)); + + function To_Length (Bit_Len : Bit_Length) return Length is + (Length ((Bit_Len + 7) / 8)); + + function To_Bit_Length (Len : Length) return Bit_Length is + (Bit_Length (Len) * 8); + + function To_First_Bit_Index (Idx : Index) return Bit_Index is + ((Bit_Length (Idx) - 1) * 8 + 1); + + function To_Last_Bit_Index (Idx : Index) return Bit_Index is + ((Bit_Length (Idx) - 1) * 8 + 8); + + function To_Last_Bit_Index (Idx : Length) return Bit_Length is + ((Bit_Length (Idx) - 1) * 8 + 8); + + function Fits_Into (V : U64; Bits : Natural) return Boolean renames RFLX_Arithmetic.Fits_Into; + function Fits_Into (V : Base_Integer; Bits : Natural) return Boolean renames RFLX_Arithmetic.Fits_Into; + + type Offset is mod 8; + + type Byte_Order is (High_Order_First, Low_Order_First); + + pragma Warnings (Off, "precondition is always False"); + + function Unreachable return Boolean is (False) with Pre => False; + + function Unreachable return Bit_Length is (0) with Pre => False; + + function Unreachable return Length is (0) with Pre => False; + + pragma Warnings (On, "precondition is always False"); + + procedure Lemma_Size (Val : Base_Integer; Size : Positive) renames RFLX.RFLX_Arithmetic.Lemma_Size; + + procedure Free is new Ada.Unchecked_Deallocation (Object => Bytes, Name => Bytes_Ptr); + +end RFLX.RFLX_Generic_Types; diff --git a/tests/data/generator/generated/boolean_variable/rflx-rflx_message_sequence.adb b/tests/data/generator/generated/boolean_variable/rflx-rflx_message_sequence.adb new file mode 100644 index 000000000..0ce6332bf --- /dev/null +++ b/tests/data/generator/generated/boolean_variable/rflx-rflx_message_sequence.adb @@ -0,0 +1,93 @@ +------------------------------------------------------------------------------ +-- -- +-- Generated by RecordFlux -- +-- -- +-- Copyright (C) AdaCore GmbH -- +-- -- +-- SPDX-License-Identifier: Apache-2.0 -- +-- -- +------------------------------------------------------------------------------ + +pragma Style_Checks ("N3aAbCdefhiIklnOprStux"); + +package body RFLX.RFLX_Message_Sequence with + SPARK_Mode +is + + procedure Initialize (Ctx : out Context; Buffer : in out RFLX_Types.Bytes_Ptr) is + begin + Initialize (Ctx, Buffer, RFLX_Types.To_First_Bit_Index (Buffer'First), RFLX_Types.To_Last_Bit_Index (Buffer'Last)); + end Initialize; + + procedure Initialize (Ctx : out Context; Buffer : in out RFLX_Types.Bytes_Ptr; First : RFLX_Types.Bit_Index; Last : RFLX_Types.Bit_Length) + is + Buffer_First : constant RFLX_Types.Index := Buffer'First; + Buffer_Last : constant RFLX_Types.Index := Buffer'Last; + begin + Ctx := (Buffer_First => Buffer_First, Buffer_Last => Buffer_Last, First => First, Last => Last, Buffer => Buffer, Sequence_Last => First - 1, State => S_Valid); + Buffer := null; + end Initialize; + + procedure Reset (Ctx : in out Context) is + begin + Ctx.Sequence_Last := Ctx.First - 1; + Ctx.State := S_Valid; + end Reset; + + procedure Take_Buffer (Ctx : in out Context; Buffer : out RFLX_Types.Bytes_Ptr) is + begin + Buffer := Ctx.Buffer; + Ctx.Buffer := null; + end Take_Buffer; + + procedure Copy (Ctx : Context; Buffer : out RFLX_Types.Bytes) is + begin + if Buffer'Length > 0 then + Buffer := Ctx.Buffer.all (RFLX_Types.To_Index (Ctx.First) .. RFLX_Types.To_Index (Ctx.Sequence_Last)); + else + Buffer := Ctx.Buffer.all (RFLX_Types.Index'Last .. RFLX_Types.Index'First); + end if; + end Copy; + + procedure Append_Element (Ctx : in out Context; Element_Ctx : Element_Context) is + begin + Element_Copy (Element_Ctx, Ctx.Buffer.all (RFLX_Types.To_Index (Ctx.Sequence_Last + 1) .. RFLX_Types.To_Index (Ctx.Sequence_Last + Element_Size (Element_Ctx)))); + Ctx.Sequence_Last := Ctx.Sequence_Last + Element_Size (Element_Ctx); + end Append_Element; + + procedure Switch (Ctx : in out Context; Element_Ctx : out Element_Context) is + Buffer : RFLX_Types.Bytes_Ptr := Ctx.Buffer; + begin + Ctx.Buffer := null; + pragma Warnings (Off, "unused assignment to ""Buffer"""); + Element_Initialize (Element_Ctx, Buffer, Ctx.Sequence_Last + 1, Ctx.Last, Ctx.Last); + pragma Warnings (On, "unused assignment to ""Buffer"""); + end Switch; + + procedure Update (Ctx : in out Context; Element_Ctx : in out Element_Context) is + Buffer : RFLX_Types.Bytes_Ptr; + Valid_Message : constant Boolean := Element_Valid_Message (Element_Ctx); + Last : RFLX_Types.Bit_Length := RFLX_Types.Bit_Length'First; + begin + if Valid_Message then + Last := Element_Last (Element_Ctx); + end if; + Element_Take_Buffer (Element_Ctx, Buffer); + Ctx.Buffer := Buffer; + if Valid_Message then + Ctx.Sequence_Last := Last; + else + Ctx.State := S_Invalid; + end if; + end Update; + + procedure Data (Ctx : Context; Data : out RFLX_Types.Bytes) is + begin + if Data'Length > 0 then + Data := Ctx.Buffer.all (RFLX_Types.To_Index (Ctx.First) .. RFLX_Types.To_Index (Ctx.Sequence_Last)); + else + Data := Ctx.Buffer.all (1 .. 0); + end if; + end Data; + +end RFLX.RFLX_Message_Sequence; diff --git a/tests/data/generator/generated/boolean_variable/rflx-rflx_message_sequence.ads b/tests/data/generator/generated/boolean_variable/rflx-rflx_message_sequence.ads new file mode 100644 index 000000000..e1abdc20c --- /dev/null +++ b/tests/data/generator/generated/boolean_variable/rflx-rflx_message_sequence.ads @@ -0,0 +1,267 @@ +------------------------------------------------------------------------------ +-- -- +-- Generated by RecordFlux -- +-- -- +-- Copyright (C) AdaCore GmbH -- +-- -- +-- SPDX-License-Identifier: Apache-2.0 -- +-- -- +------------------------------------------------------------------------------ + +pragma Style_Checks ("N3aAbCdefhiIklnOprStux"); +pragma Warnings (Off, """Always_Terminates"" is not a valid aspect identifier"); +with RFLX.RFLX_Types; + +generic + type Element_Context (Buffer_First, Buffer_Last : RFLX_Types.Index; First : RFLX_Types.Bit_Index; Last : RFLX_Types.Bit_Length) is private; + with procedure Element_Initialize (Ctx : out Element_Context; Buffer : in out RFLX_Types.Bytes_Ptr; First : RFLX_Types.Bit_Index; Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length := 0); + with procedure Element_Take_Buffer (Ctx : in out Element_Context; Buffer : out RFLX_Types.Bytes_Ptr); + with procedure Element_Copy (Ctx : Element_Context; Buffer : out RFLX_Types.Bytes); + with function Element_Has_Buffer (Ctx : Element_Context) return Boolean; + with function Element_Size (Ctx : Element_Context) return RFLX_Types.Bit_Length; + with function Element_Last (Ctx : Element_Context) return RFLX_Types.Bit_Index; + with function Element_Initialized (Ctx : Element_Context) return Boolean; + with function Element_Valid_Message (Ctx : Element_Context) return Boolean; +package RFLX.RFLX_Message_Sequence with + SPARK_Mode, + Always_Terminates +is + + pragma Unevaluated_Use_Of_Old (Allow); + + pragma Warnings (Off, """LENGTH"" is already use-visible through previous use_type_clause"); + + use type RFLX_Types.Bytes_Ptr, RFLX_Types.Index, RFLX_Types.Length, RFLX_Types.Bit_Index; + + pragma Warnings (On, """LENGTH"" is already use-visible through previous use_type_clause"); + + type Context (Buffer_First, Buffer_Last : RFLX_Types.Index := RFLX_Types.Index'First; First : RFLX_Types.Bit_Index := RFLX_Types.Bit_Index'First; Last : RFLX_Types.Bit_Length := RFLX_Types.Bit_Length'First) is private with + Default_Initial_Condition => + RFLX_Types.To_Index (First) >= Buffer_First + and RFLX_Types.To_Index (Last) <= Buffer_Last + and Buffer_Last < RFLX_Types.Index'Last + and First <= Last + 1 + and Last <= RFLX_Types.Bit_Length'Last - 1 + and First mod RFLX_Types.Byte'Size = 1 + and Last mod RFLX_Types.Byte'Size = 0; + + procedure Initialize (Ctx : out Context; Buffer : in out RFLX_Types.Bytes_Ptr) with + Pre => + (not Ctx'Constrained + and then Buffer /= null + and then Buffer'Length > 0 + and then Buffer'Last < RFLX_Types.Index'Last), + Post => + (Has_Buffer (Ctx) + and Valid (Ctx) + and Buffer = null + and Ctx.Buffer_First = Buffer'First'Old + and Ctx.Buffer_Last = Buffer'Last'Old + and Ctx.First = RFLX_Types.To_First_Bit_Index (Ctx.Buffer_First) + and Ctx.Last = RFLX_Types.To_Last_Bit_Index (Ctx.Buffer_Last) + and Sequence_Last (Ctx) = Ctx.First - 1), + Depends => + (Ctx => Buffer, Buffer => null); + + procedure Initialize (Ctx : out Context; Buffer : in out RFLX_Types.Bytes_Ptr; First : RFLX_Types.Bit_Index; Last : RFLX_Types.Bit_Length) with + Pre => + (not Ctx'Constrained + and then Buffer /= null + and then Buffer'Length > 0 + and then Buffer'Last < RFLX_Types.Index'Last + and then RFLX_Types.To_Index (First) >= Buffer'First + and then RFLX_Types.To_Index (Last) <= Buffer'Last + and then First <= Last + 1 + and then Last <= RFLX_Types.Bit_Length'Last - 1 + and then First mod RFLX_Types.Byte'Size = 1 + and then Last mod RFLX_Types.Byte'Size = 0), + Post => + (Buffer = null + and Has_Buffer (Ctx) + and Valid (Ctx) + and Ctx.Buffer_First = Buffer'First'Old + and Ctx.Buffer_Last = Buffer'Last'Old + and Ctx.First = First + and Ctx.Last = Last + and Sequence_Last (Ctx) = First - 1), + Depends => + (Ctx => (Buffer, First, Last), Buffer => null); + + procedure Reset (Ctx : in out Context) with + Pre => + Has_Buffer (Ctx), + Post => + (Has_Buffer (Ctx) + and Valid (Ctx) + and Ctx.Buffer_First = Ctx.Buffer_First'Old + and Ctx.Buffer_Last = Ctx.Buffer_Last'Old + and Ctx.First = Ctx.First'Old + and Ctx.Last = Ctx.Last'Old + and Sequence_Last (Ctx) = Ctx.First - 1); + + procedure Take_Buffer (Ctx : in out Context; Buffer : out RFLX_Types.Bytes_Ptr) with + Pre => + Has_Buffer (Ctx), + Post => + (not Has_Buffer (Ctx) + and Buffer /= null + and Buffer'First = Ctx.Buffer_First + and Buffer'Last = Ctx.Buffer_Last + and Ctx.Buffer_First = Ctx.Buffer_First'Old + and Ctx.Buffer_Last = Ctx.Buffer_Last'Old + and Ctx.First = Ctx.First'Old + and Ctx.Last = Ctx.Last'Old + and Valid (Ctx) = Valid (Ctx)'Old + and Sequence_Last (Ctx) = Sequence_Last (Ctx)'Old), + Depends => + (Ctx => Ctx, Buffer => Ctx); + + procedure Copy (Ctx : Context; Buffer : out RFLX_Types.Bytes) with + Pre => + (Has_Buffer (Ctx) + and Valid (Ctx) + and Byte_Size (Ctx) = Buffer'Length); + + function Has_Element (Ctx : Context) return Boolean; + + procedure Append_Element (Ctx : in out Context; Element_Ctx : Element_Context) with + Pre => + (Has_Buffer (Ctx) + and then Valid (Ctx) + and then Element_Has_Buffer (Element_Ctx) + and then Element_Valid_Message (Element_Ctx) + and then Element_Size (Element_Ctx) > 0 + and then Available_Space (Ctx) >= Element_Size (Element_Ctx)), + Post => + (Has_Buffer (Ctx) + and Valid (Ctx) + and Sequence_Last (Ctx) = Sequence_Last (Ctx)'Old + Element_Size (Element_Ctx) + and Ctx.Buffer_First = Ctx.Buffer_First'Old + and Ctx.Buffer_Last = Ctx.Buffer_Last'Old + and Ctx.First = Ctx.First'Old + and Ctx.Last = Ctx.Last'Old); + + procedure Switch (Ctx : in out Context; Element_Ctx : out Element_Context) with + Pre => + (not Element_Ctx'Constrained + and then Has_Buffer (Ctx) + and then Has_Element (Ctx) + and then Valid (Ctx)), + Post => + (not Has_Buffer (Ctx) + and Has_Element (Ctx) + and Valid (Ctx) + and Element_Has_Buffer (Element_Ctx) + and Ctx.Buffer_First = Element_Ctx.Buffer_First + and Ctx.Buffer_Last = Element_Ctx.Buffer_Last + and Ctx.First <= Element_Ctx.First + and Ctx.Last >= Element_Ctx.Last + and Element_Ctx.First = Sequence_Last (Ctx) + 1 + and Element_Ctx.Last = Ctx.Last + and Element_Initialized (Element_Ctx) + and Ctx.Buffer_First = Ctx.Buffer_First'Old + and Ctx.Buffer_Last = Ctx.Buffer_Last'Old + and Ctx.First = Ctx.First'Old + and Ctx.Last = Ctx.Last'Old + and Sequence_Last (Ctx) = Sequence_Last (Ctx)'Old), + Depends => + (Ctx => Ctx, Element_Ctx => Ctx); + + procedure Update (Ctx : in out Context; Element_Ctx : in out Element_Context) with + Pre => + (not Has_Buffer (Ctx) + and then Element_Has_Buffer (Element_Ctx) + and then Has_Element (Ctx) + and then Valid (Ctx) + and then Ctx.Buffer_First = Element_Ctx.Buffer_First + and then Ctx.Buffer_Last = Element_Ctx.Buffer_Last + and then Ctx.First <= Element_Ctx.First + and then Ctx.Last >= Element_Ctx.Last), + Post => + (Has_Buffer (Ctx) + and not Element_Has_Buffer (Element_Ctx) + and (if Element_Valid_Message (Element_Ctx)'Old then Valid (Ctx)) + and Sequence_Last (Ctx) = RFLX_Types.Bit_Length'(if Element_Valid_Message (Element_Ctx) then Element_Last (Element_Ctx) else Sequence_Last (Ctx))'Old + and Ctx.Buffer_First = Ctx.Buffer_First'Old + and Ctx.Buffer_Last = Ctx.Buffer_Last'Old + and Ctx.First = Ctx.First'Old + and Ctx.Last = Ctx.Last'Old), + Contract_Cases => + (Element_Valid_Message (Element_Ctx) => + (Sequence_Last (Ctx) = Element_Last (Element_Ctx)'Old), + others => + True), + Depends => + (Ctx => (Ctx, Element_Ctx), Element_Ctx => Element_Ctx); + + function Valid (Ctx : Context) return Boolean; + + function Has_Buffer (Ctx : Context) return Boolean; + + function Available_Space (Ctx : Context) return RFLX_Types.Bit_Length; + + function Sequence_Last (Ctx : Context) return RFLX_Types.Bit_Length; + + function Size (Ctx : Context) return RFLX_Types.Bit_Length; + + function Byte_Size (Ctx : Context) return RFLX_Types.Length; + + procedure Data (Ctx : Context; Data : out RFLX_Types.Bytes) with + Pre => + (Has_Buffer (Ctx) + and then Valid (Ctx) + and then Data'Length = Byte_Size (Ctx)); + +private + + pragma Warnings (Off, "use clause for package * has no effect"); + + use RFLX.RFLX_Types; + + pragma Warnings (On, "use clause for package * has no effect"); + + type Context_State is (S_Valid, S_Invalid); + + type Context (Buffer_First, Buffer_Last : RFLX_Types.Index := RFLX_Types.Index'First; First : RFLX_Types.Bit_Index := RFLX_Types.Bit_Index'First; Last : RFLX_Types.Bit_Length := RFLX_Types.Bit_Length'First) is + record + Sequence_Last : RFLX_Types.Bit_Length := First - 1; + Buffer : RFLX_Types.Bytes_Ptr := null; + State : Context_State := S_Valid; + end record with + Dynamic_Predicate => + ((if Buffer /= null then + (Buffer'First = Buffer_First + and Buffer'Last = Buffer_Last)) + and RFLX_Types.To_Index (First) >= Buffer_First + and RFLX_Types.To_Index (Last) <= Buffer_Last + and Buffer_Last < RFLX_Types.Index'Last + and First <= Last + 1 + and Last <= RFLX_Types.Bit_Length'Last - 1 + and First - 1 <= Sequence_Last + and Sequence_Last <= Last + and First mod RFLX_Types.Byte'Size = 1 + and Last mod RFLX_Types.Byte'Size = 0 + and Sequence_Last mod RFLX_Types.Byte'Size = 0); + + function Has_Element (Ctx : Context) return Boolean is + (Ctx.State = S_Valid and Ctx.Sequence_Last < Ctx.Last); + + function Valid (Ctx : Context) return Boolean is + (Ctx.State = S_Valid); + + function Has_Buffer (Ctx : Context) return Boolean is + (Ctx.Buffer /= null); + + function Available_Space (Ctx : Context) return RFLX_Types.Bit_Length is + (Ctx.Last - Ctx.Sequence_Last); + + function Sequence_Last (Ctx : Context) return RFLX_Types.Bit_Length is + (Ctx.Sequence_Last); + + function Size (Ctx : Context) return RFLX_Types.Bit_Length is + (Ctx.Sequence_Last - Ctx.First + 1); + + function Byte_Size (Ctx : Context) return RFLX_Types.Length is + (RFLX_Types.To_Length (Size (Ctx))); + +end RFLX.RFLX_Message_Sequence; diff --git a/tests/data/generator/generated/boolean_variable/rflx-rflx_scalar_sequence.adb b/tests/data/generator/generated/boolean_variable/rflx-rflx_scalar_sequence.adb new file mode 100644 index 000000000..33d8b2c86 --- /dev/null +++ b/tests/data/generator/generated/boolean_variable/rflx-rflx_scalar_sequence.adb @@ -0,0 +1,106 @@ +------------------------------------------------------------------------------ +-- -- +-- Generated by RecordFlux -- +-- -- +-- Copyright (C) AdaCore GmbH -- +-- -- +-- SPDX-License-Identifier: Apache-2.0 -- +-- -- +------------------------------------------------------------------------------ + +pragma Style_Checks ("N3aAbCdefhiIklnOprStux"); +with RFLX.RFLX_Types.Operations; + +package body RFLX.RFLX_Scalar_Sequence with + SPARK_Mode +is + + procedure Initialize (Ctx : out Context; Buffer : in out RFLX_Types.Bytes_Ptr) is + begin + Initialize (Ctx, Buffer, RFLX_Types.To_First_Bit_Index (Buffer'First), RFLX_Types.To_Last_Bit_Index (Buffer'Last)); + end Initialize; + + procedure Initialize (Ctx : out Context; Buffer : in out RFLX_Types.Bytes_Ptr; First : RFLX_Types.Bit_Index; Last : RFLX_Types.Bit_Length) + is + Buffer_First : constant RFLX_Types.Index := Buffer'First; + Buffer_Last : constant RFLX_Types.Index := Buffer'Last; + begin + Ctx := (Buffer_First => Buffer_First, Buffer_Last => Buffer_Last, First => First, Last => Last, Buffer => Buffer, Sequence_Last => First - 1, State => S_Valid, First_Element => RFLX.RFLX_Types.Base_Integer'First, Next_Element => RFLX.RFLX_Types.Base_Integer'First); + Buffer := null; + end Initialize; + + procedure Reset (Ctx : in out Context) is + begin + Ctx.Sequence_Last := Ctx.First - 1; + Ctx.State := S_Valid; + end Reset; + + procedure Take_Buffer (Ctx : in out Context; Buffer : out RFLX_Types.Bytes_Ptr) is + begin + Buffer := Ctx.Buffer; + Ctx.Buffer := null; + end Take_Buffer; + + procedure Copy (Ctx : Context; Buffer : out RFLX_Types.Bytes) is + begin + if Buffer'Length > 0 then + Buffer := Ctx.Buffer.all (RFLX_Types.To_Index (Ctx.First) .. RFLX_Types.To_Index (Ctx.Sequence_Last)); + else + Buffer := Ctx.Buffer.all (RFLX_Types.Index'Last .. RFLX_Types.Index'First); + end if; + end Copy; + + procedure Next (Ctx : in out Context) is + Last_Bit : constant RFLX_Types.Bit_Index := Ctx.Sequence_Last + RFLX.RFLX_Types.Bit_Index (Element_Size); + Buffer_First : constant RFLX_Types.Index := RFLX_Types.To_Index (Ctx.Sequence_Last + 1); + Buffer_Last : constant RFLX_Types.Index := RFLX_Types.To_Index (Last_Bit); + Offset : constant RFLX_Types.Offset := RFLX_Types.Offset ((8 - (Last_Bit mod 8)) mod 8); + begin + if Buffer_First >= Ctx.Buffer'First and Buffer_Last <= Ctx.Buffer'Last and Buffer_First <= Buffer_Last then + Ctx.Next_Element := RFLX.RFLX_Types.Operations.Extract (Ctx.Buffer.all, Buffer_First, Buffer_Last, Offset, Element_Size, RFLX_Types.High_Order_First); + if Valid_Element (Ctx) then + if Size (Ctx) = 0 then + Ctx.First_Element := Ctx.Next_Element; + end if; + else + Ctx.State := S_Invalid; + end if; + end if; + Ctx.Sequence_Last := Ctx.Sequence_Last + RFLX.RFLX_Types.Bit_Index (Element_Size); + end Next; + + function Get_Element (Ctx : Context) return Element_Type is + (To_Actual (Ctx.Next_Element)); + + function Head (Ctx : Context) return Element_Type is + (To_Actual (Ctx.First_Element)); + + procedure Append_Element (Ctx : in out Context; Value : Element_Type) is + Last_Bit : RFLX_Types.Bit_Index; + First : RFLX_Types.Index; + Last : RFLX_Types.Index; + Offset : RFLX_Types.Offset; + begin + Last_Bit := Ctx.Sequence_Last + RFLX.RFLX_Types.Bit_Index (Element_Size); + First := RFLX_Types.To_Index (Ctx.Sequence_Last + 1); + Last := RFLX_Types.To_Index (Last_Bit); + Offset := RFLX_Types.Offset ((8 - (Last_Bit mod 8)) mod 8); + if First >= Ctx.Buffer'First and Last <= Ctx.Buffer'Last and First <= Last then + RFLX.RFLX_Types.Operations.Insert (To_Base_Int (Value), Ctx.Buffer.all, First, Last, Offset, Element_Size, RFLX_Types.High_Order_First); + end if; + if Size (Ctx) = 0 then + Ctx.First_Element := To_Base_Int (Value); + end if; + Ctx.Sequence_Last := Ctx.Sequence_Last + RFLX.RFLX_Types.Bit_Index (Element_Size); + end Append_Element; + + procedure Data (Ctx : Context; Data : out RFLX_Types.Bytes) is + begin + if Data'Length > 0 then + Data := Ctx.Buffer.all (RFLX_Types.To_Index (Ctx.First) .. RFLX_Types.To_Index (Ctx.Sequence_Last)); + else + Data := Ctx.Buffer.all (1 .. 0); + end if; + end Data; + +end RFLX.RFLX_Scalar_Sequence; diff --git a/tests/data/generator/generated/boolean_variable/rflx-rflx_scalar_sequence.ads b/tests/data/generator/generated/boolean_variable/rflx-rflx_scalar_sequence.ads new file mode 100644 index 000000000..1a3af3abf --- /dev/null +++ b/tests/data/generator/generated/boolean_variable/rflx-rflx_scalar_sequence.ads @@ -0,0 +1,240 @@ +------------------------------------------------------------------------------ +-- -- +-- Generated by RecordFlux -- +-- -- +-- Copyright (C) AdaCore GmbH -- +-- -- +-- SPDX-License-Identifier: Apache-2.0 -- +-- -- +------------------------------------------------------------------------------ + +pragma Style_Checks ("N3aAbCdefhiIklnOprStux"); +pragma Warnings (Off, """Always_Terminates"" is not a valid aspect identifier"); +with RFLX.RFLX_Types; + +generic + type Element_Type is private; + Element_Size : Positive; + with function Valid (Element : RFLX.RFLX_Types.Base_Integer) return Boolean; + with function To_Actual (Element : RFLX.RFLX_Types.Base_Integer) return Element_Type; + with function To_Base_Int (Element : Element_Type) return RFLX.RFLX_Types.Base_Integer; +package RFLX.RFLX_Scalar_Sequence with + SPARK_Mode, + Always_Terminates +is + + use type RFLX_Types.Bytes_Ptr; + + use type RFLX_Types.Index; + + pragma Warnings (Off, """LENGTH"" is already use-visible through previous use_type_clause"); + + use type RFLX_Types.Length; + + pragma Warnings (On, """LENGTH"" is already use-visible through previous use_type_clause"); + + use type RFLX_Types.Bit_Index; + + use type RFLX_Types.Base_Integer; + + type Context (Buffer_First, Buffer_Last : RFLX_Types.Index := RFLX_Types.Index'First; First : RFLX_Types.Bit_Index := RFLX_Types.Bit_Index'First; Last : RFLX_Types.Bit_Length := RFLX_Types.Bit_Length'First) is private with + Default_Initial_Condition => + RFLX_Types.To_Index (First) >= Buffer_First + and RFLX_Types.To_Index (Last) <= Buffer_Last + and Buffer_Last < RFLX_Types.Index'Last + and First <= Last + 1 + and Last <= RFLX_Types.Bit_Length'Last - 1 + and First mod RFLX_Types.Byte'Size = 1; + + procedure Initialize (Ctx : out Context; Buffer : in out RFLX_Types.Bytes_Ptr) with + Pre => + (not Ctx'Constrained + and then Buffer /= null + and then Buffer'Length > 0 + and then Buffer'Last < RFLX_Types.Index'Last), + Post => + (Has_Buffer (Ctx) + and Valid (Ctx) + and Buffer = null + and Ctx.Buffer_First = Buffer'First'Old + and Ctx.Buffer_Last = Buffer'Last'Old + and Ctx.First = RFLX_Types.To_First_Bit_Index (Ctx.Buffer_First) + and Ctx.Last = RFLX_Types.To_Last_Bit_Index (Ctx.Buffer_Last) + and Sequence_Last (Ctx) = Ctx.First - 1), + Depends => + (Ctx => Buffer, Buffer => null); + + procedure Initialize (Ctx : out Context; Buffer : in out RFLX_Types.Bytes_Ptr; First : RFLX_Types.Bit_Index; Last : RFLX_Types.Bit_Length) with + Pre => + (not Ctx'Constrained + and then Buffer /= null + and then Buffer'Length > 0 + and then Buffer'Last < RFLX_Types.Index'Last + and then RFLX_Types.To_Index (First) >= Buffer'First + and then RFLX_Types.To_Index (Last) <= Buffer'Last + and then First <= Last + 1 + and then Last <= RFLX_Types.Bit_Length'Last - 1 + and then First mod RFLX_Types.Byte'Size = 1), + Post => + (Buffer = null + and Has_Buffer (Ctx) + and Valid (Ctx) + and Ctx.Buffer_First = Buffer'First'Old + and Ctx.Buffer_Last = Buffer'Last'Old + and Ctx.First = First + and Ctx.Last = Last + and Sequence_Last (Ctx) = First - 1), + Depends => + (Ctx => (Buffer, First, Last), Buffer => null); + + procedure Reset (Ctx : in out Context) with + Pre => + Has_Buffer (Ctx), + Post => + (Has_Buffer (Ctx) + and Valid (Ctx) + and Ctx.Buffer_First = Ctx.Buffer_First'Old + and Ctx.Buffer_Last = Ctx.Buffer_Last'Old + and Ctx.First = Ctx.First'Old + and Ctx.Last = Ctx.Last'Old + and Sequence_Last (Ctx) = Ctx.First - 1); + + procedure Take_Buffer (Ctx : in out Context; Buffer : out RFLX_Types.Bytes_Ptr) with + Pre => + Has_Buffer (Ctx), + Post => + (not Has_Buffer (Ctx) + and Buffer /= null + and Buffer'First = Ctx.Buffer_First + and Buffer'Last = Ctx.Buffer_Last + and Ctx.Buffer_First = Ctx.Buffer_First'Old + and Ctx.Buffer_Last = Ctx.Buffer_Last'Old + and Ctx.First = Ctx.First'Old + and Ctx.Last = Ctx.Last'Old + and Valid (Ctx) = Valid (Ctx)'Old + and Sequence_Last (Ctx) = Sequence_Last (Ctx)'Old), + Depends => + (Ctx => Ctx, Buffer => Ctx); + + procedure Copy (Ctx : Context; Buffer : out RFLX_Types.Bytes) with + Pre => + (Has_Buffer (Ctx) + and Valid (Ctx) + and Byte_Size (Ctx) = Buffer'Length); + + procedure Next (Ctx : in out Context) with + Pre => + (Has_Buffer (Ctx) + and then Has_Element (Ctx)), + Post => + (Has_Buffer (Ctx) + and Sequence_Last (Ctx) = Sequence_Last (Ctx)'Old + RFLX.RFLX_Types.Bit_Index (Element_Size) + and Ctx.Buffer_First = Ctx.Buffer_First'Old + and Ctx.Buffer_Last = Ctx.Buffer_Last'Old + and Ctx.First = Ctx.First'Old + and Ctx.Last = Ctx.Last'Old); + + function Has_Element (Ctx : Context) return Boolean; + + function Valid_Element (Ctx : Context) return Boolean; + + function Get_Element (Ctx : Context) return Element_Type with + Pre => + Valid_Element (Ctx); + + function Head (Ctx : Context) return Element_Type with + Pre => + (Valid (Ctx) + and then Sequence_Last (Ctx) >= Ctx.First + RFLX.RFLX_Types.Bit_Index (Element_Size) - 1); + + procedure Append_Element (Ctx : in out Context; Value : Element_Type) with + Pre => + (Has_Buffer (Ctx) + and then Valid (Ctx) + and then Valid (To_Base_Int (Value)) + and then (if Element_Size < 64 then To_Base_Int (Value) < 2**Element_Size) + and then Available_Space (Ctx) >= RFLX.RFLX_Types.Bit_Index (Element_Size)), + Post => + (Has_Buffer (Ctx) + and Valid (Ctx) + and Sequence_Last (Ctx) = Sequence_Last (Ctx)'Old + RFLX.RFLX_Types.Bit_Index (Element_Size) + and Ctx.Buffer_First = Ctx.Buffer_First'Old + and Ctx.Buffer_Last = Ctx.Buffer_Last'Old + and Ctx.First = Ctx.First'Old + and Ctx.Last = Ctx.Last'Old); + + function Valid (Ctx : Context) return Boolean; + + function Has_Buffer (Ctx : Context) return Boolean; + + function Available_Space (Ctx : Context) return RFLX_Types.Bit_Length; + + function Sequence_Last (Ctx : Context) return RFLX_Types.Bit_Length; + + function Size (Ctx : Context) return RFLX_Types.Bit_Length; + + function Byte_Size (Ctx : Context) return RFLX_Types.Length; + + procedure Data (Ctx : Context; Data : out RFLX_Types.Bytes) with + Pre => + (Has_Buffer (Ctx) + and then Valid (Ctx) + and then Data'Length = Byte_Size (Ctx)); + +private + + pragma Warnings (Off, "use clause for package * has no effect"); + + use RFLX.RFLX_Types; + + pragma Warnings (On, "use clause for package * has no effect"); + + type Context_State is (S_Valid, S_Invalid); + + type Context (Buffer_First, Buffer_Last : RFLX_Types.Index := RFLX_Types.Index'First; First : RFLX_Types.Bit_Index := RFLX_Types.Bit_Index'First; Last : RFLX_Types.Bit_Length := RFLX_Types.Bit_Length'First) is + record + Sequence_Last : RFLX_Types.Bit_Length := First - 1; + Buffer : RFLX_Types.Bytes_Ptr := null; + State : Context_State := S_Valid; + First_Element : RFLX.RFLX_Types.Base_Integer := RFLX.RFLX_Types.Base_Integer'First; + Next_Element : RFLX.RFLX_Types.Base_Integer := RFLX.RFLX_Types.Base_Integer'First; + end record with + Dynamic_Predicate => + ((if Buffer /= null then + (Buffer'First = Buffer_First + and Buffer'Last = Buffer_Last)) + and RFLX_Types.To_Index (First) >= Buffer_First + and RFLX_Types.To_Index (Last) <= Buffer_Last + and First mod RFLX_Types.Byte'Size = 1 + and Buffer_Last < RFLX_Types.Index'Last + and First <= Last + 1 + and Last <= RFLX_Types.Bit_Length'Last - 1 + and Sequence_Last >= First - 1 + and Sequence_Last <= Last + and (if Sequence_Last > First - 1 and State = S_Valid then Valid (First_Element))); + + function Has_Element (Ctx : Context) return Boolean is + (Ctx.State = S_Valid and Ctx.Last - Ctx.Sequence_Last >= RFLX.RFLX_Types.Bit_Index (Element_Size)); + + function Valid_Element (Ctx : Context) return Boolean is + (Ctx.State = S_Valid and Valid (Ctx.Next_Element)); + + function Valid (Ctx : Context) return Boolean is + (Ctx.State = S_Valid); + + function Has_Buffer (Ctx : Context) return Boolean is + (Ctx.Buffer /= null); + + function Available_Space (Ctx : Context) return RFLX_Types.Bit_Length is + (Ctx.Last - Ctx.Sequence_Last); + + function Sequence_Last (Ctx : Context) return RFLX_Types.Bit_Length is + (Ctx.Sequence_Last); + + function Size (Ctx : Context) return RFLX_Types.Bit_Length is + (Ctx.Sequence_Last - Ctx.First + 1); + + function Byte_Size (Ctx : Context) return RFLX_Types.Length is + (RFLX_Types.To_Length (Size (Ctx))); + +end RFLX.RFLX_Scalar_Sequence; diff --git a/tests/data/generator/generated/boolean_variable/rflx-rflx_types-operations.ads b/tests/data/generator/generated/boolean_variable/rflx-rflx_types-operations.ads new file mode 100644 index 000000000..b29d5513c --- /dev/null +++ b/tests/data/generator/generated/boolean_variable/rflx-rflx_types-operations.ads @@ -0,0 +1,16 @@ +------------------------------------------------------------------------------ +-- -- +-- Generated by RecordFlux -- +-- -- +-- Copyright (C) AdaCore GmbH -- +-- -- +-- SPDX-License-Identifier: Apache-2.0 -- +-- -- +------------------------------------------------------------------------------ + +pragma Style_Checks ("N3aAbCdefhiIklnOprStux"); +pragma SPARK_Mode; +with RFLX.RFLX_Types.Operators; +with RFLX.RFLX_Generic_Types.Generic_Operations; + +package RFLX.RFLX_Types.Operations is new RFLX.RFLX_Types.Generic_Operations (RFLX.RFLX_Types.Operators); diff --git a/tests/data/generator/generated/boolean_variable/rflx-rflx_types-operators.ads b/tests/data/generator/generated/boolean_variable/rflx-rflx_types-operators.ads new file mode 100644 index 000000000..8a5d54043 --- /dev/null +++ b/tests/data/generator/generated/boolean_variable/rflx-rflx_types-operators.ads @@ -0,0 +1,15 @@ +------------------------------------------------------------------------------ +-- -- +-- Generated by RecordFlux -- +-- -- +-- Copyright (C) AdaCore GmbH -- +-- -- +-- SPDX-License-Identifier: Apache-2.0 -- +-- -- +------------------------------------------------------------------------------ + +pragma Style_Checks ("N3aAbCdefhiIklnOprStux"); +pragma SPARK_Mode; +with RFLX.RFLX_Generic_Types.Generic_Operators; + +package RFLX.RFLX_Types.Operators is new RFLX.RFLX_Types.Generic_Operators; diff --git a/tests/data/generator/generated/boolean_variable/rflx-rflx_types.ads b/tests/data/generator/generated/boolean_variable/rflx-rflx_types.ads new file mode 100644 index 000000000..d5b35fbbb --- /dev/null +++ b/tests/data/generator/generated/boolean_variable/rflx-rflx_types.ads @@ -0,0 +1,16 @@ +------------------------------------------------------------------------------ +-- -- +-- Generated by RecordFlux -- +-- -- +-- Copyright (C) AdaCore GmbH -- +-- -- +-- SPDX-License-Identifier: Apache-2.0 -- +-- -- +------------------------------------------------------------------------------ + +pragma Style_Checks ("N3aAbCdefhiIklnOprStux"); +pragma SPARK_Mode; +with RFLX.RFLX_Generic_Types; +with RFLX.RFLX_Builtin_Types; + +package RFLX.RFLX_Types is new RFLX.RFLX_Generic_Types (RFLX_Builtin_Types.Index, RFLX_Builtin_Types.Byte, RFLX_Builtin_Types.Bytes, RFLX_Builtin_Types.Bytes_Ptr, RFLX_Builtin_Types.Length, RFLX_Builtin_Types.Bit_Length); diff --git a/tests/data/generator/generated/boolean_variable/rflx.ads b/tests/data/generator/generated/boolean_variable/rflx.ads new file mode 100644 index 000000000..033f0ac93 --- /dev/null +++ b/tests/data/generator/generated/boolean_variable/rflx.ads @@ -0,0 +1,13 @@ +------------------------------------------------------------------------------ +-- -- +-- Generated by RecordFlux -- +-- -- +-- Copyright (C) AdaCore GmbH -- +-- -- +-- SPDX-License-Identifier: Apache-2.0 -- +-- -- +------------------------------------------------------------------------------ + +package RFLX is + +end RFLX; \ No newline at end of file diff --git a/tests/unit/generator/generator_test.py b/tests/unit/generator/generator_test.py index 2b7b818a0..16f5c9d9a 100644 --- a/tests/unit/generator/generator_test.py +++ b/tests/unit/generator/generator_test.py @@ -28,14 +28,68 @@ type_ as mty, ) from rflx.model.message import FINAL, INITIAL, Field, Link, Message -from tests.const import GENERATED_DIR +from tests.const import DATA_DIR, GENERATED_DIR from tests.data import models from tests.utils import assert_equal, assert_equal_code +GENERATOR_TEST_DATA_DIR = DATA_DIR / "generator/generated" + MSG_TY = rty.Message("M") SEQ_TY = rty.Sequence("S", rty.Message("M")) +@dataclass +class TC: + name: str + model: Callable[[], Model] + integration: Callable[[], Integration] + + +GENERATOR_TEST_CASES = [ + TC( + "boolean_variable", + lambda: Model( + [ + Message( + "P::Message", + [ + Link(INITIAL, Field("A")), + Link(Field("A"), Field("B")), + Link( + Field("B"), + FINAL, + # TODO(eng/recordflux/RecordFlux#1365): Fix code generation + # condition=expr.Variable("A"), + condition=expr.Equal(expr.Variable("A"), expr.TRUE), + ), + ], + { + Field("A"): mty.BOOLEAN, + Field("B"): mty.Integer( + "P::T", + first=expr.Number(0), + last=expr.Number(127), + size=expr.Number(7), + ), + }, + ), + ], + ), + lambda: Integration(), + ), +] + + +@pytest.mark.parametrize(("tc"), GENERATOR_TEST_CASES) +def test_equality(tc: TC, tmp_path: Path) -> None: + assert_equal_code( + tc.model(), + tc.integration(), + GENERATOR_TEST_DATA_DIR / tc.name, + tmp_path, + ) + + def test_invalid_prefix() -> None: with pytest.raises(FatalError, match=r'^id: error: empty part in identifier "A::::B"$'): Generator("A..B") @@ -160,7 +214,7 @@ def test_type_translation() -> None: @pytest.mark.parametrize("model", models.spark_test_models()) -def test_equality(model: Callable[[], Model], tmp_path: Path) -> None: +def test_equality_spark_tests(model: Callable[[], Model], tmp_path: Path) -> None: assert_equal_code(model(), Integration(), GENERATED_DIR, tmp_path, accept_extra_files=True) diff --git a/tools/generate_spark_test_code.py b/tools/generate_spark_test_code.py index 4e7309deb..8be8cf47c 100755 --- a/tools/generate_spark_test_code.py +++ b/tools/generate_spark_test_code.py @@ -4,8 +4,10 @@ from __future__ import annotations +import argparse import filecmp import logging +import sys from pathlib import Path from rflx.common import unique @@ -15,11 +17,12 @@ from rflx.specification import Parser from tests.const import FEATURE_DIR, SPEC_DIR from tests.data import models +from tests.unit.generator.generator_test import GENERATOR_TEST_CASES, GENERATOR_TEST_DATA_DIR logging.basicConfig(level=logging.INFO, format="%(message)s") logging.disable(logging.NOTSET) -OUTPUT_DIRECTORY = Path("tests/spark/generated") +SPARK_TEST_DIR = Path("tests/spark/generated") SPECIFICATION_FILES = [ SPEC_DIR / "ethernet.rflx", @@ -39,13 +42,37 @@ def main() -> None: - generate_spark_tests() - deduplicate_feature_specs() - generate_feature_tests() + parser = argparse.ArgumentParser() + parser.add_argument( + "--spark", + action="store_true", + help=f"generate test code in {SPARK_TEST_DIR}", + ) + parser.add_argument( + "--generator", + action="store_true", + help=f"generate test code in {GENERATOR_TEST_DATA_DIR}", + ) + parser.add_argument( + "--feature", + action="store_true", + help=f"generate test code in {FEATURE_DIR}/*/generated", + ) + args = parser.parse_args(sys.argv[1:]) + + all_tests = not args.spark and not args.generator and not args.feature + + if all_tests or args.spark: + generate_spark_tests() + if all_tests or args.generator: + generate_generator_tests() + if all_tests or args.feature: + deduplicate_feature_specs() + generate_feature_tests() def generate_spark_tests() -> None: - remove_ada_files(OUTPUT_DIRECTORY) + remove_ada_files(SPARK_TEST_DIR) parser = Parser(Cache()) parser.parse(*SPECIFICATION_FILES) @@ -54,7 +81,22 @@ def generate_spark_tests() -> None: "RFLX", reproducible=True, ignore_unsupported_checksum=True, - ).generate(model, Integration(), OUTPUT_DIRECTORY) + ).generate(model, Integration(), SPARK_TEST_DIR) + + +def generate_generator_tests() -> None: + for directory in GENERATOR_TEST_DATA_DIR.iterdir(): + remove_ada_files(directory) + directory.rmdir() + + for tc in GENERATOR_TEST_CASES: + directory = GENERATOR_TEST_DATA_DIR / tc.name + directory.mkdir() + Generator( + "RFLX", + reproducible=True, + ignore_unsupported_checksum=True, + ).generate(tc.model(), tc.integration(), directory) def generate_feature_tests() -> None: