Skip to content

Instantly share code, notes, and snippets.

@treiher

treiher/defaults.gpr Secret

Last active November 5, 2021 14:27
Show Gist options
  • Save treiher/5e698bea7c5b8fcdd0ef4c077781281a to your computer and use it in GitHub Desktop.
Save treiher/5e698bea7c5b8fcdd0ef4c077781281a to your computer and use it in GitHub Desktop.
Download ZIP
Channel interface
Raw
defaults.gpr
abstract project Defaults is
Proof_Switches :=
(
"--prover=z3,cvc4,altergo",
"--steps=0",
"--timeout=90",
"--memlimit=1000",
"--checks-as-errors",
"--warnings=error",
-- ISSUE: Componolit/RecordFlux#670
-- "--proof-warnings",
"--no-axiom-guard",
"--counterexamples=off",
"-j0"
);
Builder_Switches :=
(
"-j0"
);
Compiler_Switches :=
(
"-gnatA", -- Avoid processing gnat.adc. If a gnat.adc file is present, it will be ignored.
"-gnatf", -- Full errors. Multiple errors per line, all undefined references, do not attempt to suppress cascaded errors.
"-gnatU", -- Tag all error messages with the unique string ‘error:’.
-- Validity Checks
"-gnatVc", -- Validity checks for copies.
"-gnatVd", -- Default (RM) validity checks.
"-gnatVe", -- Validity checks for elementary components.
"-gnatVf", -- Validity checks for floating-point values.
"-gnatVi", -- Validity checks for ``in`` mode parameters.
"-gnatVm", -- Validity checks for ``in out`` mode parameters.
"-gnatVo", -- Validity checks for operator and attribute operands.
"-gnatVp", -- Validity checks for parameters.
"-gnatVr", -- Validity checks for function returns.
"-gnatVs", -- Validity checks for subscripts.
"-gnatVt", -- Validity checks for tests.
"-gnateV", -- Check that all actual parameters of a subprogram call are valid according to the rules of validity checking (Validity Checking).
-- Debugging
"-fstack-check", -- Activate stack checking.
"-g", -- Enable generation of debugging information.
"-gnata", -- Enable assertions.
-- Warnings
"-gnatwa", -- Activate most optional warnings.
"-gnatw.d", -- Activate tagging of warning and info messages.
"-gnatwe", -- Treat all run-time exception warnings as errors.
"-gnatwd", -- Activate warnings on implicit dereferencing.
-- ISSUE: Componolit/Workarounds#27
-- "-gnatwh", -- Activate warnings on hiding.
"-gnatwt", -- Activate warnings for tracking of deleted conditional code.
-- Style Checks
"-gnaty3", -- Specify indentation level.
"-gnatya", -- Check attribute casing.
"-gnatyA", -- Use of array index numbers in array attributes.
"-gnatyb", -- Blanks not allowed at statement end.
"-gnatyc", -- Check comments, double space.
"-gnatyd", -- Check no DOS line terminators present.
"-gnatye", -- Check end/exit labels.
"-gnatyf", -- No form feeds or vertical tabs.
"-gnatyh", -- No horizontal tabs.
"-gnatyi", -- Check if-then layout.
"-gnatyI", -- Check mode IN keywords.
"-gnatyk", -- Check keyword casing.
"-gnatyl", -- Check layout.
"-gnatyL9", -- Set maximum nesting level.
"-gnatyM120", -- Set maximum line length.
"-gnatyn", -- Check casing of entities in Standard.
"-gnatyO", -- Check that overriding subprograms are explicitly marked as such.
"-gnatyp", -- Check pragma casing.
"-gnatyr", -- Check references.
"-gnatyS", -- Check no statements after then/else.
"-gnatyt", -- Check token spacing.
"-gnatyu", -- Check unnecessary blank lines.
"-gnatyx", -- Check extra parentheses.
""
);
Binder_Switches :=
(
"-Es"
);
end Defaults;
Raw
lib.adb
pragma Style_Checks ("N3aAbcdefhiIklnOprStux");
pragma Warnings (Off, "redundant conversion");
with Ada.Text_IO;
with RFLX.RFLX_Types;
package body Lib with
SPARK_Mode
is
type Channel_Number is array (Session.Channel) of Natural;
Written_Messages : Channel_Number := (others => 0);
procedure Print (Prefix : String; Buffer : RFLX.RFLX_Types.Bytes) is
begin
Ada.Text_IO.Put (Prefix & ":");
for B of Buffer loop
Ada.Text_IO.Put (B'Image);
end loop;
Ada.Text_IO.New_Line;
end Print;
function Next_Message (Chan : Session.Channel) return RFLX.RFLX_Types.Bytes is
use type Session.Channel;
None : constant RFLX.RFLX_Types.Bytes (RFLX.RFLX_Types.Index'Last .. RFLX.RFLX_Types.Index'First) := (others => RFLX.RFLX_Types.Byte'First);
M : constant RFLX.RFLX_Types.Bytes := (if
Chan = Session.C_I_1 and Written_Messages (Chan) = 0
then
(1, 0, 1, 0)
elsif
Chan = Session.C_I_1 and Written_Messages (Chan) = 1
then
(1, 0, 1, 1)
elsif
Chan = Session.C_I_2 and Written_Messages (Chan) = 0
then
(1, 0, 1, 2)
elsif
Chan = Session.C_I_2 and Written_Messages (Chan) = 1
then
(1, 0, 1, 3)
else
None);
begin
return M;
end Next_Message;
procedure Write (Chan : Session.Channel) with
Pre =>
Session.Initialized
and then Session.Needs_Data (Chan),
Post =>
Session.Initialized
is
use type RFLX.RFLX_Types.Length;
Message : constant RFLX.RFLX_Types.Bytes := Next_Message (Chan);
begin
if Message'Length > 0 and Message'Length < Session.Write_Buffer_Size (Chan) then
Print ("Write " & Chan'Image, Message);
Session.Write (Chan, Message);
if Written_Messages (Chan) < Natural'Last then
Written_Messages (Chan) := Written_Messages (Chan) + 1;
end if;
end if;
end Write;
procedure Run is
use type RFLX.RFLX_Types.Index;
use type RFLX.RFLX_Types.Length;
begin
Session.Initialize;
while Session.Active loop
pragma Loop_Invariant (Session.Initialized);
for C in Session.Channel'Range loop
pragma Loop_Invariant (Session.Initialized);
if Session.Has_Data (C) then
declare
Buffer : RFLX.RFLX_Types.Bytes (RFLX.RFLX_Types.Index'First .. RFLX.RFLX_Types.Index'First + 4095) := (others => 0);
begin
if Buffer'Length >= Session.Read_Buffer_Size (C) then
Session.Read (C, Buffer (Buffer'First .. Buffer'First - 2 + RFLX.RFLX_Types.Index (Session.Read_Buffer_Size (C) + 1)));
Print ("Read " & C'Image, Buffer (Buffer'First .. Buffer'First - 2 + RFLX.RFLX_Types.Index (Session.Read_Buffer_Size (C) + 1)));
else
Ada.Text_IO.Put_Line ("Read " & C'Image & ": buffer too small");
end if;
end;
end if;
if Session.Needs_Data (C) then
Write (C);
end if;
end loop;
Session.Run;
end loop;
Session.Finalize;
end Run;
end Lib;
Raw
lib.ads
pragma Style_Checks ("N3aAbcdefhiIklnOprStux");
pragma Warnings (Off, "redundant conversion");
with RFLX.Test.Session;
package Lib with
SPARK_Mode,
Initial_Condition =>
Session.Uninitialized
is
package Session is new RFLX.Test.Session;
procedure Run with
Pre =>
Session.Uninitialized,
Post =>
Session.Uninitialized;
end Lib;
Raw
main.adb
with Lib;
pragma Elaborate (Lib);
procedure Main with
SPARK_Mode,
Pre => Lib.Session.Uninitialized
is
begin
Lib.Run;
end Main;
Raw
main.adb.orig
with Lib;
pragma Elaborate (Lib);
procedure Main with
SPARK_Mode,
Pre => Lib.Session.Uninitialized
is
begin
Lib.Session.Run;
<<<<<<< HEAD
end Main;
=======
end Main;
>>>>>>> 89b8587 (Add initial version)
Raw
rflx-rflx_arithmetic.adb
--
-- Generated by RecordFlux 0.6.0-pre on 2021-10-25
--
-- Copyright (C) 2018-2021 Componolit GmbH
--
-- This file is distributed under the terms of the GNU Affero General Public License version 3.
--
pragma Style_Checks ("N3aAbcdefhiIklnOprStux");
package body RFLX.RFLX_Arithmetic with
SPARK_Mode
is
function Pow2 (Exp : Natural) return U64 is
(2**Exp);
function Mod_Pow2 (Value : U64; Exp : Natural) return U64 is
(Value mod Pow2 (Exp));
procedure Lemma_Right_Shift_Limit (X : U64; J : Natural; K : Natural) with
Pre =>
J <= U64'Size
and then K < U64'Size
and then J >= K
and then J - K in 0 .. U64'Size - 1
and then (if J < U64'Size then X < 2**J),
Post =>
X / Pow2 (K) < Pow2 (J - K),
Ghost
is
begin
null;
end Lemma_Right_Shift_Limit;
procedure Lemma_Left_Shift_Limit (X : U64; J : Natural; K : Natural) with
Pre =>
J <= U64'Size
and then K < U64'Size
and then J + K <= U64'Size
and then (if J < U64'Size then X < Pow2 (J)),
Post =>
(if J + K < U64'Size
then X * Pow2 (K) <= Pow2 (J + K) - Pow2 (K) and Pow2 (J + K) >= Pow2 (K)
else X * Pow2 (K) <= U64'Last - Pow2 (K) + 1),
Ghost
is
begin
null;
end Lemma_Left_Shift_Limit;
function Right_Shift (Value : U64; Value_Size : Positive; Length : Natural) return U64
is
Result : constant U64 := Value / Pow2 (Length);
begin
Lemma_Right_Shift_Limit (Value, Value_Size, Length);
return Result;
end Right_Shift;
function Left_Shift (Value : U64; Value_Size : Positive; Length : Natural) return U64
is
Result : constant U64 := Value * 2**Length;
begin
Lemma_Left_Shift_Limit (Value, Value_Size, Length);
return Result;
end Left_Shift;
end RFLX.RFLX_Arithmetic;
Raw
rflx-rflx_arithmetic.ads
--
-- Generated by RecordFlux 0.6.0-pre on 2021-10-25
--
-- Copyright (C) 2018-2021 Componolit GmbH
--
-- This file is distributed under the terms of the GNU Affero General Public License version 3.
--
pragma Style_Checks ("N3aAbcdefhiIklnOprStux");
package RFLX.RFLX_Arithmetic with
SPARK_Mode
is
type U64 is mod 2**64 with
Annotate => (GNATprove, No_Wrap_Around);
function Pow2 (Exp : Natural) return U64 with
Pre =>
Exp < U64'Size,
Post =>
Pow2'Result = 2**Exp;
function Mod_Pow2 (Value : U64; Exp : Natural) return U64 with
Pre =>
Exp < U64'Size,
Post =>
Mod_Pow2'Result < 2**Exp;
function Right_Shift (Value : U64; Value_Size : Positive; Length : Natural) return U64 with
Pre =>
Value_Size <= U64'Size
and then Length < U64'Size
and then Value_Size >= Length
and then Value_Size - Length in 0 .. U64'Size - 1
and then (if Value_Size < U64'Size then Value < 2**Value_Size),
Post =>
Right_Shift'Result < 2**(Value_Size - Length);
function Left_Shift (Value : U64; Value_Size : Positive; Length : Natural) return U64 with
Pre =>
Value_Size <= U64'Size
and then Length < U64'Size
and then Value_Size + Length in 1 .. U64'Size
and then (if Value_Size < U64'Size then Value < Pow2 (Value_Size)),
Post =>
(if
Value_Size + Length < U64'Size
then
Left_Shift'Result <= Pow2 (Value_Size + Length) - Pow2 (Length)
and Pow2 (Value_Size + Length) >= Pow2 (Length)
else
Left_Shift'Result <= U64'Last - Pow2 (Length) + 1);
end RFLX.RFLX_Arithmetic;
Raw
rflx-rflx_builtin_types-conversions.ads
--
-- Generated by RecordFlux 0.6.0-pre on 2021-10-25
--
-- Copyright (C) 2018-2021 Componolit GmbH
--
-- This file is distributed under the terms of the GNU Affero General Public License version 3.
--
pragma Style_Checks ("N3aAbcdefhiIklnOprStux");
package RFLX.RFLX_Builtin_Types.Conversions with
SPARK_Mode
is
pragma Annotate (GNATprove, Terminating, Conversions);
function Valid (Val : Boolean_Base) return Boolean is
(case Val is
when 0 | 1 =>
True);
function To_Base (Enum : Boolean) return Boolean_Base is
(case Enum is
when False =>
0,
when True =>
1);
function To_Actual (Val : Boolean_Base) return Boolean is
(case Val is
when 0 =>
False,
when 1 =>
True)
with
Pre =>
Valid (Val);
end RFLX.RFLX_Builtin_Types.Conversions;
Raw
rflx-rflx_builtin_types.ads
--
-- Generated by RecordFlux 0.6.0-pre on 2021-10-25
--
-- Copyright (C) 2018-2021 Componolit GmbH
--
-- This file is distributed under the terms of the GNU Affero General Public License version 3.
--
pragma Style_Checks ("N3aAbcdefhiIklnOprStux");
package RFLX.RFLX_Builtin_Types with
SPARK_Mode
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;
Raw
rflx-rflx_generic_types.adb
--
-- Generated by RecordFlux 0.6.0-pre on 2021-10-25
--
-- Copyright (C) 2018-2021 Componolit GmbH
--
-- This file is distributed under the terms of the GNU Affero General Public License version 3.
--
pragma Style_Checks ("N3aAbcdefhiIklnOprStux");
package body RFLX.RFLX_Generic_Types with
SPARK_Mode
is
--
-- Terminology
--
-- -----XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX---- Data
--
-- |-------|-------|-------|-------|-------| Value Bytes
-- 3 MSB 11 19 27 35 LSB 43
--
-- |----| |----|
-- MSE_Offset LSE_Offset
--
-- |--| |--|
-- MSE_Size LSE_Size
--
-- |-------|-------|-------|-------|-------|-------| Data Bytes
-- 0 8 16 24 32 40
-- MSE LSE
--
-- LSE: Least Significant Element of Data
-- MSE: Most Significant Element of Data
--
-- LSB: Least Significant Byte of Value
-- MSB: Most Significant Byte of Value
--
-- LSE_Offset: Bits the LSE is shifted left relative to last of LSE
-- MSE_Offset: Bits the MSE is shifted right relative to first of MSE
--
-- LSE_Size: Number of bits of LSE contained in LSB
-- MSE_Size: Number of bits of MSE contained in MSB
--
-- LSE_Index: Index pointing to LSE
-- MSE_Index: Index pointing to MSE
--
use type RFLX.RFLX_Arithmetic.U64;
function Left_Shift (Value : U64; Value_Size : Positive; Length : Natural) return U64 renames RFLX.RFLX_Arithmetic.Left_Shift;
function Right_Shift (Value : U64; Value_Size : Positive; Length : Natural) return U64 renames RFLX.RFLX_Arithmetic.Right_Shift;
function Mod_Pow2 (Value : U64; Exp : Natural) return U64 renames RFLX.RFLX_Arithmetic.Mod_Pow2;
function Pow2 (Exp : Natural) return U64 renames RFLX.RFLX_Arithmetic.Pow2;
function U64_Extract_Intermediate (Data_Current : U64;
Data_Next : U64;
LSE_Size : Natural;
LSE_Offset : Natural;
Shift_Length : Natural) return U64 with
Pre =>
Data_Current < 2**Byte'Size
and then Data_Next < 2**Byte'Size
and then LSE_Size in 0 .. Byte'Size
and then LSE_Offset in 0 .. Byte'Size - 1
and then Shift_Length <= U64'Size - Byte'Size
and then LSE_Size + LSE_Offset = Byte'Size,
Post =>
(if Byte'Size + Shift_Length < U64'Size
then U64_Extract_Intermediate'Result <= Pow2 (Byte'Size + Shift_Length) - Pow2 (Shift_Length)
else U64_Extract_Intermediate'Result <= U64'Last - Pow2 (Shift_Length) + 1)
is
Current : constant U64 := Right_Shift (Data_Current, Byte'Size, LSE_Offset);
Next : constant U64 := (if LSE_Offset > 0
then Left_Shift (Data_Next mod Pow2 (LSE_Offset), LSE_Offset, LSE_Size)
else Data_Next mod Pow2 (LSE_Offset));
begin
return Left_Shift (Current + Next, Byte'Size, Shift_Length);
end U64_Extract_Intermediate;
function U64_Extract_Remaining (Data : U64;
Element_Count : Natural;
MSE_Size : Natural;
LSE_Offset : Natural) return U64 with
Pre =>
MSE_Size in 0 .. Byte'Size
and LSE_Offset in 0 .. Byte'Size - 1
and MSE_Size - LSE_Offset in 1 .. Byte'Size
and Element_Count <= 7,
Post =>
(if
MSE_Size - LSE_Offset + (Byte'Size * Element_Count) < U64'Size
then
U64_Extract_Remaining'Result <= Pow2 (MSE_Size - LSE_Offset + (Byte'Size * Element_Count))
- Pow2 (Byte'Size * Element_Count)
and Pow2 (MSE_Size - LSE_Offset + (Byte'Size * Element_Count)) >= Pow2 (Byte'Size * Element_Count)
else
U64_Extract_Remaining'Result <= U64'Last - Pow2 (Byte'Size * Element_Count) + 1)
is
Remaining_Bits : constant U64 := Right_Shift (Data mod Pow2 (MSE_Size), MSE_Size, LSE_Offset);
begin
return Left_Shift (Remaining_Bits, MSE_Size - LSE_Offset, Byte'Size * Element_Count);
end U64_Extract_Remaining;
function U64_Extract (Data : Bytes;
Off : Offset;
Value_Size : Positive) return U64 with
Pre =>
(Value_Size in 1 .. U64'Size
and then Long_Integer ((Natural (Off) + Value_Size - 1) / Byte'Size) < Data'Length
and then (Natural (Off) + Value_Size - 1) / Byte'Size <= Natural'Size
and then (Byte'Size - Natural (Off) mod Byte'Size) < Long_Integer'Size - 1),
Post =>
(if Value_Size < U64'Size then U64_Extract'Result < 2**Value_Size)
is
LSE_Index : constant Long_Integer := Long_Integer (Off) / Byte'Size;
MSE_Index : constant Long_Integer := Long_Integer (Natural (Off) + Value_Size - 1) / Byte'Size;
LSE_Offset : constant Natural := Natural (Natural (Off) mod Byte'Size);
LSE_Size : constant Natural := Byte'Size - LSE_Offset;
MSE_Size : constant Natural := (LSE_Offset + Value_Size + Byte'Size - 1) mod Byte'Size + 1;
function D (Idx : Long_Integer) return Byte with
Pre =>
Idx >= 0 and then Idx < Data'Length and then Value_Size in 1 .. 64
is
function ES return Natural is (Byte'Size) with Post => ES'Result = Byte'Size;
E : constant Natural := (LSE_Offset + Value_Size + Byte'Size - 1) mod ES + 1;
pragma Assert (2**Byte'Size = 2**ES);
begin
declare
Mask : constant Natural := (if Idx < MSE_Index then 2**ES else 2**E);
Val : constant Byte := Data (Index (Long_Integer (Data'Last) - Idx));
begin
return Byte'Val (Byte'Pos (Val) mod Mask);
end;
end D;
Result : U64 := 0;
begin
for I in LSE_Index .. MSE_Index - 1
loop
Result := Result + U64_Extract_Intermediate (Byte'Pos (D (I)),
Byte'Pos (D (I + 1)),
LSE_Size,
LSE_Offset,
Byte'Size * Natural (I - LSE_Index));
pragma Loop_Invariant (I - LSE_Index <= 7);
pragma Loop_Invariant (if Byte'Size + Byte'Size * (I - LSE_Index) /= U64'Size
then Result < 2**(Byte'Size + Byte'Size * Natural (I - LSE_Index)));
end loop;
if MSE_Size > LSE_Offset then
declare
Element_Count : constant Natural := Natural (MSE_Index - LSE_Index);
Val : constant U64 := U64_Extract_Remaining (Byte'Pos (D (MSE_Index)), Element_Count, MSE_Size, LSE_Offset);
begin
Result := Result + Val;
end;
end if;
return (if Value_Size < U64'Size then Result mod Pow2 (Value_Size) else Result);
end U64_Extract;
function Extract (Data : Bytes;
Off : Offset) return Value
is
pragma Compile_Time_Error ((if Value'Size = 64 then
U64 (Value'First) /= U64'First or U64 (Value'Last) /= U64'Last
else
U64 (Value'Last) - U64 (Value'First) /= U64 (2**Value'Size) - 1),
"Value must cover entire value range");
begin
return Value (U64_Extract (Data, Off, Value'Size));
end Extract;
procedure U64_Insert (Val : U64;
Data : in out Bytes;
Off : Offset;
Value_Size : Positive) with
Pre =>
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 < Data'Length
is
LSE_Index : constant Long_Integer := Long_Integer (Off) / Byte'Size;
MSE_Index : constant Long_Integer := Long_Integer (Natural (Off) + Natural (Value_Size) - 1) / Byte'Size;
LSE_Offset : constant Natural := Natural (Natural (Off) mod Byte'Size);
LSE_Size : constant Natural := Byte'Size - LSE_Offset;
MSE_Size : constant Natural := (LSE_Offset + Value_Size + Byte'Size - 1) mod Byte'Size + 1;
MSE_Offset : constant Natural := Byte'Size - MSE_Size;
function Read (Idx : Long_Integer) return Byte with
Pre =>
Idx >= 0 and then Idx < Data'Length
is
begin
return Data (Index (Long_Integer (Data'Last) - Idx));
end Read;
procedure Write (Idx : Long_Integer; Element : Byte) with
Pre =>
Idx >= 0 and then Idx < Data'Length
is
begin
Data (Index (Long_Integer (Data'Last) - Idx)) := Element;
end Write;
RV : U64;
begin
if LSE_Index = MSE_Index then
--
-- LSE/MSE
--
-- ---XX---
--
-- |--|-|--|
-- 0 U V L 8
--
-- U: Unchanged upper bits
-- V: Bits to set
-- L: Unchanged lower bits
--
declare
L_Size : constant Natural := LSE_Offset;
V_Size : constant Natural := Value_Size;
L_Bits : constant U64 := Mod_Pow2 (Byte'Pos (Read (LSE_Index)), L_Size);
V_Bits : constant U64 := Val;
U_Bits : constant U64 := Right_Shift (Byte'Pos (Read (MSE_Index)), Byte'Size, L_Size + V_Size);
L_Value : constant U64 := L_Bits;
V_Value : constant U64 := Left_Shift (V_Bits, V_Size, L_Size);
U_Value : constant U64 := (if L_Size + V_Size < Byte'Size
then Left_Shift (U_Bits, Byte'Size - L_Size - V_Size, L_Size + V_Size)
else U_Bits);
pragma Assert (L_Value + V_Value + U_Value < Pow2 (Byte'Size));
begin
Write (LSE_Index, Byte'Val (L_Value + V_Value + U_Value));
end;
else
--
-- LSE
--
-- XXXX----
--
-- |---|---|
-- 0 V L 8
--
-- V: Bits to set
-- L: Unchanged lower bits
--
declare
L_Bits : constant U64 := Mod_Pow2 (Byte'Pos (Read (LSE_Index)), LSE_Offset);
V_Bits : constant U64 := Mod_Pow2 (Val, LSE_Size);
V_Value : constant U64 := Left_Shift (V_Bits, LSE_Size, LSE_Offset);
begin
Write (LSE_Index, Byte'Val (L_Bits + V_Value));
RV := Right_Shift (Val, Value_Size, LSE_Size);
end;
-- LSE + 1 .. MSE - 1
for I in LSE_Index + 1 .. MSE_Index - 1
loop
pragma Loop_Invariant (RV < 2**(Value_Size - LSE_Size - Natural (I - LSE_Index - 1) * Byte'Size));
Write (I, Byte'Val (RV mod 2**Byte'Size));
RV := Right_Shift (RV, Value_Size - LSE_Size - Natural (I - LSE_Index - 1) * Byte'Size, Byte'Size);
end loop;
--
-- MSE
--
-- ----XXXX
--
-- |---|---|
-- 0 U V 8
--
-- U: Unchanged upper bits
-- V: Bits to set
--
declare
V_Size : constant Natural := MSE_Size;
U_Size : constant Natural := MSE_Offset;
V_Bits : constant U64 := Mod_Pow2 (RV, V_Size);
U_Bits : constant U64 := Right_Shift (Byte'Pos (Read (MSE_Index)), Byte'Size, V_Size);
U_Value : constant U64 := (if U_Size > 0 then Left_Shift (U_Bits, U_Size, V_Size) else U_Bits);
begin
Write (MSE_Index, Byte'Val (V_Bits + U_Value));
end;
end if;
end U64_Insert;
procedure Insert (Val : Value;
Data : in out Bytes;
Off : Offset)
is
pragma Compile_Time_Error ((if Value'Size = 64 then
U64 (Value'First) /= U64'First or U64 (Value'Last) /= U64'Last
else
U64 (Value'Last) - U64 (Value'First) /= U64 (2**Value'Size) - 1),
"Value must cover entire value range");
begin
U64_Insert (U64 (Val), Data, Off, Value'Size);
end Insert;
end RFLX.RFLX_Generic_Types;
Raw
rflx-rflx_generic_types.ads
--
-- Generated by RecordFlux 0.6.0-pre on 2021-10-25
--
-- Copyright (C) 2018-2021 Componolit GmbH
--
-- This file is distributed under the terms of the GNU Affero General Public License version 3.
--
pragma Style_Checks ("N3aAbcdefhiIklnOprStux");
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
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;
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 Bit_Index is Bit_Length range 1 .. Bit_Length'Last;
subtype U64 is RFLX.RFLX_Arithmetic.U64;
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_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);
type Offset is mod 8;
generic
type Value is mod <>;
function Extract (Data : Bytes;
Off : Offset) return Value with
Pre =>
((Offset'Pos (Off) + Value'Size - 1) / Byte'Size < Data'Length
and then (Offset'Pos (Off) + Value'Size - 1) / Byte'Size <= Natural'Size
and then (Byte'Size - Natural (Offset'Pos (Off) mod Byte'Size)) < Long_Integer'Size - 1);
generic
type Value is mod <>;
procedure Insert (Val : Value;
Data : in out Bytes;
Off : Offset) with
Pre =>
(Offset'Pos (Off) + Value'Size - 1) / Byte'Size < Data'Length;
procedure Free is new Ada.Unchecked_Deallocation (Object => Bytes, Name => Bytes_Ptr);
end RFLX.RFLX_Generic_Types;
Raw
rflx-rflx_message_sequence.adb
--
-- Generated by RecordFlux 0.6.0-pre on 2021-10-25
--
-- Copyright (C) 2018-2021 Componolit GmbH
--
-- This file is distributed under the terms of the GNU Affero General Public License version 3.
--
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 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);
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;
end RFLX.RFLX_Message_Sequence;
Raw
rflx-rflx_message_sequence.ads
--
-- Generated by RecordFlux 0.6.0-pre on 2021-10-25
--
-- Copyright (C) 2018-2021 Componolit GmbH
--
-- This file is distributed under the terms of the GNU Affero General Public License version 3.
--
pragma Style_Checks ("N3aAbcdefhiIklnOprStux");
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);
with procedure Element_Take_Buffer (Ctx : in out Element_Context; Buffer : out RFLX_Types.Bytes_Ptr);
with function Element_Has_Buffer (Ctx : Element_Context) return Boolean;
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
is
pragma Annotate (GNATprove, Terminating, RFLX_Message_Sequence);
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 with
Contract_Cases =>
(Has_Buffer (Ctx) => (Has_Element'Result or not Has_Element'Result) and Has_Buffer (Ctx),
not Has_Buffer (Ctx) => (Has_Element'Result or not Has_Element'Result) and not Has_Buffer (Ctx));
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;
private
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
(if
Ctx.Sequence_Last = Ctx.First - 1
then
0
else
RFLX_Types.Length (RFLX_Types.To_Index (Ctx.Sequence_Last) - RFLX_Types.To_Index (Ctx.First)) + 1);
end RFLX.RFLX_Message_Sequence;
Raw
rflx-rflx_scalar_sequence.adb
--
-- Generated by RecordFlux 0.6.0-pre on 2021-10-25
--
-- Copyright (C) 2018-2021 Componolit GmbH
--
-- This file is distributed under the terms of the GNU Affero General Public License version 3.
--
pragma Style_Checks ("N3aAbcdefhiIklnOprStux");
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 => Element_Base_Type'First, Next_Element => Element_Base_Type'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 + Element_Base_Type'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);
function Extract is new RFLX_Types.Extract (Element_Base_Type);
begin
if Buffer_First >= Ctx.Buffer'First and Buffer_Last <= Ctx.Buffer'Last and Buffer_First <= Buffer_Last then
Ctx.Next_Element := Extract (Ctx.Buffer.all (Buffer_First .. Buffer_Last), Offset);
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 + Element_Base_Type'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;
procedure Insert is new RFLX_Types.Insert (Element_Base_Type);
begin
Last_Bit := Ctx.Sequence_Last + Element_Base_Type'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
Insert (To_Base (Value), Ctx.Buffer.all (First .. Last), Offset);
end if;
if Size (Ctx) = 0 then
Ctx.First_Element := To_Base (Value);
end if;
Ctx.Sequence_Last := Ctx.Sequence_Last + Element_Base_Type'Size;
end Append_Element;
end RFLX.RFLX_Scalar_Sequence;
Raw
rflx-rflx_scalar_sequence.ads
--
-- Generated by RecordFlux 0.6.0-pre on 2021-10-25
--
-- Copyright (C) 2018-2021 Componolit GmbH
--
-- This file is distributed under the terms of the GNU Affero General Public License version 3.
--
pragma Style_Checks ("N3aAbcdefhiIklnOprStux");
with RFLX.RFLX_Types;
generic
type Element_Type is private;
type Element_Base_Type is mod <>;
with function Valid (Element : Element_Base_Type) return Boolean;
with function To_Actual (Element : Element_Base_Type) return Element_Type;
with function To_Base (Element : Element_Type) return Element_Base_Type;
package RFLX.RFLX_Scalar_Sequence with
SPARK_Mode
is
pragma Annotate (GNATprove, Terminating, RFLX_Scalar_Sequence);
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;
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 + Element_Base_Type'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 with
Contract_Cases =>
(Has_Buffer (Ctx) => (Valid_Element'Result or not Valid_Element'Result)
and Has_Buffer (Ctx),
not Has_Buffer (Ctx) => (Valid_Element'Result or not Valid_Element'Result)
and not Has_Buffer (Ctx));
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 + Element_Base_Type'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 (Value))
and then Available_Space (Ctx) >= Element_Base_Type'Size),
Post =>
(Has_Buffer (Ctx)
and Valid (Ctx)
and Sequence_Last (Ctx) = Sequence_Last (Ctx)'Old + Element_Base_Type'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;
private
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 : Element_Base_Type := Element_Base_Type'First;
Next_Element : Element_Base_Type := Element_Base_Type'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 >= Element_Base_Type'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
(if
Ctx.Sequence_Last = Ctx.First - 1
then
0
else
RFLX_Types.Length (RFLX_Types.To_Index (Ctx.Sequence_Last) - RFLX_Types.To_Index (Ctx.First)) + 1);
end RFLX.RFLX_Scalar_Sequence;
Raw
rflx-rflx_types.ads
--
-- Generated by RecordFlux 0.6.0-pre on 2021-10-25
--
-- Copyright (C) 2018-2021 Componolit GmbH
--
-- This file is distributed under the terms of the GNU Affero General Public License version 3.
--
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);
Raw
rflx-test-session.adb
--
-- Generated by RecordFlux 0.6.0-pre on 2021-10-25
--
-- Copyright (C) 2018-2021 Componolit GmbH
--
-- This file is distributed under the terms of the GNU Affero General Public License version 3.
--
pragma Style_Checks ("N3aAbcdefhiIklnOprStux");
pragma Warnings (Off, "redundant conversion");
with Ada.Text_IO;
package body RFLX.Test.Session with
SPARK_Mode
is
procedure Start (P_Next_State : out State) with
Pre =>
Initialized,
Post =>
Initialized
is
begin
Universal.Message.Verify_Message (Message_1_Ctx);
Universal.Message.Verify_Message (Message_2_Ctx);
if Universal.Message.Byte_Size (Message_1_Ctx) > 0 then
P_Next_State := S_Reply_1;
elsif Universal.Message.Byte_Size (Message_2_Ctx) > 0 then
P_Next_State := S_Reply_2;
else
P_Next_State := S_Terminated;
end if;
end Start;
procedure Reply_1 (P_Next_State : out State) with
Pre =>
Initialized,
Post =>
Initialized
is
begin
P_Next_State := S_Start;
end Reply_1;
procedure Reply_2 (P_Next_State : out State) with
Pre =>
Initialized,
Post =>
Initialized
is
begin
P_Next_State := S_Start;
end Reply_2;
procedure Error (P_Next_State : out State) with
Pre =>
Initialized,
Post =>
Initialized
is
begin
P_Next_State := S_Terminated;
end Error;
procedure Initialize is
Message_1_Buffer : RFLX_Types.Bytes_Ptr;
Message_2_Buffer : RFLX_Types.Bytes_Ptr;
begin
Test.Session_Allocator.Initialize;
Message_1_Buffer := Test.Session_Allocator.Slot_Ptr_1;
pragma Warnings (Off, "unused assignment");
Test.Session_Allocator.Slot_Ptr_1 := null;
pragma Warnings (On, "unused assignment");
Universal.Message.Initialize (Message_1_Ctx, Message_1_Buffer);
Message_2_Buffer := Test.Session_Allocator.Slot_Ptr_2;
pragma Warnings (Off, "unused assignment");
Test.Session_Allocator.Slot_Ptr_2 := null;
pragma Warnings (On, "unused assignment");
Universal.Message.Initialize (Message_2_Ctx, Message_2_Buffer);
P_Next_State := S_Start;
end Initialize;
procedure Finalize is
Message_1_Buffer : RFLX_Types.Bytes_Ptr;
Message_2_Buffer : RFLX_Types.Bytes_Ptr;
begin
pragma Warnings (Off, "unused assignment to ""Message_1_Ctx""");
pragma Warnings (Off, """Message_1_Ctx"" is set by ""Take_Buffer"" but not used after the call");
Universal.Message.Take_Buffer (Message_1_Ctx, Message_1_Buffer);
pragma Warnings (On, """Message_1_Ctx"" is set by ""Take_Buffer"" but not used after the call");
pragma Warnings (On, "unused assignment to ""Message_1_Ctx""");
pragma Warnings (Off, "unused assignment");
Test.Session_Allocator.Slot_Ptr_1 := Message_1_Buffer;
pragma Warnings (On, "unused assignment");
pragma Warnings (Off, "unused assignment to ""Message_2_Ctx""");
pragma Warnings (Off, """Message_2_Ctx"" is set by ""Take_Buffer"" but not used after the call");
Universal.Message.Take_Buffer (Message_2_Ctx, Message_2_Buffer);
pragma Warnings (On, """Message_2_Ctx"" is set by ""Take_Buffer"" but not used after the call");
pragma Warnings (On, "unused assignment to ""Message_2_Ctx""");
pragma Warnings (Off, "unused assignment");
Test.Session_Allocator.Slot_Ptr_2 := Message_2_Buffer;
pragma Warnings (On, "unused assignment");
P_Next_State := S_Terminated;
end Finalize;
procedure Reset_Messages_Before_Read with
Pre =>
Initialized,
Post =>
Initialized
is
use type RFLX_Types.Bit_Length;
begin
case P_Next_State is
when S_Start =>
Universal.Message.Reset (Message_1_Ctx, Message_1_Ctx.First, Message_1_Ctx.First - 1);
Universal.Message.Reset (Message_2_Ctx, Message_2_Ctx.First, Message_2_Ctx.First - 1);
when S_Reply_1 =>
null;
when S_Reply_2 =>
null;
when S_Error =>
null;
when S_Terminated =>
null;
end case;
end Reset_Messages_Before_Read;
procedure Tick is
begin
case P_Next_State is
when S_Start =>
Ada.Text_IO.Put_Line ("State: Start");
Start (P_Next_State);
when S_Reply_1 =>
Ada.Text_IO.Put_Line ("State: Reply_1");
Reply_1 (P_Next_State);
when S_Reply_2 =>
Ada.Text_IO.Put_Line ("State: Reply_2");
Reply_2 (P_Next_State);
when S_Error =>
Ada.Text_IO.Put_Line ("State: Error");
Error (P_Next_State);
when S_Terminated =>
Ada.Text_IO.Put_Line ("State: Terminated");
null;
end case;
Reset_Messages_Before_Read;
end Tick;
function In_IO_State return Boolean is
(P_Next_State in S_Start | S_Reply_1 | S_Reply_2);
procedure Run is
begin
Tick;
while Active and not In_IO_State loop
pragma Loop_Invariant (Initialized);
Tick;
end loop;
end Run;
function Needs_Data (Chan : Channel) return Boolean is
((case Chan is
when C_I_1 | C_I_2 =>
(case P_Next_State is
when S_Start =>
True,
when others =>
False),
when C_O =>
False));
function Has_Data (Chan : Channel) return Boolean is
((case Chan is
when C_I_1 | C_I_2 =>
False,
when C_O =>
(case P_Next_State is
when S_Reply_1 =>
Universal.Message.Structural_Valid_Message (Message_1_Ctx)
and Universal.Message.Byte_Size (Message_1_Ctx) > 0,
when S_Reply_2 =>
Universal.Message.Structural_Valid_Message (Message_2_Ctx)
and Universal.Message.Byte_Size (Message_2_Ctx) > 0,
when others =>
False)));
function Read_Buffer_Size (Chan : Channel) return RFLX_Types.Length is
((case Chan is
when C_I_1 | C_I_2 =>
raise Program_Error,
when C_O =>
(case P_Next_State is
when S_Reply_1 =>
Universal.Message.Byte_Size (Message_1_Ctx),
when S_Reply_2 =>
Universal.Message.Byte_Size (Message_2_Ctx),
when others =>
raise Program_Error)));
function Write_Buffer_Size (Chan : Channel) return RFLX_Types.Length is
((case Chan is
when C_I_1 | C_I_2 | C_O =>
4096));
procedure Read (Chan : Channel; Buffer : out RFLX_Types.Bytes; Offset : RFLX_Types.Length := 0) is
function Read_Pre (Message_Buffer : RFLX_Types.Bytes) return Boolean is
(Buffer'Length > 0
and then Offset < Message_Buffer'Length);
procedure Read (Message_Buffer : RFLX_Types.Bytes) with
Pre =>
Read_Pre (Message_Buffer)
is
Length : constant RFLX_Types.Index := RFLX_Types.Index (RFLX_Types.Length'Min (Buffer'Length, Message_Buffer'Length - Offset));
Buffer_Last : constant RFLX_Types.Index := Buffer'First - 1 + Length;
begin
Buffer (Buffer'First .. RFLX_Types.Index (Buffer_Last)) := Message_Buffer (RFLX_Types.Index (RFLX_Types.Length (Message_Buffer'First) + Offset) .. Message_Buffer'First - 2 + RFLX_Types.Index (Offset + 1) + Length);
end Read;
procedure Universal_Message_Read is new Universal.Message.Generic_Read (Read, Read_Pre);
begin
Buffer := (others => RFLX_Types.Byte'First);
case Chan is
when C_O =>
case P_Next_State is
when S_Reply_1 =>
Universal_Message_Read (Message_1_Ctx);
when S_Reply_2 =>
Universal_Message_Read (Message_2_Ctx);
when others =>
raise Program_Error;
end case;
when others =>
raise Program_Error;
end case;
end Read;
procedure Write (Chan : Channel; Buffer : RFLX_Types.Bytes; Offset : RFLX_Types.Length := 0) is
function Write_Pre (Context_Buffer_Length : RFLX_Types.Length; Offset : RFLX_Types.Length) return Boolean is
(Buffer'Length > 0
and then Context_Buffer_Length = Write_Buffer_Size (Chan)
and then Offset <= RFLX_Types.Length'Last - Buffer'Length
and then Buffer'Length + Offset <= Write_Buffer_Size (Chan));
procedure Write (Message_Buffer : out RFLX_Types.Bytes; Length : out RFLX_Types.Length; Context_Buffer_Length : RFLX_Types.Length; Offset : RFLX_Types.Length) with
Pre =>
Write_Pre (Context_Buffer_Length, Offset)
and then Offset <= RFLX_Types.Length'Last - Message_Buffer'Length
and then Message_Buffer'Length + Offset = Write_Buffer_Size (Chan),
Post =>
Length <= Message_Buffer'Length
and Message_Buffer'Initialized,
Relaxed_Initialization =>
Message_Buffer
is
begin
Length := Buffer'Length;
Message_Buffer (Message_Buffer'First .. RFLX_Types.Index (RFLX_Types.Length (Message_Buffer'First) - 1 + Length)) := Buffer;
Message_Buffer (RFLX_Types.Index (RFLX_Types.Length (Message_Buffer'First) + Length) .. Message_Buffer'Last) := (others => 0);
end Write;
procedure Universal_Message_Write is new Universal.Message.Generic_Write (Write, Write_Pre);
begin
case Chan is
when C_I_1 =>
case P_Next_State is
when S_Start =>
Universal_Message_Write (Message_1_Ctx, Offset);
when others =>
raise Program_Error;
end case;
when C_I_2 =>
case P_Next_State is
when S_Start =>
Universal_Message_Write (Message_2_Ctx, Offset);
when others =>
raise Program_Error;
end case;
when C_O =>
raise Program_Error;
end case;
end Write;
end RFLX.Test.Session;
Raw
rflx-test-session.ads
--
-- Generated by RecordFlux 0.6.0-pre on 2021-10-25
--
-- Copyright (C) 2018-2021 Componolit GmbH
--
-- This file is distributed under the terms of the GNU Affero General Public License version 3.
--
pragma Style_Checks ("N3aAbcdefhiIklnOprStux");
pragma Warnings (Off, "redundant conversion");
with RFLX.Test.Session_Allocator;
with RFLX.RFLX_Types;
with RFLX.Universal;
with RFLX.Universal.Message;
generic
package RFLX.Test.Session with
SPARK_Mode,
Initial_Condition =>
Uninitialized
is
use type RFLX.RFLX_Types.Index;
use type RFLX.RFLX_Types.Length;
type Channel is (C_I_1, C_I_2, C_O);
type State is (S_Start, S_Reply_1, S_Reply_2, S_Error, S_Terminated);
function Uninitialized return Boolean;
function Initialized return Boolean;
function Active return Boolean;
procedure Initialize with
Pre =>
Uninitialized,
Post =>
Initialized
and Active;
procedure Finalize with
Pre =>
Initialized,
Post =>
Uninitialized
and not Active;
pragma Warnings (Off, "subprogram ""Tick"" has no effect");
procedure Tick with
Pre =>
Initialized,
Post =>
Initialized;
pragma Warnings (On, "subprogram ""Tick"" has no effect");
pragma Warnings (Off, "subprogram ""Run"" has no effect");
procedure Run with
Pre =>
Initialized,
Post =>
Initialized;
pragma Warnings (On, "subprogram ""Run"" has no effect");
function Next_State return State;
function Has_Data (Chan : Channel) return Boolean with
Pre =>
Initialized;
function Needs_Data (Chan : Channel) return Boolean with
Pre =>
Initialized;
function Read_Buffer_Size (Chan : Channel) return RFLX_Types.Length with
Pre =>
Initialized
and then Has_Data (Chan);
function Write_Buffer_Size (Chan : Channel) return RFLX_Types.Length;
procedure Read (Chan : Channel; Buffer : out RFLX_Types.Bytes; Offset : RFLX_Types.Length := 0) with
Pre =>
Initialized
and then Has_Data (Chan)
and then Buffer'Length > 0
and then Offset <= RFLX_Types.Length'Last - Buffer'Length
and then Buffer'Length + Offset <= Read_Buffer_Size (Chan),
Post =>
Initialized;
procedure Write (Chan : Channel; Buffer : RFLX_Types.Bytes; Offset : RFLX_Types.Length := 0) with
Pre =>
Initialized
and then Needs_Data (Chan)
and then Buffer'Length > 0
and then Offset <= RFLX_Types.Length'Last - Buffer'Length
and then Buffer'Length + Offset <= Write_Buffer_Size (Chan),
Post =>
Initialized;
private
P_Next_State : State := S_Start;
Message_1_Ctx : Universal.Message.Context;
Message_2_Ctx : Universal.Message.Context;
function Uninitialized return Boolean is
(not Universal.Message.Has_Buffer (Message_1_Ctx)
and not Universal.Message.Has_Buffer (Message_2_Ctx));
function Initialized return Boolean is
(Universal.Message.Has_Buffer (Message_1_Ctx)
and then Message_1_Ctx.Buffer_First = RFLX_Types.Index'First
and then Message_1_Ctx.Buffer_Last = RFLX_Types.Index'First + 4095
and then Universal.Message.Has_Buffer (Message_2_Ctx)
and then Message_2_Ctx.Buffer_First = RFLX_Types.Index'First
and then Message_2_Ctx.Buffer_Last = RFLX_Types.Index'First + 4095
and then Test.Session_Allocator.Global_Allocated);
function Active return Boolean is
(P_Next_State /= S_Terminated);
function Next_State return State is
(P_Next_State);
end RFLX.Test.Session;
Raw
rflx-test-session_allocator.adb
--
-- Generated by RecordFlux 0.6.0-pre on 2021-10-25
--
-- Copyright (C) 2018-2021 Componolit GmbH
--
-- This file is distributed under the terms of the GNU Affero General Public License version 3.
--
pragma Style_Checks ("N3aAbcdefhiIklnOprStux");
pragma Warnings (Off, "redundant conversion");
package body RFLX.Test.Session_Allocator with
SPARK_Mode
is
Slot_1 : aliased RFLX_Types.Bytes := (RFLX_Types.Index'First .. RFLX_Types.Index'First + 4095 => RFLX_Types.Byte'First);
Slot_2 : aliased RFLX_Types.Bytes := (RFLX_Types.Index'First .. RFLX_Types.Index'First + 4095 => RFLX_Types.Byte'First);
Slot_3 : aliased RFLX_Types.Bytes := (RFLX_Types.Index'First .. RFLX_Types.Index'First + 4095 => RFLX_Types.Byte'First);
procedure Initialize with
SPARK_Mode =>
Off
is
begin
Slot_Ptr_1 := Slot_1'Unrestricted_Access;
Slot_Ptr_2 := Slot_2'Unrestricted_Access;
Slot_Ptr_3 := Slot_3'Unrestricted_Access;
end Initialize;
end RFLX.Test.Session_Allocator;
Raw
rflx-test-session_allocator.ads
--
-- Generated by RecordFlux 0.6.0-pre on 2021-10-25
--
-- Copyright (C) 2018-2021 Componolit GmbH
--
-- This file is distributed under the terms of the GNU Affero General Public License version 3.
--
pragma Style_Checks ("N3aAbcdefhiIklnOprStux");
pragma Warnings (Off, "redundant conversion");
with RFLX.RFLX_Types;
use type RFLX.RFLX_Types.Index;
use type RFLX.RFLX_Types.Bytes_Ptr;
package RFLX.Test.Session_Allocator with
SPARK_Mode,
Annotate =>
(GNATprove, Terminating)
is
pragma Elaborate_Body;
subtype Slot_Ptr_Type is RFLX_Types.Bytes_Ptr with
Dynamic_Predicate =>
Slot_Ptr_Type = null
or else (Slot_Ptr_Type'First = RFLX_Types.Index'First
and then Slot_Ptr_Type'Last = RFLX_Types.Index'First + 4095);
Slot_Ptr_1 : Slot_Ptr_Type;
Slot_Ptr_2 : Slot_Ptr_Type;
Slot_Ptr_3 : Slot_Ptr_Type;
function Initialized return Boolean is
(Slot_Ptr_1 /= null
and Slot_Ptr_2 /= null
and Slot_Ptr_3 /= null);
procedure Initialize with
Post =>
Initialized;
function Global_Allocated return Boolean is
(Slot_Ptr_1 = null
and Slot_Ptr_2 = null
and Slot_Ptr_3 /= null);
end RFLX.Test.Session_Allocator;
Raw
rflx-test.ads
--
-- Generated by RecordFlux 0.6.0-pre on 2021-10-25
--
-- Copyright (C) 2018-2021 Componolit GmbH
--
-- This file is distributed under the terms of the GNU Affero General Public License version 3.
--
pragma Style_Checks ("N3aAbcdefhiIklnOprStux");
pragma Warnings (Off, "redundant conversion");
package RFLX.Test with
SPARK_Mode
is
end RFLX.Test;
Raw
rflx-universal-contains.adb
--
-- Generated by RecordFlux 0.6.0-pre on 2021-10-25
--
-- Copyright (C) 2018-2021 Componolit GmbH
--
-- This file is distributed under the terms of the GNU Affero General Public License version 3.
--
pragma Style_Checks ("N3aAbcdefhiIklnOprStux");
pragma Warnings (Off, "redundant conversion");
package body RFLX.Universal.Contains with
SPARK_Mode
is
procedure Switch_To_Data (Universal_Message_PDU_Context : in out RFLX.Universal.Message.Context; Universal_Option_SDU_Context : out RFLX.Universal.Option.Context) is
First : constant RFLX_Types.Bit_Index := RFLX.Universal.Message.Field_First (Universal_Message_PDU_Context, RFLX.Universal.Message.F_Data);
Last : constant RFLX_Types.Bit_Length := RFLX.Universal.Message.Field_Last (Universal_Message_PDU_Context, RFLX.Universal.Message.F_Data);
Buffer : RFLX_Types.Bytes_Ptr;
begin
RFLX.Universal.Message.Take_Buffer (Universal_Message_PDU_Context, Buffer);
pragma Warnings (Off, "unused assignment to ""Buffer""");
RFLX.Universal.Option.Initialize (Universal_Option_SDU_Context, Buffer, First, Last);
pragma Warnings (On, "unused assignment to ""Buffer""");
end Switch_To_Data;
procedure Copy_Data (Universal_Message_PDU_Context : RFLX.Universal.Message.Context; Universal_Option_SDU_Context : in out RFLX.Universal.Option.Context) is
First : constant RFLX_Types.Bit_Index := RFLX_Types.To_First_Bit_Index (Universal_Option_SDU_Context.Buffer_First);
Size : constant RFLX_Types.Bit_Index := RFLX.Universal.Message.Field_Size (Universal_Message_PDU_Context, RFLX.Universal.Message.F_Data);
Buffer : RFLX_Types.Bytes_Ptr;
begin
pragma Warnings (Off, """Universal_Option_SDU_Context"" is set by ""Take_Buffer"" but not used after the call");
RFLX.Universal.Option.Take_Buffer (Universal_Option_SDU_Context, Buffer);
pragma Warnings (On, """Universal_Option_SDU_Context"" is set by ""Take_Buffer"" but not used after the call");
RFLX.Universal.Message.Get_Data (Universal_Message_PDU_Context, Buffer.all);
RFLX.Universal.Option.Initialize (Universal_Option_SDU_Context, Buffer, First, First + Size - 1);
end Copy_Data;
end RFLX.Universal.Contains;
Raw
rflx-universal-contains.ads
--
-- Generated by RecordFlux 0.6.0-pre on 2021-10-25
--
-- Copyright (C) 2018-2021 Componolit GmbH
--
-- This file is distributed under the terms of the GNU Affero General Public License version 3.
--
pragma Style_Checks ("N3aAbcdefhiIklnOprStux");
pragma Warnings (Off, "redundant conversion");
with RFLX.RFLX_Types;
with RFLX.Universal.Message;
with RFLX.Universal.Option;
use RFLX.Universal.Option;
package RFLX.Universal.Contains with
SPARK_Mode,
Annotate =>
(GNATprove, Terminating)
is
use type RFLX_Types.Index;
use type RFLX_Types.Bit_Index;
function Option_In_Message_Data (Ctx : RFLX.Universal.Message.Context) return Boolean is
(RFLX.Universal.Message.Has_Buffer (Ctx)
and then RFLX.Universal.Message.Present (Ctx, RFLX.Universal.Message.F_Data));
use type RFLX.Universal.Message.Field_Cursors;
procedure Switch_To_Data (Universal_Message_PDU_Context : in out RFLX.Universal.Message.Context; Universal_Option_SDU_Context : out RFLX.Universal.Option.Context) with
Pre =>
not Universal_Message_PDU_Context'Constrained
and not Universal_Option_SDU_Context'Constrained
and RFLX.Universal.Message.Has_Buffer (Universal_Message_PDU_Context)
and RFLX.Universal.Message.Present (Universal_Message_PDU_Context, RFLX.Universal.Message.F_Data)
and Option_In_Message_Data (Universal_Message_PDU_Context),
Post =>
not RFLX.Universal.Message.Has_Buffer (Universal_Message_PDU_Context)
and RFLX.Universal.Option.Has_Buffer (Universal_Option_SDU_Context)
and Universal_Message_PDU_Context.Buffer_First = Universal_Option_SDU_Context.Buffer_First
and Universal_Message_PDU_Context.Buffer_Last = Universal_Option_SDU_Context.Buffer_Last
and Universal_Option_SDU_Context.First = RFLX.Universal.Message.Field_First (Universal_Message_PDU_Context, RFLX.Universal.Message.F_Data)
and Universal_Option_SDU_Context.Last = RFLX.Universal.Message.Field_Last (Universal_Message_PDU_Context, RFLX.Universal.Message.F_Data)
and RFLX.Universal.Option.Initialized (Universal_Option_SDU_Context)
and Universal_Message_PDU_Context.Buffer_First = Universal_Message_PDU_Context.Buffer_First'Old
and Universal_Message_PDU_Context.Buffer_Last = Universal_Message_PDU_Context.Buffer_Last'Old
and Universal_Message_PDU_Context.First = Universal_Message_PDU_Context.First'Old
and RFLX.Universal.Message.Context_Cursors (Universal_Message_PDU_Context) = RFLX.Universal.Message.Context_Cursors (Universal_Message_PDU_Context)'Old;
procedure Copy_Data (Universal_Message_PDU_Context : RFLX.Universal.Message.Context; Universal_Option_SDU_Context : in out RFLX.Universal.Option.Context) with
Pre =>
not Universal_Option_SDU_Context'Constrained
and then RFLX.Universal.Option.Has_Buffer (Universal_Option_SDU_Context)
and then RFLX.Universal.Message.Has_Buffer (Universal_Message_PDU_Context)
and then RFLX.Universal.Message.Present (Universal_Message_PDU_Context, RFLX.Universal.Message.F_Data)
and then Option_In_Message_Data (Universal_Message_PDU_Context)
and then RFLX_Types.To_Last_Bit_Index (Universal_Option_SDU_Context.Buffer_Last) - RFLX_Types.To_First_Bit_Index (Universal_Option_SDU_Context.Buffer_First) + 1 >= RFLX.Universal.Message.Field_Size (Universal_Message_PDU_Context, RFLX.Universal.Message.F_Data)
and then RFLX_Types.To_First_Bit_Index (Universal_Option_SDU_Context.Buffer_First) + RFLX.Universal.Message.Field_Size (Universal_Message_PDU_Context, RFLX.Universal.Message.F_Data) - 1 < RFLX_Types.Bit_Index'Last,
Post =>
RFLX.Universal.Message.Has_Buffer (Universal_Message_PDU_Context)
and RFLX.Universal.Option.Has_Buffer (Universal_Option_SDU_Context)
and RFLX.Universal.Option.Initialized (Universal_Option_SDU_Context)
and Universal_Option_SDU_Context.Buffer_First = Universal_Option_SDU_Context.Buffer_First'Old
and Universal_Option_SDU_Context.Buffer_Last = Universal_Option_SDU_Context.Buffer_Last'Old;
end RFLX.Universal.Contains;
Raw
rflx-universal-message.adb
--
-- Generated by RecordFlux 0.6.0-pre on 2021-10-25
--
-- Copyright (C) 2018-2021 Componolit GmbH
--
-- This file is distributed under the terms of the GNU Affero General Public License version 3.
--
pragma Style_Checks ("N3aAbcdefhiIklnOprStux");
pragma Warnings (Off, "redundant conversion");
package body RFLX.Universal.Message 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_Last, First, Last, First - 1, Buffer, (F_Message_Type => (State => S_Invalid, Predecessor => F_Initial), others => (State => S_Invalid, Predecessor => F_Final)));
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, Ctx.Buffer, (F_Message_Type => (State => S_Invalid, Predecessor => F_Initial), others => (State => S_Invalid, Predecessor => F_Final)));
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.Message_Last));
else
Buffer := Ctx.Buffer.all (RFLX_Types.Index'Last .. RFLX_Types.Index'First);
end if;
end Copy;
function Read (Ctx : Context) return RFLX_Types.Bytes is
(Ctx.Buffer.all (RFLX_Types.To_Index (Ctx.First) .. RFLX_Types.To_Index (Ctx.Message_Last)));
procedure Generic_Read (Ctx : Context) is
begin
Read (Read (Ctx));
end Generic_Read;
procedure Generic_Write (Ctx : in out Context; Offset : RFLX_Types.Length := 0) is
Length : RFLX_Types.Length;
begin
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""");
Reset (Ctx, RFLX_Types.To_First_Bit_Index (Ctx.Buffer_First), RFLX_Types.Bit_Index'Max (Ctx.Last, RFLX_Types.To_Last_Bit_Index (RFLX_Types.Length (Ctx.Buffer_First) + Offset + Length - 1)));
end Generic_Write;
function Size (Ctx : Context) return RFLX_Types.Bit_Length is
((if Ctx.Message_Last = Ctx.First - 1 then 0 else Ctx.Message_Last - Ctx.First + 1));
function Byte_Size (Ctx : Context) return RFLX_Types.Length is
((if
Ctx.Message_Last = Ctx.First - 1
then
0
else
RFLX_Types.Length (RFLX_Types.To_Index (Ctx.Message_Last) - RFLX_Types.To_Index (Ctx.First) + 1)));
pragma Warnings (Off, "precondition is always False");
function Successor (Ctx : Context; Fld : Field) return Virtual_Field is
((case Fld is
when F_Message_Type =>
(if
RFLX_Types.U64 (Ctx.Cursors (F_Message_Type).Value.Message_Type_Value) = RFLX_Types.U64 (To_Base (RFLX.Universal.MT_Unconstrained_Data))
then
F_Data
elsif
RFLX_Types.U64 (Ctx.Cursors (F_Message_Type).Value.Message_Type_Value) = RFLX_Types.U64 (To_Base (RFLX.Universal.MT_Null))
then
F_Final
elsif
RFLX_Types.U64 (Ctx.Cursors (F_Message_Type).Value.Message_Type_Value) /= RFLX_Types.U64 (To_Base (RFLX.Universal.MT_Unconstrained_Options))
and RFLX_Types.U64 (Ctx.Cursors (F_Message_Type).Value.Message_Type_Value) /= RFLX_Types.U64 (To_Base (RFLX.Universal.MT_Null))
and RFLX_Types.U64 (Ctx.Cursors (F_Message_Type).Value.Message_Type_Value) /= RFLX_Types.U64 (To_Base (RFLX.Universal.MT_Unconstrained_Data))
then
F_Length
elsif
RFLX_Types.U64 (Ctx.Cursors (F_Message_Type).Value.Message_Type_Value) = RFLX_Types.U64 (To_Base (RFLX.Universal.MT_Unconstrained_Options))
then
F_Options
else
F_Initial),
when F_Length =>
(if
RFLX_Types.U64 (Ctx.Cursors (F_Message_Type).Value.Message_Type_Value) = RFLX_Types.U64 (To_Base (RFLX.Universal.MT_Data))
then
F_Data
elsif
RFLX_Types.U64 (Ctx.Cursors (F_Message_Type).Value.Message_Type_Value) = RFLX_Types.U64 (To_Base (RFLX.Universal.MT_Option_Types))
then
F_Option_Types
elsif
RFLX_Types.U64 (Ctx.Cursors (F_Message_Type).Value.Message_Type_Value) = RFLX_Types.U64 (To_Base (RFLX.Universal.MT_Options))
then
F_Options
elsif
RFLX_Types.U64 (Ctx.Cursors (F_Message_Type).Value.Message_Type_Value) = RFLX_Types.U64 (To_Base (RFLX.Universal.MT_Value))
and RFLX_Types.U64 (Ctx.Cursors (F_Length).Value.Length_Value) = Universal.Value'Size / 8
then
F_Value
elsif
RFLX_Types.U64 (Ctx.Cursors (F_Message_Type).Value.Message_Type_Value) = RFLX_Types.U64 (To_Base (RFLX.Universal.MT_Values))
then
F_Values
else
F_Initial),
when F_Data | F_Option_Types | F_Options | F_Value | F_Values =>
F_Final))
with
Pre =>
Has_Buffer (Ctx)
and Structural_Valid (Ctx, Fld)
and Valid_Predecessor (Ctx, Fld);
pragma Warnings (On, "precondition is always False");
function Invalid_Successor (Ctx : Context; Fld : Field) return Boolean is
((case Fld is
when F_Message_Type =>
Invalid (Ctx.Cursors (F_Data))
and Invalid (Ctx.Cursors (F_Length))
and Invalid (Ctx.Cursors (F_Options)),
when F_Length =>
Invalid (Ctx.Cursors (F_Data))
and Invalid (Ctx.Cursors (F_Option_Types))
and Invalid (Ctx.Cursors (F_Options))
and Invalid (Ctx.Cursors (F_Value))
and Invalid (Ctx.Cursors (F_Values)),
when F_Data | F_Option_Types | F_Options | F_Value | F_Values =>
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 Available_Space (Ctx, Fld) >= Field_Size (Ctx, Fld))
with
Pre =>
Has_Buffer (Ctx)
and Valid_Next (Ctx, Fld);
function Equal (Ctx : Context; Fld : Field; Data : RFLX_Types.Bytes) return Boolean is
(Sufficient_Buffer_Length (Ctx, Fld)
and then (case Fld is
when F_Data | F_Option_Types | F_Options | F_Values =>
Ctx.Buffer.all (RFLX_Types.To_Index (Field_First (Ctx, Fld)) .. RFLX_Types.To_Index (Field_Last (Ctx, Fld))) = Data,
when others =>
False));
procedure Reset_Dependent_Fields (Ctx : in out Context; Fld : Field) with
Pre =>
Valid_Next (Ctx, Fld),
Post =>
Valid_Next (Ctx, Fld)
and Invalid (Ctx.Cursors (Fld))
and Invalid_Successor (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 Ctx.Cursors (Fld).Predecessor = Ctx.Cursors (Fld).Predecessor'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
First : constant RFLX_Types.Bit_Length := Field_First (Ctx, Fld) with
Ghost;
Size : constant RFLX_Types.Bit_Length := Field_Size (Ctx, Fld) with
Ghost;
begin
pragma Assert (Field_First (Ctx, Fld) = First
and Field_Size (Ctx, Fld) = Size);
case Fld is
when F_Message_Type =>
Ctx.Cursors (F_Values) := (S_Invalid, F_Final);
Ctx.Cursors (F_Value) := (S_Invalid, F_Final);
Ctx.Cursors (F_Options) := (S_Invalid, F_Final);
Ctx.Cursors (F_Option_Types) := (S_Invalid, F_Final);
Ctx.Cursors (F_Data) := (S_Invalid, F_Final);
Ctx.Cursors (F_Length) := (S_Invalid, F_Final);
Ctx.Cursors (F_Message_Type) := (S_Invalid, Ctx.Cursors (F_Message_Type).Predecessor);
pragma Assert (Field_First (Ctx, Fld) = First
and Field_Size (Ctx, Fld) = Size);
when F_Length =>
Ctx.Cursors (F_Values) := (S_Invalid, F_Final);
Ctx.Cursors (F_Value) := (S_Invalid, F_Final);
Ctx.Cursors (F_Options) := (S_Invalid, F_Final);
Ctx.Cursors (F_Option_Types) := (S_Invalid, F_Final);
Ctx.Cursors (F_Data) := (S_Invalid, F_Final);
Ctx.Cursors (F_Length) := (S_Invalid, Ctx.Cursors (F_Length).Predecessor);
pragma Assert (Field_First (Ctx, Fld) = First
and Field_Size (Ctx, Fld) = Size);
when F_Data =>
Ctx.Cursors (F_Values) := (S_Invalid, F_Final);
Ctx.Cursors (F_Value) := (S_Invalid, F_Final);
Ctx.Cursors (F_Options) := (S_Invalid, F_Final);
Ctx.Cursors (F_Option_Types) := (S_Invalid, F_Final);
Ctx.Cursors (F_Data) := (S_Invalid, Ctx.Cursors (F_Data).Predecessor);
pragma Assert (Field_First (Ctx, Fld) = First
and Field_Size (Ctx, Fld) = Size);
when F_Option_Types =>
Ctx.Cursors (F_Values) := (S_Invalid, F_Final);
Ctx.Cursors (F_Value) := (S_Invalid, F_Final);
Ctx.Cursors (F_Options) := (S_Invalid, F_Final);
Ctx.Cursors (F_Option_Types) := (S_Invalid, Ctx.Cursors (F_Option_Types).Predecessor);
pragma Assert (Field_First (Ctx, Fld) = First
and Field_Size (Ctx, Fld) = Size);
when F_Options =>
Ctx.Cursors (F_Values) := (S_Invalid, F_Final);
Ctx.Cursors (F_Value) := (S_Invalid, F_Final);
Ctx.Cursors (F_Options) := (S_Invalid, Ctx.Cursors (F_Options).Predecessor);
pragma Assert (Field_First (Ctx, Fld) = First
and Field_Size (Ctx, Fld) = Size);
when F_Value =>
Ctx.Cursors (F_Values) := (S_Invalid, F_Final);
Ctx.Cursors (F_Value) := (S_Invalid, Ctx.Cursors (F_Value).Predecessor);
pragma Assert (Field_First (Ctx, Fld) = First
and Field_Size (Ctx, Fld) = Size);
when F_Values =>
Ctx.Cursors (F_Values) := (S_Invalid, Ctx.Cursors (F_Values).Predecessor);
pragma Assert (Field_First (Ctx, Fld) = First
and Field_Size (Ctx, Fld) = Size);
end case;
end Reset_Dependent_Fields;
function Composite_Field (Fld : Field) return Boolean is
((case Fld is
when F_Message_Type | F_Length =>
False,
when F_Data | F_Option_Types | F_Options =>
True,
when F_Value =>
False,
when F_Values =>
True));
function Get_Field_Value (Ctx : Context; Fld : Field) return Field_Dependent_Value with
Pre =>
Has_Buffer (Ctx)
and then Valid_Next (Ctx, Fld)
and then Sufficient_Buffer_Length (Ctx, Fld),
Post =>
Get_Field_Value'Result.Fld = Fld
is
First : constant RFLX_Types.Bit_Index := Field_First (Ctx, Fld);
Last : constant RFLX_Types.Bit_Index := Field_Last (Ctx, Fld);
function Buffer_First return RFLX_Types.Index is
(RFLX_Types.To_Index (First));
function Buffer_Last return RFLX_Types.Index is
(RFLX_Types.To_Index (Last));
function Offset return RFLX_Types.Offset is
(RFLX_Types.Offset ((8 - Last mod 8) mod 8));
function Extract is new RFLX_Types.Extract (RFLX.Universal.Message_Type_Base);
function Extract is new RFLX_Types.Extract (RFLX.Universal.Length_Base);
function Extract is new RFLX_Types.Extract (RFLX.Universal.Value);
begin
return ((case Fld is
when F_Message_Type =>
(Fld => F_Message_Type, Message_Type_Value => Extract (Ctx.Buffer.all (Buffer_First .. Buffer_Last), Offset)),
when F_Length =>
(Fld => F_Length, Length_Value => Extract (Ctx.Buffer.all (Buffer_First .. Buffer_Last), Offset)),
when F_Data =>
(Fld => F_Data),
when F_Option_Types =>
(Fld => F_Option_Types),
when F_Options =>
(Fld => F_Options),
when F_Value =>
(Fld => F_Value, Value_Value => Extract (Ctx.Buffer.all (Buffer_First .. Buffer_Last), Offset)),
when F_Values =>
(Fld => F_Values)));
end Get_Field_Value;
procedure Verify (Ctx : in out Context; Fld : Field) is
Value : Field_Dependent_Value;
begin
if
Has_Buffer (Ctx)
and then Invalid (Ctx.Cursors (Fld))
and then Valid_Predecessor (Ctx, Fld)
and then Path_Condition (Ctx, Fld)
then
if Sufficient_Buffer_Length (Ctx, Fld) then
Value := Get_Field_Value (Ctx, Fld);
if
Valid_Value (Value)
and Field_Condition (Ctx, Value)
then
pragma Assert ((if
Fld = F_Data
or Fld = F_Message_Type
or Fld = F_Option_Types
or Fld = F_Options
or Fld = F_Value
or Fld = F_Values
then
Field_Last (Ctx, Fld) mod RFLX_Types.Byte'Size = 0));
case Fld is
when F_Message_Type =>
Ctx.Message_Last := ((Field_Last (Ctx, Fld) + 7) / 8) * 8;
when F_Length =>
Ctx.Message_Last := ((Field_Last (Ctx, Fld) + 7) / 8) * 8;
when F_Data =>
Ctx.Message_Last := ((Field_Last (Ctx, Fld) + 7) / 8) * 8;
when F_Option_Types =>
Ctx.Message_Last := ((Field_Last (Ctx, Fld) + 7) / 8) * 8;
when F_Options =>
Ctx.Message_Last := ((Field_Last (Ctx, Fld) + 7) / 8) * 8;
when F_Value =>
Ctx.Message_Last := ((Field_Last (Ctx, Fld) + 7) / 8) * 8;
when F_Values =>
Ctx.Message_Last := ((Field_Last (Ctx, Fld) + 7) / 8) * 8;
end case;
if Composite_Field (Fld) then
Ctx.Cursors (Fld) := (State => S_Structural_Valid, First => Field_First (Ctx, Fld), Last => Field_Last (Ctx, Fld), Value => Value, Predecessor => Ctx.Cursors (Fld).Predecessor);
else
Ctx.Cursors (Fld) := (State => S_Valid, First => Field_First (Ctx, Fld), Last => Field_Last (Ctx, Fld), Value => Value, Predecessor => Ctx.Cursors (Fld).Predecessor);
end if;
if Fld = F_Message_Type then
Ctx.Cursors (Successor (Ctx, Fld)) := (State => S_Invalid, Predecessor => Fld);
elsif Fld = F_Length then
Ctx.Cursors (Successor (Ctx, Fld)) := (State => S_Invalid, Predecessor => Fld);
elsif Fld = F_Data then
Ctx.Cursors (Successor (Ctx, Fld)) := (State => S_Invalid, Predecessor => Fld);
elsif Fld = F_Option_Types then
Ctx.Cursors (Successor (Ctx, Fld)) := (State => S_Invalid, Predecessor => Fld);
elsif Fld = F_Options then
Ctx.Cursors (Successor (Ctx, Fld)) := (State => S_Invalid, Predecessor => Fld);
elsif Fld = F_Value then
Ctx.Cursors (Successor (Ctx, Fld)) := (State => S_Invalid, Predecessor => Fld);
elsif Fld = F_Values then
Ctx.Cursors (Successor (Ctx, Fld)) := (State => S_Invalid, Predecessor => Fld);
end if;
else
Ctx.Cursors (Fld) := (State => S_Invalid, Predecessor => F_Final);
end if;
else
Ctx.Cursors (Fld) := (State => S_Incomplete, Predecessor => F_Final);
end if;
end if;
end Verify;
procedure Verify_Message (Ctx : in out Context) is
begin
Verify (Ctx, F_Message_Type);
Verify (Ctx, F_Length);
Verify (Ctx, F_Data);
Verify (Ctx, F_Option_Types);
Verify (Ctx, F_Options);
Verify (Ctx, F_Value);
Verify (Ctx, F_Values);
end Verify_Message;
function Get_Data (Ctx : Context) return RFLX_Types.Bytes is
First : constant RFLX_Types.Index := RFLX_Types.To_Index (Ctx.Cursors (F_Data).First);
Last : constant RFLX_Types.Index := RFLX_Types.To_Index (Ctx.Cursors (F_Data).Last);
begin
return Ctx.Buffer.all (First .. Last);
end Get_Data;
procedure Get_Data (Ctx : Context; Data : out RFLX_Types.Bytes) is
First : constant RFLX_Types.Index := RFLX_Types.To_Index (Ctx.Cursors (F_Data).First);
Last : constant RFLX_Types.Index := RFLX_Types.To_Index (Ctx.Cursors (F_Data).Last);
begin
Data := (others => RFLX_Types.Byte'First);
Data (Data'First .. Data'First + (Last - First)) := Ctx.Buffer.all (First .. Last);
end Get_Data;
procedure Generic_Get_Data (Ctx : Context) is
First : constant RFLX_Types.Index := RFLX_Types.To_Index (Ctx.Cursors (F_Data).First);
Last : constant RFLX_Types.Index := RFLX_Types.To_Index (Ctx.Cursors (F_Data).Last);
begin
Process_Data (Ctx.Buffer.all (First .. Last));
end Generic_Get_Data;
procedure Set_Field_Value (Ctx : in out Context; Val : Field_Dependent_Value; Fst, Lst : out RFLX_Types.Bit_Index) with
Pre =>
not Ctx'Constrained
and then Has_Buffer (Ctx)
and then Val.Fld in Field'Range
and then Valid_Next (Ctx, Val.Fld)
and then Available_Space (Ctx, Val.Fld) >= Field_Size (Ctx, Val.Fld)
and then (for all F in Field'Range =>
(if Structural_Valid (Ctx.Cursors (F)) then Ctx.Cursors (F).Last <= Field_Last (Ctx, Val.Fld))),
Post =>
Has_Buffer (Ctx)
and Fst = Field_First (Ctx, Val.Fld)
and Lst = Field_Last (Ctx, Val.Fld)
and Fst >= Ctx.First
and Fst <= Lst + 1
and Lst <= Ctx.Last
and (for all F in Field'Range =>
(if Structural_Valid (Ctx.Cursors (F)) then Ctx.Cursors (F).Last <= Lst))
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 Ctx.Cursors = Ctx.Cursors'Old
is
First : constant RFLX_Types.Bit_Index := Field_First (Ctx, Val.Fld);
Last : constant RFLX_Types.Bit_Index := Field_Last (Ctx, Val.Fld);
function Buffer_First return RFLX_Types.Index is
(RFLX_Types.To_Index (First));
function Buffer_Last return RFLX_Types.Index is
(RFLX_Types.To_Index (Last));
function Offset return RFLX_Types.Offset is
(RFLX_Types.Offset ((8 - Last mod 8) mod 8));
procedure Insert is new RFLX_Types.Insert (RFLX.Universal.Message_Type_Base);
procedure Insert is new RFLX_Types.Insert (RFLX.Universal.Length_Base);
procedure Insert is new RFLX_Types.Insert (RFLX.Universal.Value);
begin
Fst := First;
Lst := Last;
case Val.Fld is
when F_Initial =>
null;
when F_Message_Type =>
Insert (Val.Message_Type_Value, Ctx.Buffer.all (Buffer_First .. Buffer_Last), Offset);
when F_Length =>
Insert (Val.Length_Value, Ctx.Buffer.all (Buffer_First .. Buffer_Last), Offset);
when F_Data | F_Option_Types | F_Options =>
null;
when F_Value =>
Insert (Val.Value_Value, Ctx.Buffer.all (Buffer_First .. Buffer_Last), Offset);
when F_Values | F_Final =>
null;
end case;
end Set_Field_Value;
procedure Set_Message_Type (Ctx : in out Context; Val : RFLX.Universal.Message_Type) is
Field_Value : constant Field_Dependent_Value := (F_Message_Type, To_Base (Val));
First, Last : RFLX_Types.Bit_Index;
begin
Reset_Dependent_Fields (Ctx, F_Message_Type);
Set_Field_Value (Ctx, Field_Value, First, Last);
Ctx.Message_Last := Last;
Ctx.Cursors (F_Message_Type) := (State => S_Valid, First => First, Last => Last, Value => Field_Value, Predecessor => Ctx.Cursors (F_Message_Type).Predecessor);
Ctx.Cursors (Successor (Ctx, F_Message_Type)) := (State => S_Invalid, Predecessor => F_Message_Type);
end Set_Message_Type;
procedure Set_Length (Ctx : in out Context; Val : RFLX.Universal.Length) is
Field_Value : constant Field_Dependent_Value := (F_Length, To_Base (Val));
First, Last : RFLX_Types.Bit_Index;
begin
Reset_Dependent_Fields (Ctx, F_Length);
Set_Field_Value (Ctx, Field_Value, First, Last);
Ctx.Message_Last := ((Last + 7) / 8) * 8;
Ctx.Cursors (F_Length) := (State => S_Valid, First => First, Last => Last, Value => Field_Value, Predecessor => Ctx.Cursors (F_Length).Predecessor);
Ctx.Cursors (Successor (Ctx, F_Length)) := (State => S_Invalid, Predecessor => F_Length);
end Set_Length;
procedure Set_Value (Ctx : in out Context; Val : RFLX.Universal.Value) is
Field_Value : constant Field_Dependent_Value := (F_Value, To_Base (Val));
First, Last : RFLX_Types.Bit_Index;
begin
Reset_Dependent_Fields (Ctx, F_Value);
Set_Field_Value (Ctx, Field_Value, First, Last);
Ctx.Message_Last := Last;
Ctx.Cursors (F_Value) := (State => S_Valid, First => First, Last => Last, Value => Field_Value, Predecessor => Ctx.Cursors (F_Value).Predecessor);
Ctx.Cursors (Successor (Ctx, F_Value)) := (State => S_Invalid, Predecessor => F_Value);
end Set_Value;
procedure Set_Data_Empty (Ctx : in out Context) is
First : constant RFLX_Types.Bit_Index := Field_First (Ctx, F_Data);
Last : constant RFLX_Types.Bit_Index := Field_Last (Ctx, F_Data);
begin
Reset_Dependent_Fields (Ctx, F_Data);
Ctx.Message_Last := Last;
Ctx.Cursors (F_Data) := (State => S_Valid, First => First, Last => Last, Value => (Fld => F_Data), Predecessor => Ctx.Cursors (F_Data).Predecessor);
Ctx.Cursors (Successor (Ctx, F_Data)) := (State => S_Invalid, Predecessor => F_Data);
end Set_Data_Empty;
procedure Set_Option_Types_Empty (Ctx : in out Context) is
First : constant RFLX_Types.Bit_Index := Field_First (Ctx, F_Option_Types);
Last : constant RFLX_Types.Bit_Index := Field_Last (Ctx, F_Option_Types);
begin
Reset_Dependent_Fields (Ctx, F_Option_Types);
Ctx.Message_Last := Last;
Ctx.Cursors (F_Option_Types) := (State => S_Valid, First => First, Last => Last, Value => (Fld => F_Option_Types), Predecessor => Ctx.Cursors (F_Option_Types).Predecessor);
Ctx.Cursors (Successor (Ctx, F_Option_Types)) := (State => S_Invalid, Predecessor => F_Option_Types);
end Set_Option_Types_Empty;
procedure Set_Options_Empty (Ctx : in out Context) is
First : constant RFLX_Types.Bit_Index := Field_First (Ctx, F_Options);
Last : constant RFLX_Types.Bit_Index := Field_Last (Ctx, F_Options);
begin
Reset_Dependent_Fields (Ctx, F_Options);
Ctx.Message_Last := Last;
Ctx.Cursors (F_Options) := (State => S_Valid, First => First, Last => Last, Value => (Fld => F_Options), Predecessor => Ctx.Cursors (F_Options).Predecessor);
Ctx.Cursors (Successor (Ctx, F_Options)) := (State => S_Invalid, Predecessor => F_Options);
end Set_Options_Empty;
procedure Set_Values_Empty (Ctx : in out Context) is
First : constant RFLX_Types.Bit_Index := Field_First (Ctx, F_Values);
Last : constant RFLX_Types.Bit_Index := Field_Last (Ctx, F_Values);
begin
Reset_Dependent_Fields (Ctx, F_Values);
Ctx.Message_Last := Last;
Ctx.Cursors (F_Values) := (State => S_Valid, First => First, Last => Last, Value => (Fld => F_Values), Predecessor => Ctx.Cursors (F_Values).Predecessor);
Ctx.Cursors (Successor (Ctx, F_Values)) := (State => S_Invalid, Predecessor => F_Values);
end Set_Values_Empty;
procedure Set_Option_Types (Ctx : in out Context; Seq_Ctx : Universal.Option_Types.Context) is
First : constant RFLX_Types.Bit_Index := Field_First (Ctx, F_Option_Types);
Last : constant RFLX_Types.Bit_Index := Field_Last (Ctx, F_Option_Types);
function Buffer_First return RFLX_Types.Index is
(RFLX_Types.To_Index (First));
function Buffer_Last return RFLX_Types.Index is
(RFLX_Types.To_Index (Last));
begin
Reset_Dependent_Fields (Ctx, F_Option_Types);
Ctx.Message_Last := Last;
Ctx.Cursors (F_Option_Types) := (State => S_Valid, First => First, Last => Last, Value => (Fld => F_Option_Types), Predecessor => Ctx.Cursors (F_Option_Types).Predecessor);
Ctx.Cursors (Successor (Ctx, F_Option_Types)) := (State => S_Invalid, Predecessor => F_Option_Types);
Universal.Option_Types.Copy (Seq_Ctx, Ctx.Buffer.all (Buffer_First .. Buffer_Last));
end Set_Option_Types;
procedure Set_Options (Ctx : in out Context; Seq_Ctx : Universal.Options.Context) is
First : constant RFLX_Types.Bit_Index := Field_First (Ctx, F_Options);
Last : constant RFLX_Types.Bit_Index := Field_Last (Ctx, F_Options);
function Buffer_First return RFLX_Types.Index is
(RFLX_Types.To_Index (First));
function Buffer_Last return RFLX_Types.Index is
(RFLX_Types.To_Index (Last));
begin
Reset_Dependent_Fields (Ctx, F_Options);
Ctx.Message_Last := Last;
Ctx.Cursors (F_Options) := (State => S_Valid, First => First, Last => Last, Value => (Fld => F_Options), Predecessor => Ctx.Cursors (F_Options).Predecessor);
Ctx.Cursors (Successor (Ctx, F_Options)) := (State => S_Invalid, Predecessor => F_Options);
Universal.Options.Copy (Seq_Ctx, Ctx.Buffer.all (Buffer_First .. Buffer_Last));
end Set_Options;
procedure Set_Values (Ctx : in out Context; Seq_Ctx : Universal.Values.Context) is
First : constant RFLX_Types.Bit_Index := Field_First (Ctx, F_Values);
Last : constant RFLX_Types.Bit_Index := Field_Last (Ctx, F_Values);
function Buffer_First return RFLX_Types.Index is
(RFLX_Types.To_Index (First));
function Buffer_Last return RFLX_Types.Index is
(RFLX_Types.To_Index (Last));
begin
Reset_Dependent_Fields (Ctx, F_Values);
Ctx.Message_Last := Last;
Ctx.Cursors (F_Values) := (State => S_Valid, First => First, Last => Last, Value => (Fld => F_Values), Predecessor => Ctx.Cursors (F_Values).Predecessor);
Ctx.Cursors (Successor (Ctx, F_Values)) := (State => S_Invalid, Predecessor => F_Values);
Universal.Values.Copy (Seq_Ctx, Ctx.Buffer.all (Buffer_First .. Buffer_Last));
end Set_Values;
procedure Initialize_Data_Private (Ctx : in out Context) with
Pre =>
not Ctx'Constrained
and then Has_Buffer (Ctx)
and then Valid_Next (Ctx, F_Data)
and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data)
and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1
and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0
and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0,
Post =>
Has_Buffer (Ctx)
and Structural_Valid (Ctx, F_Data)
and Ctx.Message_Last = Field_Last (Ctx, F_Data)
and Invalid (Ctx, F_Option_Types)
and Invalid (Ctx, F_Options)
and Invalid (Ctx, F_Value)
and Invalid (Ctx, F_Values)
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 Predecessor (Ctx, F_Data) = Predecessor (Ctx, F_Data)'Old
and Valid_Next (Ctx, F_Data) = Valid_Next (Ctx, F_Data)'Old
and Get_Message_Type (Ctx) = Get_Message_Type (Ctx)'Old
is
First : constant RFLX_Types.Bit_Index := Field_First (Ctx, F_Data);
Last : constant RFLX_Types.Bit_Index := Field_Last (Ctx, F_Data);
begin
Reset_Dependent_Fields (Ctx, F_Data);
Ctx.Message_Last := Last;
Ctx.Cursors (F_Data) := (State => S_Structural_Valid, First => First, Last => Last, Value => (Fld => F_Data), Predecessor => Ctx.Cursors (F_Data).Predecessor);
Ctx.Cursors (Successor (Ctx, F_Data)) := (State => S_Invalid, Predecessor => F_Data);
end Initialize_Data_Private;
procedure Initialize_Data (Ctx : in out Context) is
begin
Initialize_Data_Private (Ctx);
end Initialize_Data;
procedure Set_Data (Ctx : in out Context; Data : RFLX_Types.Bytes) is
First : constant RFLX_Types.Bit_Index := Field_First (Ctx, F_Data);
Last : constant RFLX_Types.Bit_Index := Field_Last (Ctx, F_Data);
function Buffer_First return RFLX_Types.Index is
(RFLX_Types.To_Index (First));
function Buffer_Last return RFLX_Types.Index is
(RFLX_Types.To_Index (Last));
begin
Initialize_Data_Private (Ctx);
Ctx.Buffer.all (Buffer_First .. Buffer_Last) := Data;
end Set_Data;
procedure Generic_Set_Data (Ctx : in out Context) is
First : constant RFLX_Types.Bit_Index := Field_First (Ctx, F_Data);
Last : constant RFLX_Types.Bit_Index := Field_Last (Ctx, F_Data);
function Buffer_First return RFLX_Types.Index is
(RFLX_Types.To_Index (First));
function Buffer_Last return RFLX_Types.Index is
(RFLX_Types.To_Index (Last));
begin
Initialize_Data_Private (Ctx);
Process_Data (Ctx.Buffer.all (Buffer_First .. Buffer_Last));
end Generic_Set_Data;
procedure Switch_To_Option_Types (Ctx : in out Context; Seq_Ctx : out Universal.Option_Types.Context) is
First : constant RFLX_Types.Bit_Index := Field_First (Ctx, F_Option_Types);
Last : constant RFLX_Types.Bit_Index := Field_Last (Ctx, F_Option_Types);
Buffer : RFLX_Types.Bytes_Ptr;
begin
if Invalid (Ctx, F_Option_Types) then
Reset_Dependent_Fields (Ctx, F_Option_Types);
Ctx.Message_Last := Last;
Ctx.Cursors (F_Option_Types) := (State => S_Structural_Valid, First => First, Last => Last, Value => (Fld => F_Option_Types), Predecessor => Ctx.Cursors (F_Option_Types).Predecessor);
Ctx.Cursors (Successor (Ctx, F_Option_Types)) := (State => S_Invalid, Predecessor => F_Option_Types);
end if;
Take_Buffer (Ctx, Buffer);
pragma Warnings (Off, "unused assignment to ""Buffer""");
Universal.Option_Types.Initialize (Seq_Ctx, Buffer, First, Last);
pragma Warnings (On, "unused assignment to ""Buffer""");
end Switch_To_Option_Types;
procedure Switch_To_Options (Ctx : in out Context; Seq_Ctx : out Universal.Options.Context) is
First : constant RFLX_Types.Bit_Index := Field_First (Ctx, F_Options);
Last : constant RFLX_Types.Bit_Index := Field_Last (Ctx, F_Options);
Buffer : RFLX_Types.Bytes_Ptr;
begin
if Invalid (Ctx, F_Options) then
Reset_Dependent_Fields (Ctx, F_Options);
Ctx.Message_Last := Last;
Ctx.Cursors (F_Options) := (State => S_Structural_Valid, First => First, Last => Last, Value => (Fld => F_Options), Predecessor => Ctx.Cursors (F_Options).Predecessor);
Ctx.Cursors (Successor (Ctx, F_Options)) := (State => S_Invalid, Predecessor => F_Options);
end if;
Take_Buffer (Ctx, Buffer);
pragma Warnings (Off, "unused assignment to ""Buffer""");
Universal.Options.Initialize (Seq_Ctx, Buffer, First, Last);
pragma Warnings (On, "unused assignment to ""Buffer""");
end Switch_To_Options;
procedure Switch_To_Values (Ctx : in out Context; Seq_Ctx : out Universal.Values.Context) is
First : constant RFLX_Types.Bit_Index := Field_First (Ctx, F_Values);
Last : constant RFLX_Types.Bit_Index := Field_Last (Ctx, F_Values);
Buffer : RFLX_Types.Bytes_Ptr;
begin
if Invalid (Ctx, F_Values) then
Reset_Dependent_Fields (Ctx, F_Values);
Ctx.Message_Last := Last;
Ctx.Cursors (F_Values) := (State => S_Structural_Valid, First => First, Last => Last, Value => (Fld => F_Values), Predecessor => Ctx.Cursors (F_Values).Predecessor);
Ctx.Cursors (Successor (Ctx, F_Values)) := (State => S_Invalid, Predecessor => F_Values);
end if;
Take_Buffer (Ctx, Buffer);
pragma Warnings (Off, "unused assignment to ""Buffer""");
Universal.Values.Initialize (Seq_Ctx, Buffer, First, Last);
pragma Warnings (On, "unused assignment to ""Buffer""");
end Switch_To_Values;
procedure Update_Option_Types (Ctx : in out Context; Seq_Ctx : in out Universal.Option_Types.Context) is
Valid_Sequence : constant Boolean := Universal.Option_Types.Valid (Seq_Ctx);
Buffer : RFLX_Types.Bytes_Ptr;
begin
Universal.Option_Types.Take_Buffer (Seq_Ctx, Buffer);
Ctx.Buffer := Buffer;
if Valid_Sequence then
Ctx.Cursors (F_Option_Types) := (State => S_Valid, First => Ctx.Cursors (F_Option_Types).First, Last => Ctx.Cursors (F_Option_Types).Last, Value => Ctx.Cursors (F_Option_Types).Value, Predecessor => Ctx.Cursors (F_Option_Types).Predecessor);
end if;
end Update_Option_Types;
procedure Update_Options (Ctx : in out Context; Seq_Ctx : in out Universal.Options.Context) is
Valid_Sequence : constant Boolean := Universal.Options.Valid (Seq_Ctx);
Buffer : RFLX_Types.Bytes_Ptr;
begin
Universal.Options.Take_Buffer (Seq_Ctx, Buffer);
Ctx.Buffer := Buffer;
if Valid_Sequence then
Ctx.Cursors (F_Options) := (State => S_Valid, First => Ctx.Cursors (F_Options).First, Last => Ctx.Cursors (F_Options).Last, Value => Ctx.Cursors (F_Options).Value, Predecessor => Ctx.Cursors (F_Options).Predecessor);
end if;
end Update_Options;
procedure Update_Values (Ctx : in out Context; Seq_Ctx : in out Universal.Values.Context) is
Valid_Sequence : constant Boolean := Universal.Values.Valid (Seq_Ctx);
Buffer : RFLX_Types.Bytes_Ptr;
begin
Universal.Values.Take_Buffer (Seq_Ctx, Buffer);
Ctx.Buffer := Buffer;
if Valid_Sequence then
Ctx.Cursors (F_Values) := (State => S_Valid, First => Ctx.Cursors (F_Values).First, Last => Ctx.Cursors (F_Values).Last, Value => Ctx.Cursors (F_Values).Value, Predecessor => Ctx.Cursors (F_Values).Predecessor);
end if;
end Update_Values;
end RFLX.Universal.Message;
Raw
rflx-universal-message.ads
--
-- Generated by RecordFlux 0.6.0-pre on 2021-10-25
--
-- Copyright (C) 2018-2021 Componolit GmbH
--
-- This file is distributed under the terms of the GNU Affero General Public License version 3.
--
pragma Style_Checks ("N3aAbcdefhiIklnOprStux");
pragma Warnings (Off, "redundant conversion");
with RFLX.RFLX_Types;
with RFLX.Universal.Option_Types;
with RFLX.Universal.Options;
with RFLX.Universal.Values;
package RFLX.Universal.Message with
SPARK_Mode,
Annotate =>
(GNATprove, Terminating)
is
pragma Warnings (Off, "use clause for type ""U64"" * has no effect");
pragma Warnings (Off, """LENGTH"" is already use-visible through previous use_type_clause");
use type RFLX_Types.Bytes;
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.U64;
pragma Warnings (On, """LENGTH"" is already use-visible through previous use_type_clause");
pragma Warnings (On, "use clause for type ""U64"" * has no effect");
type Virtual_Field is (F_Initial, F_Message_Type, F_Length, F_Data, F_Option_Types, F_Options, F_Value, F_Values, F_Final);
subtype Field is Virtual_Field range F_Message_Type .. F_Values;
type Field_Cursor is private with
Default_Initial_Condition =>
False;
type Field_Cursors is private with
Default_Initial_Condition =>
False;
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 mod RFLX_Types.Byte'Size = 1
and Last mod RFLX_Types.Byte'Size = 0;
type Field_Dependent_Value (Fld : Virtual_Field := F_Initial) is
record
case Fld is
when F_Initial | F_Data | F_Option_Types | F_Options | F_Values | F_Final =>
null;
when F_Message_Type =>
Message_Type_Value : RFLX.Universal.Message_Type_Base;
when F_Length =>
Length_Value : RFLX.Universal.Length_Base;
when F_Value =>
Value_Value : RFLX.Universal.Value;
end case;
end record;
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 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, 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_Index'Last
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 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), Buffer => null);
function Initialized (Ctx : Context) return Boolean with
Ghost;
procedure Reset (Ctx : in out Context) with
Pre =>
not Ctx'Constrained
and 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 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 mod RFLX_Types.Byte'Size = 1
and Last mod 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 =>
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 =>
Has_Buffer (Ctx)
and then Structural_Valid_Message (Ctx)
and then Byte_Size (Ctx) = Buffer'Length;
function Read (Ctx : Context) return RFLX_Types.Bytes with
Pre =>
Has_Buffer (Ctx)
and then Structural_Valid_Message (Ctx);
pragma Warnings (Off, "formal parameter ""*"" is not referenced");
function Always_Valid (Buffer : RFLX_Types.Bytes) return Boolean is
(True)
with
Ghost;
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 =>
Has_Buffer (Ctx)
and then Structural_Valid_Message (Ctx)
and then Pre (Read (Ctx));
pragma Warnings (Off, "formal parameter ""*"" is not referenced");
function Always_Valid (Context_Buffer_Length : RFLX_Types.Length; Offset : RFLX_Types.Length) return Boolean is
(True)
with
Ghost;
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 Has_Buffer (Ctx)
and then Offset < Buffer_Length (Ctx)
and then Pre (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 =>
Has_Buffer (Ctx);
function Size (Ctx : Context) return RFLX_Types.Bit_Length;
function Byte_Size (Ctx : Context) return RFLX_Types.Length;
function Message_Last (Ctx : Context) return RFLX_Types.Bit_Length with
Pre =>
Has_Buffer (Ctx)
and then Structural_Valid_Message (Ctx);
function Message_Data (Ctx : Context) return RFLX_Types.Bytes with
Pre =>
Has_Buffer (Ctx)
and then Structural_Valid_Message (Ctx),
Post =>
Message_Data'Result'Length = Byte_Size (Ctx);
function Path_Condition (Ctx : Context; Fld : Field) return Boolean with
Pre =>
Valid_Predecessor (Ctx, Fld);
function Field_Condition (Ctx : Context; Val : Field_Dependent_Value) return Boolean with
Pre =>
Has_Buffer (Ctx)
and Val.Fld in Field'Range
and Valid_Predecessor (Ctx, Val.Fld);
function Field_Size (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Length with
Pre =>
Valid_Next (Ctx, Fld);
function Field_First (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with
Pre =>
Valid_Next (Ctx, Fld);
function Field_Last (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with
Pre =>
Valid_Next (Ctx, Fld)
and then Available_Space (Ctx, Fld) >= Field_Size (Ctx, Fld);
function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field;
function Valid_Predecessor (Ctx : Context; Fld : Virtual_Field) return Boolean;
function Valid_Next (Ctx : Context; Fld : Field) return Boolean;
function Available_Space (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Length with
Pre =>
Valid_Next (Ctx, Fld);
function Equal (Ctx : Context; Fld : Field; Data : RFLX_Types.Bytes) return Boolean with
Pre =>
Has_Buffer (Ctx)
and Valid_Next (Ctx, Fld);
procedure Verify (Ctx : in out Context; Fld : Field) with
Post =>
Has_Buffer (Ctx) = Has_Buffer (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;
procedure Verify_Message (Ctx : in out Context) with
Post =>
Has_Buffer (Ctx) = Has_Buffer (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;
function Present (Ctx : Context; Fld : Field) return Boolean;
function Structural_Valid (Ctx : Context; Fld : Field) return Boolean;
function Valid (Ctx : Context; Fld : Field) return Boolean with
Post =>
(if Valid'Result then Structural_Valid (Ctx, Fld) and Present (Ctx, Fld));
function Incomplete (Ctx : Context; Fld : Field) return Boolean;
function Invalid (Ctx : Context; Fld : Field) return Boolean;
function Structural_Valid_Message (Ctx : Context) return Boolean with
Pre =>
Has_Buffer (Ctx);
function Valid_Message (Ctx : Context) return Boolean with
Pre =>
Has_Buffer (Ctx);
function Incomplete_Message (Ctx : Context) return Boolean;
pragma Warnings (Off, "precondition is always False");
function Get_Message_Type (Ctx : Context) return RFLX.Universal.Message_Type with
Pre =>
Valid (Ctx, F_Message_Type);
function Get_Length (Ctx : Context) return RFLX.Universal.Length with
Pre =>
Valid (Ctx, F_Length);
function Get_Value (Ctx : Context) return RFLX.Universal.Value with
Pre =>
Valid (Ctx, F_Value);
pragma Warnings (On, "precondition is always False");
function Get_Data (Ctx : Context) return RFLX_Types.Bytes with
Pre =>
Has_Buffer (Ctx)
and then Structural_Valid (Ctx, F_Data)
and then Valid_Next (Ctx, F_Data),
Post =>
Get_Data'Result'Length = RFLX_Types.To_Length (Field_Size (Ctx, F_Data));
procedure Get_Data (Ctx : Context; Data : out RFLX_Types.Bytes) with
Pre =>
Has_Buffer (Ctx)
and then Structural_Valid (Ctx, F_Data)
and then Valid_Next (Ctx, F_Data)
and then Data'Length >= RFLX_Types.To_Length (Field_Size (Ctx, F_Data));
generic
with procedure Process_Data (Data : RFLX_Types.Bytes);
procedure Generic_Get_Data (Ctx : Context) with
Pre =>
Has_Buffer (Ctx)
and Present (Ctx, F_Data);
procedure Set_Message_Type (Ctx : in out Context; Val : RFLX.Universal.Message_Type) with
Pre =>
not Ctx'Constrained
and then Has_Buffer (Ctx)
and then Valid_Next (Ctx, F_Message_Type)
and then Field_Condition (Ctx, (F_Message_Type, To_Base (Val)))
and then True
and then Available_Space (Ctx, F_Message_Type) >= Field_Size (Ctx, F_Message_Type),
Post =>
Has_Buffer (Ctx)
and Valid (Ctx, F_Message_Type)
and Get_Message_Type (Ctx) = Val
and (if Structural_Valid_Message (Ctx) then Message_Last (Ctx) = Field_Last (Ctx, F_Message_Type))
and Invalid (Ctx, F_Length)
and Invalid (Ctx, F_Data)
and Invalid (Ctx, F_Option_Types)
and Invalid (Ctx, F_Options)
and Invalid (Ctx, F_Value)
and Invalid (Ctx, F_Values)
and (if
RFLX_Types.U64 (To_Base (Get_Message_Type (Ctx))) = RFLX_Types.U64 (To_Base (RFLX.Universal.MT_Unconstrained_Data))
then
Predecessor (Ctx, F_Data) = F_Message_Type
and Valid_Next (Ctx, F_Data))
and (if
RFLX_Types.U64 (To_Base (Get_Message_Type (Ctx))) /= RFLX_Types.U64 (To_Base (RFLX.Universal.MT_Unconstrained_Options))
and RFLX_Types.U64 (To_Base (Get_Message_Type (Ctx))) /= RFLX_Types.U64 (To_Base (RFLX.Universal.MT_Null))
and RFLX_Types.U64 (To_Base (Get_Message_Type (Ctx))) /= RFLX_Types.U64 (To_Base (RFLX.Universal.MT_Unconstrained_Data))
then
Predecessor (Ctx, F_Length) = F_Message_Type
and Valid_Next (Ctx, F_Length))
and (if
RFLX_Types.U64 (To_Base (Get_Message_Type (Ctx))) = RFLX_Types.U64 (To_Base (RFLX.Universal.MT_Unconstrained_Options))
then
Predecessor (Ctx, F_Options) = F_Message_Type
and Valid_Next (Ctx, F_Options))
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 Predecessor (Ctx, F_Message_Type) = Predecessor (Ctx, F_Message_Type)'Old
and Valid_Next (Ctx, F_Message_Type) = Valid_Next (Ctx, F_Message_Type)'Old;
procedure Set_Length (Ctx : in out Context; Val : RFLX.Universal.Length) with
Pre =>
not Ctx'Constrained
and then Has_Buffer (Ctx)
and then Valid_Next (Ctx, F_Length)
and then Field_Condition (Ctx, (F_Length, To_Base (Val)))
and then Valid (To_Base (Val))
and then Available_Space (Ctx, F_Length) >= Field_Size (Ctx, F_Length),
Post =>
Has_Buffer (Ctx)
and Valid (Ctx, F_Length)
and Get_Length (Ctx) = Val
and Invalid (Ctx, F_Data)
and Invalid (Ctx, F_Option_Types)
and Invalid (Ctx, F_Options)
and Invalid (Ctx, F_Value)
and Invalid (Ctx, F_Values)
and (if
RFLX_Types.U64 (To_Base (Get_Message_Type (Ctx))) = RFLX_Types.U64 (To_Base (RFLX.Universal.MT_Data))
then
Predecessor (Ctx, F_Data) = F_Length
and Valid_Next (Ctx, F_Data))
and (if
RFLX_Types.U64 (To_Base (Get_Message_Type (Ctx))) = RFLX_Types.U64 (To_Base (RFLX.Universal.MT_Option_Types))
then
Predecessor (Ctx, F_Option_Types) = F_Length
and Valid_Next (Ctx, F_Option_Types))
and (if
RFLX_Types.U64 (To_Base (Get_Message_Type (Ctx))) = RFLX_Types.U64 (To_Base (RFLX.Universal.MT_Options))
then
Predecessor (Ctx, F_Options) = F_Length
and Valid_Next (Ctx, F_Options))
and (if
RFLX_Types.U64 (To_Base (Get_Message_Type (Ctx))) = RFLX_Types.U64 (To_Base (RFLX.Universal.MT_Value))
and RFLX_Types.U64 (Get_Length (Ctx)) = Universal.Value'Size / 8
then
Predecessor (Ctx, F_Value) = F_Length
and Valid_Next (Ctx, F_Value))
and (if
RFLX_Types.U64 (To_Base (Get_Message_Type (Ctx))) = RFLX_Types.U64 (To_Base (RFLX.Universal.MT_Values))
then
Predecessor (Ctx, F_Values) = F_Length
and Valid_Next (Ctx, F_Values))
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 Predecessor (Ctx, F_Length) = Predecessor (Ctx, F_Length)'Old
and Valid_Next (Ctx, F_Length) = Valid_Next (Ctx, F_Length)'Old
and Get_Message_Type (Ctx) = Get_Message_Type (Ctx)'Old
and Context_Cursor (Ctx, F_Message_Type) = Context_Cursor (Ctx, F_Message_Type)'Old;
procedure Set_Value (Ctx : in out Context; Val : RFLX.Universal.Value) with
Pre =>
not Ctx'Constrained
and then Has_Buffer (Ctx)
and then Valid_Next (Ctx, F_Value)
and then Field_Condition (Ctx, (F_Value, To_Base (Val)))
and then Valid (To_Base (Val))
and then Available_Space (Ctx, F_Value) >= Field_Size (Ctx, F_Value),
Post =>
Has_Buffer (Ctx)
and Valid (Ctx, F_Value)
and Get_Value (Ctx) = Val
and (if Structural_Valid_Message (Ctx) then Message_Last (Ctx) = Field_Last (Ctx, F_Value))
and Invalid (Ctx, F_Values)
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 Predecessor (Ctx, F_Value) = Predecessor (Ctx, F_Value)'Old
and Valid_Next (Ctx, F_Value) = Valid_Next (Ctx, F_Value)'Old
and Get_Message_Type (Ctx) = Get_Message_Type (Ctx)'Old
and Get_Length (Ctx) = Get_Length (Ctx)'Old
and Context_Cursor (Ctx, F_Message_Type) = Context_Cursor (Ctx, F_Message_Type)'Old
and Context_Cursor (Ctx, F_Length) = Context_Cursor (Ctx, F_Length)'Old
and Context_Cursor (Ctx, F_Data) = Context_Cursor (Ctx, F_Data)'Old
and Context_Cursor (Ctx, F_Option_Types) = Context_Cursor (Ctx, F_Option_Types)'Old
and Context_Cursor (Ctx, F_Options) = Context_Cursor (Ctx, F_Options)'Old;
procedure Set_Data_Empty (Ctx : in out Context) with
Pre =>
not Ctx'Constrained
and then Has_Buffer (Ctx)
and then Valid_Next (Ctx, F_Data)
and then Field_Condition (Ctx, (Fld => F_Data))
and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data)
and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1
and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0
and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0
and then Field_Size (Ctx, F_Data) = 0,
Post =>
Has_Buffer (Ctx)
and Structural_Valid (Ctx, F_Data)
and (if Structural_Valid_Message (Ctx) then Message_Last (Ctx) = Field_Last (Ctx, F_Data))
and Invalid (Ctx, F_Option_Types)
and Invalid (Ctx, F_Options)
and Invalid (Ctx, F_Value)
and Invalid (Ctx, F_Values)
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 Predecessor (Ctx, F_Data) = Predecessor (Ctx, F_Data)'Old
and Valid_Next (Ctx, F_Data) = Valid_Next (Ctx, F_Data)'Old
and Get_Message_Type (Ctx) = Get_Message_Type (Ctx)'Old;
procedure Set_Option_Types_Empty (Ctx : in out Context) with
Pre =>
not Ctx'Constrained
and then Has_Buffer (Ctx)
and then Valid_Next (Ctx, F_Option_Types)
and then Field_Condition (Ctx, (Fld => F_Option_Types))
and then Available_Space (Ctx, F_Option_Types) >= Field_Size (Ctx, F_Option_Types)
and then Field_First (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 1
and then Field_Last (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 0
and then Field_Size (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 0
and then Field_Size (Ctx, F_Option_Types) = 0,
Post =>
Has_Buffer (Ctx)
and Structural_Valid (Ctx, F_Option_Types)
and (if Structural_Valid_Message (Ctx) then Message_Last (Ctx) = Field_Last (Ctx, F_Option_Types))
and Invalid (Ctx, F_Options)
and Invalid (Ctx, F_Value)
and Invalid (Ctx, F_Values)
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 Predecessor (Ctx, F_Option_Types) = Predecessor (Ctx, F_Option_Types)'Old
and Valid_Next (Ctx, F_Option_Types) = Valid_Next (Ctx, F_Option_Types)'Old
and Get_Message_Type (Ctx) = Get_Message_Type (Ctx)'Old
and Get_Length (Ctx) = Get_Length (Ctx)'Old;
procedure Set_Options_Empty (Ctx : in out Context) with
Pre =>
not Ctx'Constrained
and then Has_Buffer (Ctx)
and then Valid_Next (Ctx, F_Options)
and then Field_Condition (Ctx, (Fld => F_Options))
and then Available_Space (Ctx, F_Options) >= Field_Size (Ctx, F_Options)
and then Field_First (Ctx, F_Options) mod RFLX_Types.Byte'Size = 1
and then Field_Last (Ctx, F_Options) mod RFLX_Types.Byte'Size = 0
and then Field_Size (Ctx, F_Options) mod RFLX_Types.Byte'Size = 0
and then Field_Size (Ctx, F_Options) = 0,
Post =>
Has_Buffer (Ctx)
and Structural_Valid (Ctx, F_Options)
and (if Structural_Valid_Message (Ctx) then Message_Last (Ctx) = Field_Last (Ctx, F_Options))
and Invalid (Ctx, F_Value)
and Invalid (Ctx, F_Values)
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 Predecessor (Ctx, F_Options) = Predecessor (Ctx, F_Options)'Old
and Valid_Next (Ctx, F_Options) = Valid_Next (Ctx, F_Options)'Old
and Get_Message_Type (Ctx) = Get_Message_Type (Ctx)'Old;
procedure Set_Values_Empty (Ctx : in out Context) with
Pre =>
not Ctx'Constrained
and then Has_Buffer (Ctx)
and then Valid_Next (Ctx, F_Values)
and then Field_Condition (Ctx, (Fld => F_Values))
and then Available_Space (Ctx, F_Values) >= Field_Size (Ctx, F_Values)
and then Field_First (Ctx, F_Values) mod RFLX_Types.Byte'Size = 1
and then Field_Last (Ctx, F_Values) mod RFLX_Types.Byte'Size = 0
and then Field_Size (Ctx, F_Values) mod RFLX_Types.Byte'Size = 0
and then Field_Size (Ctx, F_Values) = 0,
Post =>
Has_Buffer (Ctx)
and Structural_Valid (Ctx, F_Values)
and (if Structural_Valid_Message (Ctx) then Message_Last (Ctx) = Field_Last (Ctx, F_Values))
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 Predecessor (Ctx, F_Values) = Predecessor (Ctx, F_Values)'Old
and Valid_Next (Ctx, F_Values) = Valid_Next (Ctx, F_Values)'Old
and Get_Message_Type (Ctx) = Get_Message_Type (Ctx)'Old
and Get_Length (Ctx) = Get_Length (Ctx)'Old;
procedure Set_Option_Types (Ctx : in out Context; Seq_Ctx : Universal.Option_Types.Context) with
Pre =>
not Ctx'Constrained
and then Has_Buffer (Ctx)
and then Valid_Next (Ctx, F_Option_Types)
and then Field_Condition (Ctx, (Fld => F_Option_Types))
and then Available_Space (Ctx, F_Option_Types) >= Field_Size (Ctx, F_Option_Types)
and then Field_First (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 1
and then Field_Last (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 0
and then Field_Size (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 0
and then Field_Size (Ctx, F_Option_Types) = Universal.Option_Types.Size (Seq_Ctx)
and then Universal.Option_Types.Has_Buffer (Seq_Ctx)
and then Universal.Option_Types.Valid (Seq_Ctx),
Post =>
Has_Buffer (Ctx)
and Structural_Valid (Ctx, F_Option_Types)
and (if Structural_Valid_Message (Ctx) then Message_Last (Ctx) = Field_Last (Ctx, F_Option_Types))
and Invalid (Ctx, F_Options)
and Invalid (Ctx, F_Value)
and Invalid (Ctx, F_Values)
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 Predecessor (Ctx, F_Option_Types) = Predecessor (Ctx, F_Option_Types)'Old
and Valid_Next (Ctx, F_Option_Types) = Valid_Next (Ctx, F_Option_Types)'Old
and Get_Message_Type (Ctx) = Get_Message_Type (Ctx)'Old
and Get_Length (Ctx) = Get_Length (Ctx)'Old
and (if Field_Size (Ctx, F_Option_Types) > 0 then Present (Ctx, F_Option_Types));
procedure Set_Options (Ctx : in out Context; Seq_Ctx : Universal.Options.Context) with
Pre =>
not Ctx'Constrained
and then Has_Buffer (Ctx)
and then Valid_Next (Ctx, F_Options)
and then Field_Condition (Ctx, (Fld => F_Options))
and then Available_Space (Ctx, F_Options) >= Field_Size (Ctx, F_Options)
and then Field_First (Ctx, F_Options) mod RFLX_Types.Byte'Size = 1
and then Field_Last (Ctx, F_Options) mod RFLX_Types.Byte'Size = 0
and then Field_Size (Ctx, F_Options) mod RFLX_Types.Byte'Size = 0
and then Field_Size (Ctx, F_Options) = Universal.Options.Size (Seq_Ctx)
and then Universal.Options.Has_Buffer (Seq_Ctx)
and then Universal.Options.Valid (Seq_Ctx),
Post =>
Has_Buffer (Ctx)
and Structural_Valid (Ctx, F_Options)
and (if Structural_Valid_Message (Ctx) then Message_Last (Ctx) = Field_Last (Ctx, F_Options))
and Invalid (Ctx, F_Value)
and Invalid (Ctx, F_Values)
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 Predecessor (Ctx, F_Options) = Predecessor (Ctx, F_Options)'Old
and Valid_Next (Ctx, F_Options) = Valid_Next (Ctx, F_Options)'Old
and Get_Message_Type (Ctx) = Get_Message_Type (Ctx)'Old
and (if Field_Size (Ctx, F_Options) > 0 then Present (Ctx, F_Options));
procedure Set_Values (Ctx : in out Context; Seq_Ctx : Universal.Values.Context) with
Pre =>
not Ctx'Constrained
and then Has_Buffer (Ctx)
and then Valid_Next (Ctx, F_Values)
and then Field_Condition (Ctx, (Fld => F_Values))
and then Available_Space (Ctx, F_Values) >= Field_Size (Ctx, F_Values)
and then Field_First (Ctx, F_Values) mod RFLX_Types.Byte'Size = 1
and then Field_Last (Ctx, F_Values) mod RFLX_Types.Byte'Size = 0
and then Field_Size (Ctx, F_Values) mod RFLX_Types.Byte'Size = 0
and then Field_Size (Ctx, F_Values) = Universal.Values.Size (Seq_Ctx)
and then Universal.Values.Has_Buffer (Seq_Ctx)
and then Universal.Values.Valid (Seq_Ctx),
Post =>
Has_Buffer (Ctx)
and Structural_Valid (Ctx, F_Values)
and (if Structural_Valid_Message (Ctx) then Message_Last (Ctx) = Field_Last (Ctx, F_Values))
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 Predecessor (Ctx, F_Values) = Predecessor (Ctx, F_Values)'Old
and Valid_Next (Ctx, F_Values) = Valid_Next (Ctx, F_Values)'Old
and Get_Message_Type (Ctx) = Get_Message_Type (Ctx)'Old
and Get_Length (Ctx) = Get_Length (Ctx)'Old
and (if Field_Size (Ctx, F_Values) > 0 then Present (Ctx, F_Values));
procedure Initialize_Data (Ctx : in out Context) with
Pre =>
not Ctx'Constrained
and then Has_Buffer (Ctx)
and then Valid_Next (Ctx, F_Data)
and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data)
and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1
and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0
and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0,
Post =>
Has_Buffer (Ctx)
and Structural_Valid (Ctx, F_Data)
and (if Structural_Valid_Message (Ctx) then Message_Last (Ctx) = Field_Last (Ctx, F_Data))
and Invalid (Ctx, F_Option_Types)
and Invalid (Ctx, F_Options)
and Invalid (Ctx, F_Value)
and Invalid (Ctx, F_Values)
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 Predecessor (Ctx, F_Data) = Predecessor (Ctx, F_Data)'Old
and Valid_Next (Ctx, F_Data) = Valid_Next (Ctx, F_Data)'Old
and Get_Message_Type (Ctx) = Get_Message_Type (Ctx)'Old;
procedure Set_Data (Ctx : in out Context; Data : RFLX_Types.Bytes) with
Pre =>
not Ctx'Constrained
and then Has_Buffer (Ctx)
and then Valid_Next (Ctx, F_Data)
and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data)
and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1
and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0
and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0
and then Data'Length = RFLX_Types.To_Length (Field_Size (Ctx, F_Data))
and then Field_Condition (Ctx, (Fld => F_Data)),
Post =>
Has_Buffer (Ctx)
and Structural_Valid (Ctx, F_Data)
and (if Structural_Valid_Message (Ctx) then Message_Last (Ctx) = Field_Last (Ctx, F_Data))
and Invalid (Ctx, F_Option_Types)
and Invalid (Ctx, F_Options)
and Invalid (Ctx, F_Value)
and Invalid (Ctx, F_Values)
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 Predecessor (Ctx, F_Data) = Predecessor (Ctx, F_Data)'Old
and Valid_Next (Ctx, F_Data) = Valid_Next (Ctx, F_Data)'Old
and Get_Message_Type (Ctx) = Get_Message_Type (Ctx)'Old;
generic
with procedure Process_Data (Data : out RFLX_Types.Bytes);
with function Valid_Length (Length : RFLX_Types.Length) return Boolean;
procedure Generic_Set_Data (Ctx : in out Context) with
Pre =>
not Ctx'Constrained
and then Has_Buffer (Ctx)
and then Valid_Next (Ctx, F_Data)
and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data)
and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1
and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0
and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0
and then Valid_Length (RFLX_Types.Length (Field_Size (Ctx, F_Data) / RFLX_Types.Byte'Size)),
Post =>
Has_Buffer (Ctx)
and Structural_Valid (Ctx, F_Data)
and (if Structural_Valid_Message (Ctx) then Message_Last (Ctx) = Field_Last (Ctx, F_Data))
and Invalid (Ctx, F_Option_Types)
and Invalid (Ctx, F_Options)
and Invalid (Ctx, F_Value)
and Invalid (Ctx, F_Values)
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 Predecessor (Ctx, F_Data) = Predecessor (Ctx, F_Data)'Old
and Valid_Next (Ctx, F_Data) = Valid_Next (Ctx, F_Data)'Old
and Get_Message_Type (Ctx) = Get_Message_Type (Ctx)'Old;
procedure Switch_To_Option_Types (Ctx : in out Context; Seq_Ctx : out Universal.Option_Types.Context) with
Pre =>
not Ctx'Constrained
and then not Seq_Ctx'Constrained
and then Has_Buffer (Ctx)
and then Valid_Next (Ctx, F_Option_Types)
and then Field_Size (Ctx, F_Option_Types) > 0
and then Field_First (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 1
and then Field_Condition (Ctx, (Fld => F_Option_Types))
and then Available_Space (Ctx, F_Option_Types) >= Field_Size (Ctx, F_Option_Types),
Post =>
not Has_Buffer (Ctx)
and Universal.Option_Types.Has_Buffer (Seq_Ctx)
and Ctx.Buffer_First = Seq_Ctx.Buffer_First
and Ctx.Buffer_Last = Seq_Ctx.Buffer_Last
and Seq_Ctx.First = Field_First (Ctx, F_Option_Types)
and Seq_Ctx.Last = Field_Last (Ctx, F_Option_Types)
and Universal.Option_Types.Valid (Seq_Ctx)
and Universal.Option_Types.Sequence_Last (Seq_Ctx) = Seq_Ctx.First - 1
and Present (Ctx, F_Option_Types)
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 Predecessor (Ctx, F_Option_Types) = Predecessor (Ctx, F_Option_Types)'Old
and Path_Condition (Ctx, F_Option_Types) = Path_Condition (Ctx, F_Option_Types)'Old
and Context_Cursor (Ctx, F_Message_Type) = Context_Cursor (Ctx, F_Message_Type)'Old
and Context_Cursor (Ctx, F_Length) = Context_Cursor (Ctx, F_Length)'Old
and Context_Cursor (Ctx, F_Data) = Context_Cursor (Ctx, F_Data)'Old,
Contract_Cases =>
(Structural_Valid (Ctx, F_Option_Types) =>
Context_Cursor (Ctx, F_Options) = Context_Cursor (Ctx, F_Options)'Old
and Context_Cursor (Ctx, F_Value) = Context_Cursor (Ctx, F_Value)'Old
and Context_Cursor (Ctx, F_Values) = Context_Cursor (Ctx, F_Values)'Old,
others =>
Invalid (Ctx, F_Options)
and Invalid (Ctx, F_Value)
and Invalid (Ctx, F_Values));
procedure Switch_To_Options (Ctx : in out Context; Seq_Ctx : out Universal.Options.Context) with
Pre =>
not Ctx'Constrained
and then not Seq_Ctx'Constrained
and then Has_Buffer (Ctx)
and then Valid_Next (Ctx, F_Options)
and then Field_Size (Ctx, F_Options) > 0
and then Field_First (Ctx, F_Options) mod RFLX_Types.Byte'Size = 1
and then Field_Condition (Ctx, (Fld => F_Options))
and then Available_Space (Ctx, F_Options) >= Field_Size (Ctx, F_Options),
Post =>
not Has_Buffer (Ctx)
and Universal.Options.Has_Buffer (Seq_Ctx)
and Ctx.Buffer_First = Seq_Ctx.Buffer_First
and Ctx.Buffer_Last = Seq_Ctx.Buffer_Last
and Seq_Ctx.First = Field_First (Ctx, F_Options)
and Seq_Ctx.Last = Field_Last (Ctx, F_Options)
and Universal.Options.Valid (Seq_Ctx)
and Universal.Options.Sequence_Last (Seq_Ctx) = Seq_Ctx.First - 1
and Present (Ctx, F_Options)
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 Predecessor (Ctx, F_Options) = Predecessor (Ctx, F_Options)'Old
and Path_Condition (Ctx, F_Options) = Path_Condition (Ctx, F_Options)'Old
and Context_Cursor (Ctx, F_Message_Type) = Context_Cursor (Ctx, F_Message_Type)'Old
and Context_Cursor (Ctx, F_Length) = Context_Cursor (Ctx, F_Length)'Old
and Context_Cursor (Ctx, F_Data) = Context_Cursor (Ctx, F_Data)'Old
and Context_Cursor (Ctx, F_Option_Types) = Context_Cursor (Ctx, F_Option_Types)'Old,
Contract_Cases =>
(Structural_Valid (Ctx, F_Options) =>
Context_Cursor (Ctx, F_Value) = Context_Cursor (Ctx, F_Value)'Old
and Context_Cursor (Ctx, F_Values) = Context_Cursor (Ctx, F_Values)'Old,
others =>
Invalid (Ctx, F_Value)
and Invalid (Ctx, F_Values));
procedure Switch_To_Values (Ctx : in out Context; Seq_Ctx : out Universal.Values.Context) with
Pre =>
not Ctx'Constrained
and then not Seq_Ctx'Constrained
and then Has_Buffer (Ctx)
and then Valid_Next (Ctx, F_Values)
and then Field_Size (Ctx, F_Values) > 0
and then Field_First (Ctx, F_Values) mod RFLX_Types.Byte'Size = 1
and then Field_Condition (Ctx, (Fld => F_Values))
and then Available_Space (Ctx, F_Values) >= Field_Size (Ctx, F_Values),
Post =>
not Has_Buffer (Ctx)
and Universal.Values.Has_Buffer (Seq_Ctx)
and Ctx.Buffer_First = Seq_Ctx.Buffer_First
and Ctx.Buffer_Last = Seq_Ctx.Buffer_Last
and Seq_Ctx.First = Field_First (Ctx, F_Values)
and Seq_Ctx.Last = Field_Last (Ctx, F_Values)
and Universal.Values.Valid (Seq_Ctx)
and Universal.Values.Sequence_Last (Seq_Ctx) = Seq_Ctx.First - 1
and Present (Ctx, F_Values)
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 Predecessor (Ctx, F_Values) = Predecessor (Ctx, F_Values)'Old
and Path_Condition (Ctx, F_Values) = Path_Condition (Ctx, F_Values)'Old
and Context_Cursor (Ctx, F_Message_Type) = Context_Cursor (Ctx, F_Message_Type)'Old
and Context_Cursor (Ctx, F_Length) = Context_Cursor (Ctx, F_Length)'Old
and Context_Cursor (Ctx, F_Data) = Context_Cursor (Ctx, F_Data)'Old
and Context_Cursor (Ctx, F_Option_Types) = Context_Cursor (Ctx, F_Option_Types)'Old
and Context_Cursor (Ctx, F_Options) = Context_Cursor (Ctx, F_Options)'Old
and Context_Cursor (Ctx, F_Value) = Context_Cursor (Ctx, F_Value)'Old,
Contract_Cases =>
(Structural_Valid (Ctx, F_Values) =>
True,
others =>
True);
function Complete_Option_Types (Ctx : Context; Seq_Ctx : Universal.Option_Types.Context) return Boolean with
Pre =>
Valid_Next (Ctx, F_Option_Types);
function Complete_Options (Ctx : Context; Seq_Ctx : Universal.Options.Context) return Boolean with
Pre =>
Valid_Next (Ctx, F_Options);
function Complete_Values (Ctx : Context; Seq_Ctx : Universal.Values.Context) return Boolean with
Pre =>
Valid_Next (Ctx, F_Values);
procedure Update_Option_Types (Ctx : in out Context; Seq_Ctx : in out Universal.Option_Types.Context) with
Pre =>
Present (Ctx, F_Option_Types)
and then Complete_Option_Types (Ctx, Seq_Ctx)
and then not Has_Buffer (Ctx)
and then Universal.Option_Types.Has_Buffer (Seq_Ctx)
and then Ctx.Buffer_First = Seq_Ctx.Buffer_First
and then Ctx.Buffer_Last = Seq_Ctx.Buffer_Last
and then Seq_Ctx.First = Field_First (Ctx, F_Option_Types)
and then Seq_Ctx.Last = Field_Last (Ctx, F_Option_Types),
Post =>
Present (Ctx, F_Option_Types)
and Has_Buffer (Ctx)
and not Universal.Option_Types.Has_Buffer (Seq_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 Seq_Ctx.First = Seq_Ctx.First'Old
and Seq_Ctx.Last = Seq_Ctx.Last'Old
and Field_First (Ctx, F_Option_Types) = Field_First (Ctx, F_Option_Types)'Old
and Field_Size (Ctx, F_Option_Types) = Field_Size (Ctx, F_Option_Types)'Old
and Context_Cursor (Ctx, F_Message_Type) = Context_Cursor (Ctx, F_Message_Type)'Old
and Context_Cursor (Ctx, F_Length) = Context_Cursor (Ctx, F_Length)'Old
and Context_Cursor (Ctx, F_Data) = Context_Cursor (Ctx, F_Data)'Old
and Context_Cursor (Ctx, F_Options) = Context_Cursor (Ctx, F_Options)'Old
and Context_Cursor (Ctx, F_Value) = Context_Cursor (Ctx, F_Value)'Old
and Context_Cursor (Ctx, F_Values) = Context_Cursor (Ctx, F_Values)'Old,
Depends =>
(Ctx => (Ctx, Seq_Ctx), Seq_Ctx => Seq_Ctx);
procedure Update_Options (Ctx : in out Context; Seq_Ctx : in out Universal.Options.Context) with
Pre =>
Present (Ctx, F_Options)
and then Complete_Options (Ctx, Seq_Ctx)
and then not Has_Buffer (Ctx)
and then Universal.Options.Has_Buffer (Seq_Ctx)
and then Ctx.Buffer_First = Seq_Ctx.Buffer_First
and then Ctx.Buffer_Last = Seq_Ctx.Buffer_Last
and then Seq_Ctx.First = Field_First (Ctx, F_Options)
and then Seq_Ctx.Last = Field_Last (Ctx, F_Options),
Post =>
Present (Ctx, F_Options)
and Has_Buffer (Ctx)
and not Universal.Options.Has_Buffer (Seq_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 Seq_Ctx.First = Seq_Ctx.First'Old
and Seq_Ctx.Last = Seq_Ctx.Last'Old
and Field_First (Ctx, F_Options) = Field_First (Ctx, F_Options)'Old
and Field_Size (Ctx, F_Options) = Field_Size (Ctx, F_Options)'Old
and Context_Cursor (Ctx, F_Message_Type) = Context_Cursor (Ctx, F_Message_Type)'Old
and Context_Cursor (Ctx, F_Length) = Context_Cursor (Ctx, F_Length)'Old
and Context_Cursor (Ctx, F_Data) = Context_Cursor (Ctx, F_Data)'Old
and Context_Cursor (Ctx, F_Option_Types) = Context_Cursor (Ctx, F_Option_Types)'Old
and Context_Cursor (Ctx, F_Value) = Context_Cursor (Ctx, F_Value)'Old
and Context_Cursor (Ctx, F_Values) = Context_Cursor (Ctx, F_Values)'Old,
Depends =>
(Ctx => (Ctx, Seq_Ctx), Seq_Ctx => Seq_Ctx);
procedure Update_Values (Ctx : in out Context; Seq_Ctx : in out Universal.Values.Context) with
Pre =>
Present (Ctx, F_Values)
and then Complete_Values (Ctx, Seq_Ctx)
and then not Has_Buffer (Ctx)
and then Universal.Values.Has_Buffer (Seq_Ctx)
and then Ctx.Buffer_First = Seq_Ctx.Buffer_First
and then Ctx.Buffer_Last = Seq_Ctx.Buffer_Last
and then Seq_Ctx.First = Field_First (Ctx, F_Values)
and then Seq_Ctx.Last = Field_Last (Ctx, F_Values),
Post =>
Present (Ctx, F_Values)
and Has_Buffer (Ctx)
and not Universal.Values.Has_Buffer (Seq_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 Seq_Ctx.First = Seq_Ctx.First'Old
and Seq_Ctx.Last = Seq_Ctx.Last'Old
and Field_First (Ctx, F_Values) = Field_First (Ctx, F_Values)'Old
and Field_Size (Ctx, F_Values) = Field_Size (Ctx, F_Values)'Old
and Context_Cursor (Ctx, F_Message_Type) = Context_Cursor (Ctx, F_Message_Type)'Old
and Context_Cursor (Ctx, F_Length) = Context_Cursor (Ctx, F_Length)'Old
and Context_Cursor (Ctx, F_Data) = Context_Cursor (Ctx, F_Data)'Old
and Context_Cursor (Ctx, F_Option_Types) = Context_Cursor (Ctx, F_Option_Types)'Old
and Context_Cursor (Ctx, F_Options) = Context_Cursor (Ctx, F_Options)'Old
and Context_Cursor (Ctx, F_Value) = Context_Cursor (Ctx, F_Value)'Old,
Depends =>
(Ctx => (Ctx, Seq_Ctx), Seq_Ctx => Seq_Ctx);
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;
private
type Cursor_State is (S_Valid, S_Structural_Valid, S_Invalid, S_Incomplete);
function Valid_Value (Val : Field_Dependent_Value) return Boolean is
((case Val.Fld is
when F_Message_Type =>
Valid (Val.Message_Type_Value),
when F_Length =>
Valid (Val.Length_Value),
when F_Data | F_Option_Types | F_Options =>
True,
when F_Value =>
Valid (Val.Value_Value),
when F_Values =>
True,
when F_Initial | F_Final =>
False));
type Field_Cursor (State : Cursor_State := S_Invalid) is
record
Predecessor : Virtual_Field := F_Final;
case State is
when S_Valid | S_Structural_Valid =>
First : RFLX_Types.Bit_Index := RFLX_Types.Bit_Index'First;
Last : RFLX_Types.Bit_Length := RFLX_Types.Bit_Length'First;
Value : Field_Dependent_Value := (Fld => F_Final);
when S_Invalid | S_Incomplete =>
null;
end case;
end record with
Dynamic_Predicate =>
(if State = S_Valid or State = S_Structural_Valid then Valid_Value (Field_Cursor.Value));
type Field_Cursors is array (Virtual_Field) of Field_Cursor;
function Structural_Valid (Cursor : Field_Cursor) return Boolean is
(Cursor.State = S_Valid
or Cursor.State = S_Structural_Valid);
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, """Buffer"" is not modified, could be of access constant type");
function Valid_Context (Buffer_First, Buffer_Last : RFLX_Types.Index; First : RFLX_Types.Bit_Index; Last : RFLX_Types.Bit_Length; Message_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 mod RFLX_Types.Byte'Size = 1
and Last mod RFLX_Types.Byte'Size = 0)
and then First - 1 <= Message_Last
and then Message_Last <= Last
and then First mod RFLX_Types.Byte'Size = 1
and then Last mod RFLX_Types.Byte'Size = 0
and then Message_Last mod RFLX_Types.Byte'Size = 0
and then (for all F in Field'First .. Field'Last =>
(if
Structural_Valid (Cursors (F))
then
Cursors (F).First >= First
and Cursors (F).Last <= Message_Last
and Cursors (F).First <= Cursors (F).Last + 1
and Cursors (F).Value.Fld = F))
and then ((if
Structural_Valid (Cursors (F_Length))
then
(Valid (Cursors (F_Message_Type))
and then Cursors (F_Length).Predecessor = F_Message_Type
and then (RFLX_Types.U64 (Cursors (F_Message_Type).Value.Message_Type_Value) /= RFLX_Types.U64 (To_Base (RFLX.Universal.MT_Unconstrained_Options))
and RFLX_Types.U64 (Cursors (F_Message_Type).Value.Message_Type_Value) /= RFLX_Types.U64 (To_Base (RFLX.Universal.MT_Null))
and RFLX_Types.U64 (Cursors (F_Message_Type).Value.Message_Type_Value) /= RFLX_Types.U64 (To_Base (RFLX.Universal.MT_Unconstrained_Data)))))
and then (if
Structural_Valid (Cursors (F_Data))
then
(Valid (Cursors (F_Length))
and then Cursors (F_Data).Predecessor = F_Length
and then RFLX_Types.U64 (Cursors (F_Message_Type).Value.Message_Type_Value) = RFLX_Types.U64 (To_Base (RFLX.Universal.MT_Data)))
or (Valid (Cursors (F_Message_Type))
and then Cursors (F_Data).Predecessor = F_Message_Type
and then RFLX_Types.U64 (Cursors (F_Message_Type).Value.Message_Type_Value) = RFLX_Types.U64 (To_Base (RFLX.Universal.MT_Unconstrained_Data))))
and then (if
Structural_Valid (Cursors (F_Option_Types))
then
(Valid (Cursors (F_Length))
and then Cursors (F_Option_Types).Predecessor = F_Length
and then RFLX_Types.U64 (Cursors (F_Message_Type).Value.Message_Type_Value) = RFLX_Types.U64 (To_Base (RFLX.Universal.MT_Option_Types))))
and then (if
Structural_Valid (Cursors (F_Options))
then
(Valid (Cursors (F_Length))
and then Cursors (F_Options).Predecessor = F_Length
and then RFLX_Types.U64 (Cursors (F_Message_Type).Value.Message_Type_Value) = RFLX_Types.U64 (To_Base (RFLX.Universal.MT_Options)))
or (Valid (Cursors (F_Message_Type))
and then Cursors (F_Options).Predecessor = F_Message_Type
and then RFLX_Types.U64 (Cursors (F_Message_Type).Value.Message_Type_Value) = RFLX_Types.U64 (To_Base (RFLX.Universal.MT_Unconstrained_Options))))
and then (if
Structural_Valid (Cursors (F_Value))
then
(Valid (Cursors (F_Length))
and then Cursors (F_Value).Predecessor = F_Length
and then (RFLX_Types.U64 (Cursors (F_Message_Type).Value.Message_Type_Value) = RFLX_Types.U64 (To_Base (RFLX.Universal.MT_Value))
and RFLX_Types.U64 (Cursors (F_Length).Value.Length_Value) = Universal.Value'Size / 8)))
and then (if
Structural_Valid (Cursors (F_Values))
then
(Valid (Cursors (F_Length))
and then Cursors (F_Values).Predecessor = F_Length
and then RFLX_Types.U64 (Cursors (F_Message_Type).Value.Message_Type_Value) = RFLX_Types.U64 (To_Base (RFLX.Universal.MT_Values)))))
and then ((if Invalid (Cursors (F_Message_Type)) then Invalid (Cursors (F_Length)))
and then (if
Invalid (Cursors (F_Length))
and then Invalid (Cursors (F_Message_Type))
then
Invalid (Cursors (F_Data)))
and then (if Invalid (Cursors (F_Length)) then Invalid (Cursors (F_Option_Types)))
and then (if
Invalid (Cursors (F_Length))
and then Invalid (Cursors (F_Message_Type))
then
Invalid (Cursors (F_Options)))
and then (if Invalid (Cursors (F_Length)) then Invalid (Cursors (F_Value)))
and then (if Invalid (Cursors (F_Length)) then Invalid (Cursors (F_Values))))
and then (if
Structural_Valid (Cursors (F_Message_Type))
then
Cursors (F_Message_Type).Last - Cursors (F_Message_Type).First + 1 = RFLX.Universal.Message_Type_Base'Size
and then Cursors (F_Message_Type).Predecessor = F_Initial
and then Cursors (F_Message_Type).First = First
and then (if
Structural_Valid (Cursors (F_Data))
and then RFLX_Types.U64 (Cursors (F_Message_Type).Value.Message_Type_Value) = RFLX_Types.U64 (To_Base (RFLX.Universal.MT_Unconstrained_Data))
then
Cursors (F_Data).Last - Cursors (F_Data).First + 1 = RFLX_Types.Bit_Length (Last) - RFLX_Types.Bit_Length (Cursors (F_Message_Type).Last)
and then Cursors (F_Data).Predecessor = F_Message_Type
and then Cursors (F_Data).First = Cursors (F_Message_Type).Last + 1)
and then (if
Structural_Valid (Cursors (F_Length))
and then (RFLX_Types.U64 (Cursors (F_Message_Type).Value.Message_Type_Value) /= RFLX_Types.U64 (To_Base (RFLX.Universal.MT_Unconstrained_Options))
and RFLX_Types.U64 (Cursors (F_Message_Type).Value.Message_Type_Value) /= RFLX_Types.U64 (To_Base (RFLX.Universal.MT_Null))
and RFLX_Types.U64 (Cursors (F_Message_Type).Value.Message_Type_Value) /= RFLX_Types.U64 (To_Base (RFLX.Universal.MT_Unconstrained_Data)))
then
Cursors (F_Length).Last - Cursors (F_Length).First + 1 = RFLX.Universal.Length_Base'Size
and then Cursors (F_Length).Predecessor = F_Message_Type
and then Cursors (F_Length).First = Cursors (F_Message_Type).Last + 1
and then (if
Structural_Valid (Cursors (F_Data))
and then RFLX_Types.U64 (Cursors (F_Message_Type).Value.Message_Type_Value) = RFLX_Types.U64 (To_Base (RFLX.Universal.MT_Data))
then
Cursors (F_Data).Last - Cursors (F_Data).First + 1 = RFLX_Types.Bit_Length (Cursors (F_Length).Value.Length_Value) * 8
and then Cursors (F_Data).Predecessor = F_Length
and then Cursors (F_Data).First = Cursors (F_Length).Last + 1)
and then (if
Structural_Valid (Cursors (F_Option_Types))
and then RFLX_Types.U64 (Cursors (F_Message_Type).Value.Message_Type_Value) = RFLX_Types.U64 (To_Base (RFLX.Universal.MT_Option_Types))
then
Cursors (F_Option_Types).Last - Cursors (F_Option_Types).First + 1 = RFLX_Types.Bit_Length (Cursors (F_Length).Value.Length_Value) * 8
and then Cursors (F_Option_Types).Predecessor = F_Length
and then Cursors (F_Option_Types).First = Cursors (F_Length).Last + 1)
and then (if
Structural_Valid (Cursors (F_Options))
and then RFLX_Types.U64 (Cursors (F_Message_Type).Value.Message_Type_Value) = RFLX_Types.U64 (To_Base (RFLX.Universal.MT_Options))
then
Cursors (F_Options).Last - Cursors (F_Options).First + 1 = RFLX_Types.Bit_Length (Cursors (F_Length).Value.Length_Value) * 8
and then Cursors (F_Options).Predecessor = F_Length
and then Cursors (F_Options).First = Cursors (F_Length).Last + 1)
and then (if
Structural_Valid (Cursors (F_Value))
and then (RFLX_Types.U64 (Cursors (F_Message_Type).Value.Message_Type_Value) = RFLX_Types.U64 (To_Base (RFLX.Universal.MT_Value))
and RFLX_Types.U64 (Cursors (F_Length).Value.Length_Value) = Universal.Value'Size / 8)
then
Cursors (F_Value).Last - Cursors (F_Value).First + 1 = RFLX.Universal.Value'Size
and then Cursors (F_Value).Predecessor = F_Length
and then Cursors (F_Value).First = Cursors (F_Length).Last + 1)
and then (if
Structural_Valid (Cursors (F_Values))
and then RFLX_Types.U64 (Cursors (F_Message_Type).Value.Message_Type_Value) = RFLX_Types.U64 (To_Base (RFLX.Universal.MT_Values))
then
Cursors (F_Values).Last - Cursors (F_Values).First + 1 = RFLX_Types.Bit_Length (Cursors (F_Length).Value.Length_Value) * 8
and then Cursors (F_Values).Predecessor = F_Length
and then Cursors (F_Values).First = Cursors (F_Length).Last + 1))
and then (if
Structural_Valid (Cursors (F_Options))
and then RFLX_Types.U64 (Cursors (F_Message_Type).Value.Message_Type_Value) = RFLX_Types.U64 (To_Base (RFLX.Universal.MT_Unconstrained_Options))
then
Cursors (F_Options).Last - Cursors (F_Options).First + 1 = RFLX_Types.Bit_Length (Last) - RFLX_Types.Bit_Length (Cursors (F_Message_Type).Last)
and then Cursors (F_Options).Predecessor = F_Message_Type
and then Cursors (F_Options).First = Cursors (F_Message_Type).Last + 1)));
pragma Warnings (On, """Buffer"" is not modified, could be of access constant type");
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
Message_Last : RFLX_Types.Bit_Length := First - 1;
Buffer : RFLX_Types.Bytes_Ptr := null;
Cursors : Field_Cursors := (others => (State => S_Invalid, Predecessor => F_Final));
end record with
Dynamic_Predicate =>
Valid_Context (Context.Buffer_First, Context.Buffer_Last, Context.First, Context.Last, Context.Message_Last, Context.Buffer, Context.Cursors);
function Initialized (Ctx : Context) return Boolean is
(Ctx.Message_Last = Ctx.First - 1
and then Valid_Next (Ctx, F_Message_Type)
and then Field_First (Ctx, F_Message_Type) mod RFLX_Types.Byte'Size = 1
and then Available_Space (Ctx, F_Message_Type) = Ctx.Last - Ctx.First + 1
and then Invalid (Ctx, F_Message_Type)
and then Invalid (Ctx, F_Length)
and then Invalid (Ctx, F_Data)
and then Invalid (Ctx, F_Option_Types)
and then Invalid (Ctx, F_Options)
and then Invalid (Ctx, F_Value)
and then Invalid (Ctx, F_Values));
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 Message_Last (Ctx : Context) return RFLX_Types.Bit_Length is
(Ctx.Message_Last);
function Message_Data (Ctx : Context) return RFLX_Types.Bytes is
(Ctx.Buffer.all (RFLX_Types.To_Index (Ctx.First) .. RFLX_Types.To_Index (Ctx.Message_Last)));
function Path_Condition (Ctx : Context; Fld : Field) return Boolean is
((case Ctx.Cursors (Fld).Predecessor is
when F_Initial =>
(case Fld is
when F_Message_Type =>
True,
when others =>
False),
when F_Message_Type =>
(case Fld is
when F_Data =>
RFLX_Types.U64 (Ctx.Cursors (F_Message_Type).Value.Message_Type_Value) = RFLX_Types.U64 (To_Base (RFLX.Universal.MT_Unconstrained_Data)),
when F_Length =>
RFLX_Types.U64 (Ctx.Cursors (F_Message_Type).Value.Message_Type_Value) /= RFLX_Types.U64 (To_Base (RFLX.Universal.MT_Unconstrained_Options))
and RFLX_Types.U64 (Ctx.Cursors (F_Message_Type).Value.Message_Type_Value) /= RFLX_Types.U64 (To_Base (RFLX.Universal.MT_Null))
and RFLX_Types.U64 (Ctx.Cursors (F_Message_Type).Value.Message_Type_Value) /= RFLX_Types.U64 (To_Base (RFLX.Universal.MT_Unconstrained_Data)),
when F_Options =>
RFLX_Types.U64 (Ctx.Cursors (F_Message_Type).Value.Message_Type_Value) = RFLX_Types.U64 (To_Base (RFLX.Universal.MT_Unconstrained_Options)),
when others =>
False),
when F_Length =>
(case Fld is
when F_Data =>
RFLX_Types.U64 (Ctx.Cursors (F_Message_Type).Value.Message_Type_Value) = RFLX_Types.U64 (To_Base (RFLX.Universal.MT_Data)),
when F_Option_Types =>
RFLX_Types.U64 (Ctx.Cursors (F_Message_Type).Value.Message_Type_Value) = RFLX_Types.U64 (To_Base (RFLX.Universal.MT_Option_Types)),
when F_Options =>
RFLX_Types.U64 (Ctx.Cursors (F_Message_Type).Value.Message_Type_Value) = RFLX_Types.U64 (To_Base (RFLX.Universal.MT_Options)),
when F_Value =>
RFLX_Types.U64 (Ctx.Cursors (F_Message_Type).Value.Message_Type_Value) = RFLX_Types.U64 (To_Base (RFLX.Universal.MT_Value))
and RFLX_Types.U64 (Ctx.Cursors (F_Length).Value.Length_Value) = Universal.Value'Size / 8,
when F_Values =>
RFLX_Types.U64 (Ctx.Cursors (F_Message_Type).Value.Message_Type_Value) = RFLX_Types.U64 (To_Base (RFLX.Universal.MT_Values)),
when others =>
False),
when F_Data | F_Option_Types | F_Options | F_Value | F_Values | F_Final =>
False));
function Field_Condition (Ctx : Context; Val : Field_Dependent_Value) return Boolean is
((case Val.Fld is
when F_Initial =>
True,
when F_Message_Type =>
RFLX_Types.U64 (Val.Message_Type_Value) = RFLX_Types.U64 (To_Base (RFLX.Universal.MT_Unconstrained_Data))
or RFLX_Types.U64 (Val.Message_Type_Value) = RFLX_Types.U64 (To_Base (RFLX.Universal.MT_Null))
or (RFLX_Types.U64 (Val.Message_Type_Value) /= RFLX_Types.U64 (To_Base (RFLX.Universal.MT_Unconstrained_Options))
and RFLX_Types.U64 (Val.Message_Type_Value) /= RFLX_Types.U64 (To_Base (RFLX.Universal.MT_Null))
and RFLX_Types.U64 (Val.Message_Type_Value) /= RFLX_Types.U64 (To_Base (RFLX.Universal.MT_Unconstrained_Data)))
or RFLX_Types.U64 (Val.Message_Type_Value) = RFLX_Types.U64 (To_Base (RFLX.Universal.MT_Unconstrained_Options)),
when F_Length =>
RFLX_Types.U64 (Ctx.Cursors (F_Message_Type).Value.Message_Type_Value) = RFLX_Types.U64 (To_Base (RFLX.Universal.MT_Data))
or RFLX_Types.U64 (Ctx.Cursors (F_Message_Type).Value.Message_Type_Value) = RFLX_Types.U64 (To_Base (RFLX.Universal.MT_Option_Types))
or RFLX_Types.U64 (Ctx.Cursors (F_Message_Type).Value.Message_Type_Value) = RFLX_Types.U64 (To_Base (RFLX.Universal.MT_Options))
or (RFLX_Types.U64 (Ctx.Cursors (F_Message_Type).Value.Message_Type_Value) = RFLX_Types.U64 (To_Base (RFLX.Universal.MT_Value))
and RFLX_Types.U64 (Val.Length_Value) = Universal.Value'Size / 8)
or RFLX_Types.U64 (Ctx.Cursors (F_Message_Type).Value.Message_Type_Value) = RFLX_Types.U64 (To_Base (RFLX.Universal.MT_Values)),
when F_Data | F_Option_Types | F_Options | F_Value | F_Values =>
True,
when F_Final =>
False));
function Field_Size (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Length is
((case Ctx.Cursors (Fld).Predecessor is
when F_Initial =>
(case Fld is
when F_Message_Type =>
RFLX.Universal.Message_Type_Base'Size,
when others =>
raise Program_Error),
when F_Message_Type =>
(case Fld is
when F_Data =>
RFLX_Types.Bit_Length (Ctx.Last) - RFLX_Types.Bit_Length (Ctx.Cursors (F_Message_Type).Last),
when F_Length =>
RFLX.Universal.Length_Base'Size,
when F_Options =>
RFLX_Types.Bit_Length (Ctx.Last) - RFLX_Types.Bit_Length (Ctx.Cursors (F_Message_Type).Last),
when others =>
raise Program_Error),
when F_Length =>
(case Fld is
when F_Data | F_Option_Types | F_Options =>
RFLX_Types.Bit_Length (Ctx.Cursors (F_Length).Value.Length_Value) * 8,
when F_Value =>
RFLX.Universal.Value'Size,
when F_Values =>
RFLX_Types.Bit_Length (Ctx.Cursors (F_Length).Value.Length_Value) * 8,
when others =>
raise Program_Error),
when F_Data | F_Option_Types | F_Options | F_Value | F_Values | F_Final =>
0));
function Field_First (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index is
((case Fld is
when F_Message_Type =>
Ctx.First,
when F_Length =>
(if
Ctx.Cursors (Fld).Predecessor = F_Message_Type
and then (RFLX_Types.U64 (Ctx.Cursors (F_Message_Type).Value.Message_Type_Value) /= RFLX_Types.U64 (To_Base (RFLX.Universal.MT_Unconstrained_Options))
and RFLX_Types.U64 (Ctx.Cursors (F_Message_Type).Value.Message_Type_Value) /= RFLX_Types.U64 (To_Base (RFLX.Universal.MT_Null))
and RFLX_Types.U64 (Ctx.Cursors (F_Message_Type).Value.Message_Type_Value) /= RFLX_Types.U64 (To_Base (RFLX.Universal.MT_Unconstrained_Data)))
then
Ctx.Cursors (Ctx.Cursors (Fld).Predecessor).Last + 1
else
raise Program_Error),
when F_Data =>
(if
Ctx.Cursors (Fld).Predecessor = F_Length
and then RFLX_Types.U64 (Ctx.Cursors (F_Message_Type).Value.Message_Type_Value) = RFLX_Types.U64 (To_Base (RFLX.Universal.MT_Data))
then
Ctx.Cursors (Ctx.Cursors (Fld).Predecessor).Last + 1
elsif
Ctx.Cursors (Fld).Predecessor = F_Message_Type
and then RFLX_Types.U64 (Ctx.Cursors (F_Message_Type).Value.Message_Type_Value) = RFLX_Types.U64 (To_Base (RFLX.Universal.MT_Unconstrained_Data))
then
Ctx.Cursors (Ctx.Cursors (Fld).Predecessor).Last + 1
else
raise Program_Error),
when F_Option_Types =>
(if
Ctx.Cursors (Fld).Predecessor = F_Length
and then RFLX_Types.U64 (Ctx.Cursors (F_Message_Type).Value.Message_Type_Value) = RFLX_Types.U64 (To_Base (RFLX.Universal.MT_Option_Types))
then
Ctx.Cursors (Ctx.Cursors (Fld).Predecessor).Last + 1
else
raise Program_Error),
when F_Options =>
(if
Ctx.Cursors (Fld).Predecessor = F_Length
and then RFLX_Types.U64 (Ctx.Cursors (F_Message_Type).Value.Message_Type_Value) = RFLX_Types.U64 (To_Base (RFLX.Universal.MT_Options))
then
Ctx.Cursors (Ctx.Cursors (Fld).Predecessor).Last + 1
elsif
Ctx.Cursors (Fld).Predecessor = F_Message_Type
and then RFLX_Types.U64 (Ctx.Cursors (F_Message_Type).Value.Message_Type_Value) = RFLX_Types.U64 (To_Base (RFLX.Universal.MT_Unconstrained_Options))
then
Ctx.Cursors (Ctx.Cursors (Fld).Predecessor).Last + 1
else
raise Program_Error),
when F_Value =>
(if
Ctx.Cursors (Fld).Predecessor = F_Length
and then (RFLX_Types.U64 (Ctx.Cursors (F_Message_Type).Value.Message_Type_Value) = RFLX_Types.U64 (To_Base (RFLX.Universal.MT_Value))
and RFLX_Types.U64 (Ctx.Cursors (F_Length).Value.Length_Value) = Universal.Value'Size / 8)
then
Ctx.Cursors (Ctx.Cursors (Fld).Predecessor).Last + 1
else
raise Program_Error),
when F_Values =>
(if
Ctx.Cursors (Fld).Predecessor = F_Length
and then RFLX_Types.U64 (Ctx.Cursors (F_Message_Type).Value.Message_Type_Value) = RFLX_Types.U64 (To_Base (RFLX.Universal.MT_Values))
then
Ctx.Cursors (Ctx.Cursors (Fld).Predecessor).Last + 1
else
raise Program_Error)));
function Field_Last (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index is
(Field_First (Ctx, Fld) + Field_Size (Ctx, Fld) - 1);
function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field is
((case Fld is
when F_Initial =>
F_Initial,
when others =>
Ctx.Cursors (Fld).Predecessor));
function Valid_Predecessor (Ctx : Context; Fld : Virtual_Field) return Boolean is
((case Fld is
when F_Initial =>
True,
when F_Message_Type =>
Ctx.Cursors (Fld).Predecessor = F_Initial,
when F_Length =>
(Valid (Ctx.Cursors (F_Message_Type))
and Ctx.Cursors (Fld).Predecessor = F_Message_Type),
when F_Data =>
(Valid (Ctx.Cursors (F_Length))
and Ctx.Cursors (Fld).Predecessor = F_Length)
or (Valid (Ctx.Cursors (F_Message_Type))
and Ctx.Cursors (Fld).Predecessor = F_Message_Type),
when F_Option_Types =>
(Valid (Ctx.Cursors (F_Length))
and Ctx.Cursors (Fld).Predecessor = F_Length),
when F_Options =>
(Valid (Ctx.Cursors (F_Length))
and Ctx.Cursors (Fld).Predecessor = F_Length)
or (Valid (Ctx.Cursors (F_Message_Type))
and Ctx.Cursors (Fld).Predecessor = F_Message_Type),
when F_Value | F_Values =>
(Valid (Ctx.Cursors (F_Length))
and Ctx.Cursors (Fld).Predecessor = F_Length),
when F_Final =>
(Structural_Valid (Ctx.Cursors (F_Data))
and Ctx.Cursors (Fld).Predecessor = F_Data)
or (Valid (Ctx.Cursors (F_Message_Type))
and Ctx.Cursors (Fld).Predecessor = F_Message_Type)
or (Structural_Valid (Ctx.Cursors (F_Option_Types))
and Ctx.Cursors (Fld).Predecessor = F_Option_Types)
or (Structural_Valid (Ctx.Cursors (F_Options))
and Ctx.Cursors (Fld).Predecessor = F_Options)
or (Valid (Ctx.Cursors (F_Value))
and Ctx.Cursors (Fld).Predecessor = F_Value)
or (Structural_Valid (Ctx.Cursors (F_Values))
and Ctx.Cursors (Fld).Predecessor = F_Values)));
function Valid_Next (Ctx : Context; Fld : Field) return Boolean is
(Valid_Predecessor (Ctx, Fld)
and then Path_Condition (Ctx, Fld));
function Available_Space (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Length is
(Ctx.Last - Field_First (Ctx, Fld) + 1);
function Present (Ctx : Context; Fld : Field) return Boolean is
(Structural_Valid (Ctx.Cursors (Fld))
and then Ctx.Cursors (Fld).First < Ctx.Cursors (Fld).Last + 1);
function Structural_Valid (Ctx : Context; Fld : Field) return Boolean is
((Ctx.Cursors (Fld).State = S_Valid
or Ctx.Cursors (Fld).State = S_Structural_Valid));
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 Structural_Valid_Message (Ctx : Context) return Boolean is
(Valid (Ctx, F_Message_Type)
and then ((Structural_Valid (Ctx, F_Data)
and then RFLX_Types.U64 (Ctx.Cursors (F_Message_Type).Value.Message_Type_Value) = RFLX_Types.U64 (To_Base (RFLX.Universal.MT_Unconstrained_Data)))
or RFLX_Types.U64 (Ctx.Cursors (F_Message_Type).Value.Message_Type_Value) = RFLX_Types.U64 (To_Base (RFLX.Universal.MT_Null))
or (Valid (Ctx, F_Length)
and then (RFLX_Types.U64 (Ctx.Cursors (F_Message_Type).Value.Message_Type_Value) /= RFLX_Types.U64 (To_Base (RFLX.Universal.MT_Unconstrained_Options))
and RFLX_Types.U64 (Ctx.Cursors (F_Message_Type).Value.Message_Type_Value) /= RFLX_Types.U64 (To_Base (RFLX.Universal.MT_Null))
and RFLX_Types.U64 (Ctx.Cursors (F_Message_Type).Value.Message_Type_Value) /= RFLX_Types.U64 (To_Base (RFLX.Universal.MT_Unconstrained_Data)))
and then ((Structural_Valid (Ctx, F_Data)
and then RFLX_Types.U64 (Ctx.Cursors (F_Message_Type).Value.Message_Type_Value) = RFLX_Types.U64 (To_Base (RFLX.Universal.MT_Data)))
or (Structural_Valid (Ctx, F_Option_Types)
and then RFLX_Types.U64 (Ctx.Cursors (F_Message_Type).Value.Message_Type_Value) = RFLX_Types.U64 (To_Base (RFLX.Universal.MT_Option_Types)))
or (Structural_Valid (Ctx, F_Options)
and then RFLX_Types.U64 (Ctx.Cursors (F_Message_Type).Value.Message_Type_Value) = RFLX_Types.U64 (To_Base (RFLX.Universal.MT_Options)))
or (Valid (Ctx, F_Value)
and then (RFLX_Types.U64 (Ctx.Cursors (F_Message_Type).Value.Message_Type_Value) = RFLX_Types.U64 (To_Base (RFLX.Universal.MT_Value))
and RFLX_Types.U64 (Ctx.Cursors (F_Length).Value.Length_Value) = Universal.Value'Size / 8))
or (Structural_Valid (Ctx, F_Values)
and then RFLX_Types.U64 (Ctx.Cursors (F_Message_Type).Value.Message_Type_Value) = RFLX_Types.U64 (To_Base (RFLX.Universal.MT_Values)))))
or (Structural_Valid (Ctx, F_Options)
and then RFLX_Types.U64 (Ctx.Cursors (F_Message_Type).Value.Message_Type_Value) = RFLX_Types.U64 (To_Base (RFLX.Universal.MT_Unconstrained_Options)))));
function Valid_Message (Ctx : Context) return Boolean is
(Valid (Ctx, F_Message_Type)
and then ((Valid (Ctx, F_Data)
and then RFLX_Types.U64 (Ctx.Cursors (F_Message_Type).Value.Message_Type_Value) = RFLX_Types.U64 (To_Base (RFLX.Universal.MT_Unconstrained_Data)))
or RFLX_Types.U64 (Ctx.Cursors (F_Message_Type).Value.Message_Type_Value) = RFLX_Types.U64 (To_Base (RFLX.Universal.MT_Null))
or (Valid (Ctx, F_Length)
and then (RFLX_Types.U64 (Ctx.Cursors (F_Message_Type).Value.Message_Type_Value) /= RFLX_Types.U64 (To_Base (RFLX.Universal.MT_Unconstrained_Options))
and RFLX_Types.U64 (Ctx.Cursors (F_Message_Type).Value.Message_Type_Value) /= RFLX_Types.U64 (To_Base (RFLX.Universal.MT_Null))
and RFLX_Types.U64 (Ctx.Cursors (F_Message_Type).Value.Message_Type_Value) /= RFLX_Types.U64 (To_Base (RFLX.Universal.MT_Unconstrained_Data)))
and then ((Valid (Ctx, F_Data)
and then RFLX_Types.U64 (Ctx.Cursors (F_Message_Type).Value.Message_Type_Value) = RFLX_Types.U64 (To_Base (RFLX.Universal.MT_Data)))
or (Valid (Ctx, F_Option_Types)
and then RFLX_Types.U64 (Ctx.Cursors (F_Message_Type).Value.Message_Type_Value) = RFLX_Types.U64 (To_Base (RFLX.Universal.MT_Option_Types)))
or (Valid (Ctx, F_Options)
and then RFLX_Types.U64 (Ctx.Cursors (F_Message_Type).Value.Message_Type_Value) = RFLX_Types.U64 (To_Base (RFLX.Universal.MT_Options)))
or (Valid (Ctx, F_Value)
and then (RFLX_Types.U64 (Ctx.Cursors (F_Message_Type).Value.Message_Type_Value) = RFLX_Types.U64 (To_Base (RFLX.Universal.MT_Value))
and RFLX_Types.U64 (Ctx.Cursors (F_Length).Value.Length_Value) = Universal.Value'Size / 8))
or (Valid (Ctx, F_Values)
and then RFLX_Types.U64 (Ctx.Cursors (F_Message_Type).Value.Message_Type_Value) = RFLX_Types.U64 (To_Base (RFLX.Universal.MT_Values)))))
or (Valid (Ctx, F_Options)
and then RFLX_Types.U64 (Ctx.Cursors (F_Message_Type).Value.Message_Type_Value) = RFLX_Types.U64 (To_Base (RFLX.Universal.MT_Unconstrained_Options)))));
function Incomplete_Message (Ctx : Context) return Boolean is
(Incomplete (Ctx, F_Message_Type)
or Incomplete (Ctx, F_Length)
or Incomplete (Ctx, F_Data)
or Incomplete (Ctx, F_Option_Types)
or Incomplete (Ctx, F_Options)
or Incomplete (Ctx, F_Value)
or Incomplete (Ctx, F_Values));
function Get_Message_Type (Ctx : Context) return RFLX.Universal.Message_Type is
(To_Actual (Ctx.Cursors (F_Message_Type).Value.Message_Type_Value));
function Get_Length (Ctx : Context) return RFLX.Universal.Length is
(To_Actual (Ctx.Cursors (F_Length).Value.Length_Value));
function Get_Value (Ctx : Context) return RFLX.Universal.Value is
(To_Actual (Ctx.Cursors (F_Value).Value.Value_Value));
function Complete_Option_Types (Ctx : Context; Seq_Ctx : Universal.Option_Types.Context) return Boolean is
(Universal.Option_Types.Valid (Seq_Ctx)
and Universal.Option_Types.Size (Seq_Ctx) = Field_Size (Ctx, F_Option_Types));
function Complete_Options (Ctx : Context; Seq_Ctx : Universal.Options.Context) return Boolean is
(Universal.Options.Valid (Seq_Ctx)
and Universal.Options.Size (Seq_Ctx) = Field_Size (Ctx, F_Options));
function Complete_Values (Ctx : Context; Seq_Ctx : Universal.Values.Context) return Boolean is
(Universal.Values.Valid (Seq_Ctx)
and Universal.Values.Size (Seq_Ctx) = Field_Size (Ctx, F_Values));
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);
end RFLX.Universal.Message;
Raw
rflx-universal-option.adb
--
-- Generated by RecordFlux 0.6.0-pre on 2021-10-25
--
-- Copyright (C) 2018-2021 Componolit GmbH
--
-- This file is distributed under the terms of the GNU Affero General Public License version 3.
--
pragma Style_Checks ("N3aAbcdefhiIklnOprStux");
pragma Warnings (Off, "redundant conversion");
package body RFLX.Universal.Option 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_Last, First, Last, First - 1, Buffer, (F_Option_Type => (State => S_Invalid, Predecessor => F_Initial), others => (State => S_Invalid, Predecessor => F_Final)));
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, Ctx.Buffer, (F_Option_Type => (State => S_Invalid, Predecessor => F_Initial), others => (State => S_Invalid, Predecessor => F_Final)));
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.Message_Last));
else
Buffer := Ctx.Buffer.all (RFLX_Types.Index'Last .. RFLX_Types.Index'First);
end if;
end Copy;
procedure Read (Ctx : Context) is
begin
Read (Ctx.Buffer.all (RFLX_Types.To_Index (Ctx.First) .. RFLX_Types.To_Index (Ctx.Message_Last)));
end Read;
procedure Write (Ctx : in out Context) is
Length : RFLX_Types.Length;
begin
Write (Ctx.Buffer.all, Length);
pragma Assert (Length <= Ctx.Buffer.all'Length, "Length <= Buffer'Length is not ensured by postcondition of ""Write""");
Reset (Ctx, RFLX_Types.To_First_Bit_Index (Ctx.Buffer_First), RFLX_Types.To_Last_Bit_Index (RFLX_Types.Length (Ctx.Buffer_First) + Length - 1));
end Write;
function Size (Ctx : Context) return RFLX_Types.Bit_Length is
((if Ctx.Message_Last = Ctx.First - 1 then 0 else Ctx.Message_Last - Ctx.First + 1));
function Byte_Size (Ctx : Context) return RFLX_Types.Length is
((if
Ctx.Message_Last = Ctx.First - 1
then
0
else
RFLX_Types.Length (RFLX_Types.To_Index (Ctx.Message_Last) - RFLX_Types.To_Index (Ctx.First) + 1)));
pragma Warnings (Off, "precondition is always False");
function Successor (Ctx : Context; Fld : Field) return Virtual_Field is
((case Fld is
when F_Option_Type =>
(if
RFLX_Types.U64 (Ctx.Cursors (F_Option_Type).Value.Option_Type_Value) = RFLX_Types.U64 (To_Base (RFLX.Universal.OT_Null))
then
F_Final
elsif
RFLX_Types.U64 (Ctx.Cursors (F_Option_Type).Value.Option_Type_Value) = RFLX_Types.U64 (To_Base (RFLX.Universal.OT_Data))
then
F_Length
else
F_Initial),
when F_Length =>
F_Data,
when F_Data =>
F_Final))
with
Pre =>
Has_Buffer (Ctx)
and Structural_Valid (Ctx, Fld)
and Valid_Predecessor (Ctx, Fld);
pragma Warnings (On, "precondition is always False");
function Invalid_Successor (Ctx : Context; Fld : Field) return Boolean is
((case Fld is
when F_Option_Type =>
Invalid (Ctx.Cursors (F_Length)),
when F_Length =>
Invalid (Ctx.Cursors (F_Data)),
when F_Data =>
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 Available_Space (Ctx, Fld) >= Field_Size (Ctx, Fld))
with
Pre =>
Has_Buffer (Ctx)
and Valid_Next (Ctx, Fld);
function Equal (Ctx : Context; Fld : Field; Data : RFLX_Types.Bytes) return Boolean is
(Sufficient_Buffer_Length (Ctx, Fld)
and then (case Fld is
when F_Data =>
Ctx.Buffer.all (RFLX_Types.To_Index (Field_First (Ctx, Fld)) .. RFLX_Types.To_Index (Field_Last (Ctx, Fld))) = Data,
when others =>
False));
procedure Reset_Dependent_Fields (Ctx : in out Context; Fld : Field) with
Pre =>
Valid_Next (Ctx, Fld),
Post =>
Valid_Next (Ctx, Fld)
and Invalid (Ctx.Cursors (Fld))
and Invalid_Successor (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 Ctx.Cursors (Fld).Predecessor = Ctx.Cursors (Fld).Predecessor'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
First : constant RFLX_Types.Bit_Length := Field_First (Ctx, Fld) with
Ghost;
Size : constant RFLX_Types.Bit_Length := Field_Size (Ctx, Fld) with
Ghost;
begin
pragma Assert (Field_First (Ctx, Fld) = First
and Field_Size (Ctx, Fld) = Size);
case Fld is
when F_Option_Type =>
Ctx.Cursors (F_Data) := (S_Invalid, F_Final);
Ctx.Cursors (F_Length) := (S_Invalid, F_Final);
Ctx.Cursors (F_Option_Type) := (S_Invalid, Ctx.Cursors (F_Option_Type).Predecessor);
pragma Assert (Field_First (Ctx, Fld) = First
and Field_Size (Ctx, Fld) = Size);
when F_Length =>
Ctx.Cursors (F_Data) := (S_Invalid, F_Final);
Ctx.Cursors (F_Length) := (S_Invalid, Ctx.Cursors (F_Length).Predecessor);
pragma Assert (Field_First (Ctx, Fld) = First
and Field_Size (Ctx, Fld) = Size);
when F_Data =>
Ctx.Cursors (F_Data) := (S_Invalid, Ctx.Cursors (F_Data).Predecessor);
pragma Assert (Field_First (Ctx, Fld) = First
and Field_Size (Ctx, Fld) = Size);
end case;
end Reset_Dependent_Fields;
function Composite_Field (Fld : Field) return Boolean is
((case Fld is
when F_Option_Type | F_Length =>
False,
when F_Data =>
True));
function Get_Field_Value (Ctx : Context; Fld : Field) return Field_Dependent_Value with
Pre =>
Has_Buffer (Ctx)
and then Valid_Next (Ctx, Fld)
and then Sufficient_Buffer_Length (Ctx, Fld),
Post =>
Get_Field_Value'Result.Fld = Fld
is
First : constant RFLX_Types.Bit_Index := Field_First (Ctx, Fld);
Last : constant RFLX_Types.Bit_Index := Field_Last (Ctx, Fld);
function Buffer_First return RFLX_Types.Index is
(RFLX_Types.To_Index (First));
function Buffer_Last return RFLX_Types.Index is
(RFLX_Types.To_Index (Last));
function Offset return RFLX_Types.Offset is
(RFLX_Types.Offset ((8 - Last mod 8) mod 8));
function Extract is new RFLX_Types.Extract (RFLX.Universal.Option_Type_Base);
function Extract is new RFLX_Types.Extract (RFLX.Universal.Length_Base);
begin
return ((case Fld is
when F_Option_Type =>
(Fld => F_Option_Type, Option_Type_Value => Extract (Ctx.Buffer.all (Buffer_First .. Buffer_Last), Offset)),
when F_Length =>
(Fld => F_Length, Length_Value => Extract (Ctx.Buffer.all (Buffer_First .. Buffer_Last), Offset)),
when F_Data =>
(Fld => F_Data)));
end Get_Field_Value;
procedure Verify (Ctx : in out Context; Fld : Field) is
Value : Field_Dependent_Value;
begin
if
Has_Buffer (Ctx)
and then Invalid (Ctx.Cursors (Fld))
and then Valid_Predecessor (Ctx, Fld)
and then Path_Condition (Ctx, Fld)
then
if Sufficient_Buffer_Length (Ctx, Fld) then
Value := Get_Field_Value (Ctx, Fld);
if
Valid_Value (Value)
and Field_Condition (Ctx, Value)
then
pragma Assert ((if Fld = F_Data or Fld = F_Option_Type then Field_Last (Ctx, Fld) mod RFLX_Types.Byte'Size = 0));
case Fld is
when F_Option_Type =>
Ctx.Message_Last := ((Field_Last (Ctx, Fld) + 7) / 8) * 8;
when F_Length =>
Ctx.Message_Last := ((Field_Last (Ctx, Fld) + 7) / 8) * 8;
when F_Data =>
Ctx.Message_Last := ((Field_Last (Ctx, Fld) + 7) / 8) * 8;
end case;
if Composite_Field (Fld) then
Ctx.Cursors (Fld) := (State => S_Structural_Valid, First => Field_First (Ctx, Fld), Last => Field_Last (Ctx, Fld), Value => Value, Predecessor => Ctx.Cursors (Fld).Predecessor);
else
Ctx.Cursors (Fld) := (State => S_Valid, First => Field_First (Ctx, Fld), Last => Field_Last (Ctx, Fld), Value => Value, Predecessor => Ctx.Cursors (Fld).Predecessor);
end if;
if Fld = F_Option_Type then
Ctx.Cursors (Successor (Ctx, Fld)) := (State => S_Invalid, Predecessor => Fld);
elsif Fld = F_Length then
Ctx.Cursors (Successor (Ctx, Fld)) := (State => S_Invalid, Predecessor => Fld);
elsif Fld = F_Data then
Ctx.Cursors (Successor (Ctx, Fld)) := (State => S_Invalid, Predecessor => Fld);
end if;
else
Ctx.Cursors (Fld) := (State => S_Invalid, Predecessor => F_Final);
end if;
else
Ctx.Cursors (Fld) := (State => S_Incomplete, Predecessor => F_Final);
end if;
end if;
end Verify;
procedure Verify_Message (Ctx : in out Context) is
begin
Verify (Ctx, F_Option_Type);
Verify (Ctx, F_Length);
Verify (Ctx, F_Data);
end Verify_Message;
function Get_Data (Ctx : Context) return RFLX_Types.Bytes is
First : constant RFLX_Types.Index := RFLX_Types.To_Index (Ctx.Cursors (F_Data).First);
Last : constant RFLX_Types.Index := RFLX_Types.To_Index (Ctx.Cursors (F_Data).Last);
begin
return Ctx.Buffer.all (First .. Last);
end Get_Data;
procedure Get_Data (Ctx : Context; Data : out RFLX_Types.Bytes) is
First : constant RFLX_Types.Index := RFLX_Types.To_Index (Ctx.Cursors (F_Data).First);
Last : constant RFLX_Types.Index := RFLX_Types.To_Index (Ctx.Cursors (F_Data).Last);
begin
Data := (others => RFLX_Types.Byte'First);
Data (Data'First .. Data'First + (Last - First)) := Ctx.Buffer.all (First .. Last);
end Get_Data;
procedure Generic_Get_Data (Ctx : Context) is
First : constant RFLX_Types.Index := RFLX_Types.To_Index (Ctx.Cursors (F_Data).First);
Last : constant RFLX_Types.Index := RFLX_Types.To_Index (Ctx.Cursors (F_Data).Last);
begin
Process_Data (Ctx.Buffer.all (First .. Last));
end Generic_Get_Data;
procedure Set_Field_Value (Ctx : in out Context; Val : Field_Dependent_Value; Fst, Lst : out RFLX_Types.Bit_Index) with
Pre =>
not Ctx'Constrained
and then Has_Buffer (Ctx)
and then Val.Fld in Field'Range
and then Valid_Next (Ctx, Val.Fld)
and then Available_Space (Ctx, Val.Fld) >= Field_Size (Ctx, Val.Fld)
and then (for all F in Field'Range =>
(if Structural_Valid (Ctx.Cursors (F)) then Ctx.Cursors (F).Last <= Field_Last (Ctx, Val.Fld))),
Post =>
Has_Buffer (Ctx)
and Fst = Field_First (Ctx, Val.Fld)
and Lst = Field_Last (Ctx, Val.Fld)
and Fst >= Ctx.First
and Fst <= Lst + 1
and Lst <= Ctx.Last
and (for all F in Field'Range =>
(if Structural_Valid (Ctx.Cursors (F)) then Ctx.Cursors (F).Last <= Lst))
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 Ctx.Cursors = Ctx.Cursors'Old
is
First : constant RFLX_Types.Bit_Index := Field_First (Ctx, Val.Fld);
Last : constant RFLX_Types.Bit_Index := Field_Last (Ctx, Val.Fld);
function Buffer_First return RFLX_Types.Index is
(RFLX_Types.To_Index (First));
function Buffer_Last return RFLX_Types.Index is
(RFLX_Types.To_Index (Last));
function Offset return RFLX_Types.Offset is
(RFLX_Types.Offset ((8 - Last mod 8) mod 8));
procedure Insert is new RFLX_Types.Insert (RFLX.Universal.Option_Type_Base);
procedure Insert is new RFLX_Types.Insert (RFLX.Universal.Length_Base);
begin
Fst := First;
Lst := Last;
case Val.Fld is
when F_Initial =>
null;
when F_Option_Type =>
Insert (Val.Option_Type_Value, Ctx.Buffer.all (Buffer_First .. Buffer_Last), Offset);
when F_Length =>
Insert (Val.Length_Value, Ctx.Buffer.all (Buffer_First .. Buffer_Last), Offset);
when F_Data | F_Final =>
null;
end case;
end Set_Field_Value;
procedure Set_Option_Type (Ctx : in out Context; Val : RFLX.Universal.Option_Type_Enum) is
Field_Value : constant Field_Dependent_Value := (F_Option_Type, To_Base (Val));
First, Last : RFLX_Types.Bit_Index;
begin
Reset_Dependent_Fields (Ctx, F_Option_Type);
Set_Field_Value (Ctx, Field_Value, First, Last);
Ctx.Message_Last := Last;
Ctx.Cursors (F_Option_Type) := (State => S_Valid, First => First, Last => Last, Value => Field_Value, Predecessor => Ctx.Cursors (F_Option_Type).Predecessor);
Ctx.Cursors (Successor (Ctx, F_Option_Type)) := (State => S_Invalid, Predecessor => F_Option_Type);
end Set_Option_Type;
procedure Set_Length (Ctx : in out Context; Val : RFLX.Universal.Length) is
Field_Value : constant Field_Dependent_Value := (F_Length, To_Base (Val));
First, Last : RFLX_Types.Bit_Index;
begin
Reset_Dependent_Fields (Ctx, F_Length);
Set_Field_Value (Ctx, Field_Value, First, Last);
Ctx.Message_Last := ((Last + 7) / 8) * 8;
Ctx.Cursors (F_Length) := (State => S_Valid, First => First, Last => Last, Value => Field_Value, Predecessor => Ctx.Cursors (F_Length).Predecessor);
Ctx.Cursors (Successor (Ctx, F_Length)) := (State => S_Invalid, Predecessor => F_Length);
end Set_Length;
procedure Set_Data_Empty (Ctx : in out Context) is
First : constant RFLX_Types.Bit_Index := Field_First (Ctx, F_Data);
Last : constant RFLX_Types.Bit_Index := Field_Last (Ctx, F_Data);
begin
Reset_Dependent_Fields (Ctx, F_Data);
Ctx.Message_Last := Last;
Ctx.Cursors (F_Data) := (State => S_Valid, First => First, Last => Last, Value => (Fld => F_Data), Predecessor => Ctx.Cursors (F_Data).Predecessor);
Ctx.Cursors (Successor (Ctx, F_Data)) := (State => S_Invalid, Predecessor => F_Data);
end Set_Data_Empty;
procedure Initialize_Data_Private (Ctx : in out Context) with
Pre =>
not Ctx'Constrained
and then Has_Buffer (Ctx)
and then Valid_Next (Ctx, F_Data)
and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data)
and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1
and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0
and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0,
Post =>
Has_Buffer (Ctx)
and Structural_Valid (Ctx, F_Data)
and Ctx.Message_Last = Field_Last (Ctx, F_Data)
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 Predecessor (Ctx, F_Data) = Predecessor (Ctx, F_Data)'Old
and Valid_Next (Ctx, F_Data) = Valid_Next (Ctx, F_Data)'Old
and Get_Option_Type (Ctx) = Get_Option_Type (Ctx)'Old
and Get_Length (Ctx) = Get_Length (Ctx)'Old
is
First : constant RFLX_Types.Bit_Index := Field_First (Ctx, F_Data);
Last : constant RFLX_Types.Bit_Index := Field_Last (Ctx, F_Data);
begin
Reset_Dependent_Fields (Ctx, F_Data);
Ctx.Message_Last := Last;
Ctx.Cursors (F_Data) := (State => S_Structural_Valid, First => First, Last => Last, Value => (Fld => F_Data), Predecessor => Ctx.Cursors (F_Data).Predecessor);
Ctx.Cursors (Successor (Ctx, F_Data)) := (State => S_Invalid, Predecessor => F_Data);
end Initialize_Data_Private;
procedure Initialize_Data (Ctx : in out Context) is
begin
Initialize_Data_Private (Ctx);
end Initialize_Data;
procedure Set_Data (Ctx : in out Context; Data : RFLX_Types.Bytes) is
First : constant RFLX_Types.Bit_Index := Field_First (Ctx, F_Data);
Last : constant RFLX_Types.Bit_Index := Field_Last (Ctx, F_Data);
function Buffer_First return RFLX_Types.Index is
(RFLX_Types.To_Index (First));
function Buffer_Last return RFLX_Types.Index is
(RFLX_Types.To_Index (Last));
begin
Initialize_Data_Private (Ctx);
Ctx.Buffer.all (Buffer_First .. Buffer_Last) := Data;
end Set_Data;
procedure Generic_Set_Data (Ctx : in out Context) is
First : constant RFLX_Types.Bit_Index := Field_First (Ctx, F_Data);
Last : constant RFLX_Types.Bit_Index := Field_Last (Ctx, F_Data);
function Buffer_First return RFLX_Types.Index is
(RFLX_Types.To_Index (First));
function Buffer_Last return RFLX_Types.Index is
(RFLX_Types.To_Index (Last));
begin
Initialize_Data_Private (Ctx);
Process_Data (Ctx.Buffer.all (Buffer_First .. Buffer_Last));
end Generic_Set_Data;
end RFLX.Universal.Option;
Raw
rflx-universal-option.ads
--
-- Generated by RecordFlux 0.6.0-pre on 2021-10-25
--
-- Copyright (C) 2018-2021 Componolit GmbH
--
-- This file is distributed under the terms of the GNU Affero General Public License version 3.
--
pragma Style_Checks ("N3aAbcdefhiIklnOprStux");
pragma Warnings (Off, "redundant conversion");
with RFLX.RFLX_Types;
package RFLX.Universal.Option with
SPARK_Mode,
Annotate =>
(GNATprove, Terminating)
is
pragma Warnings (Off, "use clause for type ""U64"" * has no effect");
pragma Warnings (Off, """LENGTH"" is already use-visible through previous use_type_clause");
use type RFLX_Types.Bytes;
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.U64;
pragma Warnings (On, """LENGTH"" is already use-visible through previous use_type_clause");
pragma Warnings (On, "use clause for type ""U64"" * has no effect");
type Virtual_Field is (F_Initial, F_Option_Type, F_Length, F_Data, F_Final);
subtype Field is Virtual_Field range F_Option_Type .. F_Data;
type Field_Cursor is private with
Default_Initial_Condition =>
False;
type Field_Cursors is private with
Default_Initial_Condition =>
False;
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 mod RFLX_Types.Byte'Size = 1
and Last mod RFLX_Types.Byte'Size = 0;
type Field_Dependent_Value (Fld : Virtual_Field := F_Initial) is
record
case Fld is
when F_Initial | F_Data | F_Final =>
null;
when F_Option_Type =>
Option_Type_Value : RFLX.Universal.Option_Type_Base;
when F_Length =>
Length_Value : RFLX.Universal.Length_Base;
end case;
end record;
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 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, 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_Index'Last
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 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), Buffer => null);
function Initialized (Ctx : Context) return Boolean with
Ghost;
procedure Reset (Ctx : in out Context) with
Pre =>
not Ctx'Constrained
and 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 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 mod RFLX_Types.Byte'Size = 1
and Last mod 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 =>
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 =>
Has_Buffer (Ctx)
and then Structural_Valid_Message (Ctx)
and then Byte_Size (Ctx) = Buffer'Length;
generic
with procedure Read (Buffer : RFLX_Types.Bytes);
procedure Read (Ctx : Context) with
Pre =>
Has_Buffer (Ctx)
and then Structural_Valid_Message (Ctx);
generic
with procedure Write (Buffer : out RFLX_Types.Bytes; Length : out RFLX_Types.Length);
procedure Write (Ctx : in out Context) with
Pre =>
not Ctx'Constrained
and 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 Initialized (Ctx);
function Has_Buffer (Ctx : Context) return Boolean;
function Size (Ctx : Context) return RFLX_Types.Bit_Length;
function Byte_Size (Ctx : Context) return RFLX_Types.Length;
function Message_Last (Ctx : Context) return RFLX_Types.Bit_Length with
Pre =>
Has_Buffer (Ctx)
and then Structural_Valid_Message (Ctx);
function Message_Data (Ctx : Context) return RFLX_Types.Bytes with
Pre =>
Has_Buffer (Ctx)
and then Structural_Valid_Message (Ctx),
Post =>
Message_Data'Result'Length = Byte_Size (Ctx);
function Path_Condition (Ctx : Context; Fld : Field) return Boolean with
Pre =>
Valid_Predecessor (Ctx, Fld);
function Field_Condition (Ctx : Context; Val : Field_Dependent_Value) return Boolean with
Pre =>
Has_Buffer (Ctx)
and Val.Fld in Field'Range
and Valid_Predecessor (Ctx, Val.Fld);
function Field_Size (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Length with
Pre =>
Valid_Next (Ctx, Fld);
function Field_First (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with
Pre =>
Valid_Next (Ctx, Fld);
function Field_Last (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with
Pre =>
Valid_Next (Ctx, Fld)
and then Available_Space (Ctx, Fld) >= Field_Size (Ctx, Fld);
function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field;
function Valid_Predecessor (Ctx : Context; Fld : Virtual_Field) return Boolean;
function Valid_Next (Ctx : Context; Fld : Field) return Boolean;
function Available_Space (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Length with
Pre =>
Valid_Next (Ctx, Fld);
function Equal (Ctx : Context; Fld : Field; Data : RFLX_Types.Bytes) return Boolean with
Pre =>
Has_Buffer (Ctx)
and Valid_Next (Ctx, Fld);
procedure Verify (Ctx : in out Context; Fld : Field) with
Post =>
Has_Buffer (Ctx) = Has_Buffer (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;
procedure Verify_Message (Ctx : in out Context) with
Post =>
Has_Buffer (Ctx) = Has_Buffer (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;
function Present (Ctx : Context; Fld : Field) return Boolean;
function Structural_Valid (Ctx : Context; Fld : Field) return Boolean;
function Valid (Ctx : Context; Fld : Field) return Boolean with
Post =>
(if Valid'Result then Structural_Valid (Ctx, Fld) and Present (Ctx, Fld));
function Incomplete (Ctx : Context; Fld : Field) return Boolean;
function Invalid (Ctx : Context; Fld : Field) return Boolean;
function Structural_Valid_Message (Ctx : Context) return Boolean with
Pre =>
Has_Buffer (Ctx);
function Valid_Message (Ctx : Context) return Boolean with
Pre =>
Has_Buffer (Ctx);
function Incomplete_Message (Ctx : Context) return Boolean;
pragma Warnings (Off, "precondition is always False");
function Get_Option_Type (Ctx : Context) return RFLX.Universal.Option_Type with
Pre =>
Valid (Ctx, F_Option_Type);
function Get_Length (Ctx : Context) return RFLX.Universal.Length with
Pre =>
Valid (Ctx, F_Length);
pragma Warnings (On, "precondition is always False");
function Get_Data (Ctx : Context) return RFLX_Types.Bytes with
Pre =>
Has_Buffer (Ctx)
and then Structural_Valid (Ctx, F_Data)
and then Valid_Next (Ctx, F_Data),
Post =>
Get_Data'Result'Length = RFLX_Types.To_Length (Field_Size (Ctx, F_Data));
procedure Get_Data (Ctx : Context; Data : out RFLX_Types.Bytes) with
Pre =>
Has_Buffer (Ctx)
and then Structural_Valid (Ctx, F_Data)
and then Valid_Next (Ctx, F_Data)
and then Data'Length >= RFLX_Types.To_Length (Field_Size (Ctx, F_Data));
generic
with procedure Process_Data (Data : RFLX_Types.Bytes);
procedure Generic_Get_Data (Ctx : Context) with
Pre =>
Has_Buffer (Ctx)
and Present (Ctx, F_Data);
procedure Set_Option_Type (Ctx : in out Context; Val : RFLX.Universal.Option_Type_Enum) with
Pre =>
not Ctx'Constrained
and then Has_Buffer (Ctx)
and then Valid_Next (Ctx, F_Option_Type)
and then Field_Condition (Ctx, (F_Option_Type, To_Base (Val)))
and then True
and then Available_Space (Ctx, F_Option_Type) >= Field_Size (Ctx, F_Option_Type),
Post =>
Has_Buffer (Ctx)
and Valid (Ctx, F_Option_Type)
and Get_Option_Type (Ctx) = (True, Val)
and (if Structural_Valid_Message (Ctx) then Message_Last (Ctx) = Field_Last (Ctx, F_Option_Type))
and Invalid (Ctx, F_Length)
and Invalid (Ctx, F_Data)
and (if
RFLX_Types.U64 (To_Base (Get_Option_Type (Ctx))) = RFLX_Types.U64 (To_Base (RFLX.Universal.OT_Data))
then
Predecessor (Ctx, F_Length) = F_Option_Type
and Valid_Next (Ctx, F_Length))
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 Predecessor (Ctx, F_Option_Type) = Predecessor (Ctx, F_Option_Type)'Old
and Valid_Next (Ctx, F_Option_Type) = Valid_Next (Ctx, F_Option_Type)'Old;
procedure Set_Length (Ctx : in out Context; Val : RFLX.Universal.Length) with
Pre =>
not Ctx'Constrained
and then Has_Buffer (Ctx)
and then Valid_Next (Ctx, F_Length)
and then Field_Condition (Ctx, (F_Length, To_Base (Val)))
and then Valid (To_Base (Val))
and then Available_Space (Ctx, F_Length) >= Field_Size (Ctx, F_Length),
Post =>
Has_Buffer (Ctx)
and Valid (Ctx, F_Length)
and Get_Length (Ctx) = Val
and Invalid (Ctx, F_Data)
and (Predecessor (Ctx, F_Data) = F_Length
and Valid_Next (Ctx, F_Data))
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 Predecessor (Ctx, F_Length) = Predecessor (Ctx, F_Length)'Old
and Valid_Next (Ctx, F_Length) = Valid_Next (Ctx, F_Length)'Old
and Get_Option_Type (Ctx) = Get_Option_Type (Ctx)'Old
and Context_Cursor (Ctx, F_Option_Type) = Context_Cursor (Ctx, F_Option_Type)'Old;
procedure Set_Data_Empty (Ctx : in out Context) with
Pre =>
not Ctx'Constrained
and then Has_Buffer (Ctx)
and then Valid_Next (Ctx, F_Data)
and then Field_Condition (Ctx, (Fld => F_Data))
and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data)
and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1
and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0
and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0
and then Field_Size (Ctx, F_Data) = 0,
Post =>
Has_Buffer (Ctx)
and Structural_Valid (Ctx, F_Data)
and (if Structural_Valid_Message (Ctx) then Message_Last (Ctx) = Field_Last (Ctx, F_Data))
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 Predecessor (Ctx, F_Data) = Predecessor (Ctx, F_Data)'Old
and Valid_Next (Ctx, F_Data) = Valid_Next (Ctx, F_Data)'Old
and Get_Option_Type (Ctx) = Get_Option_Type (Ctx)'Old
and Get_Length (Ctx) = Get_Length (Ctx)'Old;
procedure Initialize_Data (Ctx : in out Context) with
Pre =>
not Ctx'Constrained
and then Has_Buffer (Ctx)
and then Valid_Next (Ctx, F_Data)
and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data)
and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1
and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0
and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0,
Post =>
Has_Buffer (Ctx)
and Structural_Valid (Ctx, F_Data)
and (if Structural_Valid_Message (Ctx) then Message_Last (Ctx) = Field_Last (Ctx, F_Data))
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 Predecessor (Ctx, F_Data) = Predecessor (Ctx, F_Data)'Old
and Valid_Next (Ctx, F_Data) = Valid_Next (Ctx, F_Data)'Old
and Get_Option_Type (Ctx) = Get_Option_Type (Ctx)'Old
and Get_Length (Ctx) = Get_Length (Ctx)'Old;
procedure Set_Data (Ctx : in out Context; Data : RFLX_Types.Bytes) with
Pre =>
not Ctx'Constrained
and then Has_Buffer (Ctx)
and then Valid_Next (Ctx, F_Data)
and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data)
and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1
and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0
and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0
and then Data'Length = RFLX_Types.To_Length (Field_Size (Ctx, F_Data))
and then Field_Condition (Ctx, (Fld => F_Data)),
Post =>
Has_Buffer (Ctx)
and Structural_Valid (Ctx, F_Data)
and (if Structural_Valid_Message (Ctx) then Message_Last (Ctx) = Field_Last (Ctx, F_Data))
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 Predecessor (Ctx, F_Data) = Predecessor (Ctx, F_Data)'Old
and Valid_Next (Ctx, F_Data) = Valid_Next (Ctx, F_Data)'Old
and Get_Option_Type (Ctx) = Get_Option_Type (Ctx)'Old
and Get_Length (Ctx) = Get_Length (Ctx)'Old;
generic
with procedure Process_Data (Data : out RFLX_Types.Bytes);
with function Valid_Length (Length : RFLX_Types.Length) return Boolean;
procedure Generic_Set_Data (Ctx : in out Context) with
Pre =>
not Ctx'Constrained
and then Has_Buffer (Ctx)
and then Valid_Next (Ctx, F_Data)
and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data)
and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1
and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0
and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0
and then Valid_Length (RFLX_Types.Length (Field_Size (Ctx, F_Data) / RFLX_Types.Byte'Size)),
Post =>
Has_Buffer (Ctx)
and Structural_Valid (Ctx, F_Data)
and (if Structural_Valid_Message (Ctx) then Message_Last (Ctx) = Field_Last (Ctx, F_Data))
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 Predecessor (Ctx, F_Data) = Predecessor (Ctx, F_Data)'Old
and Valid_Next (Ctx, F_Data) = Valid_Next (Ctx, F_Data)'Old
and Get_Option_Type (Ctx) = Get_Option_Type (Ctx)'Old
and Get_Length (Ctx) = Get_Length (Ctx)'Old;
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;
private
type Cursor_State is (S_Valid, S_Structural_Valid, S_Invalid, S_Incomplete);
function Valid_Value (Val : Field_Dependent_Value) return Boolean is
((case Val.Fld is
when F_Option_Type =>
Valid (Val.Option_Type_Value),
when F_Length =>
Valid (Val.Length_Value),
when F_Data =>
True,
when F_Initial | F_Final =>
False));
type Field_Cursor (State : Cursor_State := S_Invalid) is
record
Predecessor : Virtual_Field := F_Final;
case State is
when S_Valid | S_Structural_Valid =>
First : RFLX_Types.Bit_Index := RFLX_Types.Bit_Index'First;
Last : RFLX_Types.Bit_Length := RFLX_Types.Bit_Length'First;
Value : Field_Dependent_Value := (Fld => F_Final);
when S_Invalid | S_Incomplete =>
null;
end case;
end record with
Dynamic_Predicate =>
(if State = S_Valid or State = S_Structural_Valid then Valid_Value (Field_Cursor.Value));
type Field_Cursors is array (Virtual_Field) of Field_Cursor;
function Structural_Valid (Cursor : Field_Cursor) return Boolean is
(Cursor.State = S_Valid
or Cursor.State = S_Structural_Valid);
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, """Buffer"" is not modified, could be of access constant type");
function Valid_Context (Buffer_First, Buffer_Last : RFLX_Types.Index; First : RFLX_Types.Bit_Index; Last : RFLX_Types.Bit_Length; Message_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 mod RFLX_Types.Byte'Size = 1
and Last mod RFLX_Types.Byte'Size = 0)
and then First - 1 <= Message_Last
and then Message_Last <= Last
and then First mod RFLX_Types.Byte'Size = 1
and then Last mod RFLX_Types.Byte'Size = 0
and then Message_Last mod RFLX_Types.Byte'Size = 0
and then (for all F in Field'First .. Field'Last =>
(if
Structural_Valid (Cursors (F))
then
Cursors (F).First >= First
and Cursors (F).Last <= Message_Last
and Cursors (F).First <= Cursors (F).Last + 1
and Cursors (F).Value.Fld = F))
and then ((if
Structural_Valid (Cursors (F_Length))
then
(Valid (Cursors (F_Option_Type))
and then Cursors (F_Length).Predecessor = F_Option_Type
and then RFLX_Types.U64 (Cursors (F_Option_Type).Value.Option_Type_Value) = RFLX_Types.U64 (To_Base (RFLX.Universal.OT_Data))))
and then (if
Structural_Valid (Cursors (F_Data))
then
(Valid (Cursors (F_Length))
and then Cursors (F_Data).Predecessor = F_Length)))
and then ((if Invalid (Cursors (F_Option_Type)) then Invalid (Cursors (F_Length)))
and then (if Invalid (Cursors (F_Length)) then Invalid (Cursors (F_Data))))
and then (if
Structural_Valid (Cursors (F_Option_Type))
then
Cursors (F_Option_Type).Last - Cursors (F_Option_Type).First + 1 = RFLX.Universal.Option_Type_Base'Size
and then Cursors (F_Option_Type).Predecessor = F_Initial
and then Cursors (F_Option_Type).First = First
and then (if
Structural_Valid (Cursors (F_Length))
and then RFLX_Types.U64 (Cursors (F_Option_Type).Value.Option_Type_Value) = RFLX_Types.U64 (To_Base (RFLX.Universal.OT_Data))
then
Cursors (F_Length).Last - Cursors (F_Length).First + 1 = RFLX.Universal.Length_Base'Size
and then Cursors (F_Length).Predecessor = F_Option_Type
and then Cursors (F_Length).First = Cursors (F_Option_Type).Last + 1
and then (if
Structural_Valid (Cursors (F_Data))
then
Cursors (F_Data).Last - Cursors (F_Data).First + 1 = RFLX_Types.Bit_Length (Cursors (F_Length).Value.Length_Value) * 8
and then Cursors (F_Data).Predecessor = F_Length
and then Cursors (F_Data).First = Cursors (F_Length).Last + 1))));
pragma Warnings (On, """Buffer"" is not modified, could be of access constant type");
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
Message_Last : RFLX_Types.Bit_Length := First - 1;
Buffer : RFLX_Types.Bytes_Ptr := null;
Cursors : Field_Cursors := (others => (State => S_Invalid, Predecessor => F_Final));
end record with
Dynamic_Predicate =>
Valid_Context (Context.Buffer_First, Context.Buffer_Last, Context.First, Context.Last, Context.Message_Last, Context.Buffer, Context.Cursors);
function Initialized (Ctx : Context) return Boolean is
(Ctx.Message_Last = Ctx.First - 1
and then Valid_Next (Ctx, F_Option_Type)
and then Field_First (Ctx, F_Option_Type) mod RFLX_Types.Byte'Size = 1
and then Available_Space (Ctx, F_Option_Type) = Ctx.Last - Ctx.First + 1
and then Invalid (Ctx, F_Option_Type)
and then Invalid (Ctx, F_Length)
and then Invalid (Ctx, F_Data));
function Has_Buffer (Ctx : Context) return Boolean is
(Ctx.Buffer /= null);
function Message_Last (Ctx : Context) return RFLX_Types.Bit_Length is
(Ctx.Message_Last);
function Message_Data (Ctx : Context) return RFLX_Types.Bytes is
(Ctx.Buffer.all (RFLX_Types.To_Index (Ctx.First) .. RFLX_Types.To_Index (Ctx.Message_Last)));
function Path_Condition (Ctx : Context; Fld : Field) return Boolean is
((case Ctx.Cursors (Fld).Predecessor is
when F_Initial =>
(case Fld is
when F_Option_Type =>
True,
when others =>
False),
when F_Option_Type =>
(case Fld is
when F_Length =>
RFLX_Types.U64 (Ctx.Cursors (F_Option_Type).Value.Option_Type_Value) = RFLX_Types.U64 (To_Base (RFLX.Universal.OT_Data)),
when others =>
False),
when F_Length =>
(case Fld is
when F_Data =>
True,
when others =>
False),
when F_Data | F_Final =>
False));
function Field_Condition (Ctx : Context; Val : Field_Dependent_Value) return Boolean is
((case Val.Fld is
when F_Initial =>
True,
when F_Option_Type =>
RFLX_Types.U64 (Val.Option_Type_Value) = RFLX_Types.U64 (To_Base (RFLX.Universal.OT_Null))
or RFLX_Types.U64 (Val.Option_Type_Value) = RFLX_Types.U64 (To_Base (RFLX.Universal.OT_Data)),
when F_Length | F_Data =>
True,
when F_Final =>
False));
function Field_Size (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Length is
((case Ctx.Cursors (Fld).Predecessor is
when F_Initial =>
(case Fld is
when F_Option_Type =>
RFLX.Universal.Option_Type_Base'Size,
when others =>
raise Program_Error),
when F_Option_Type =>
(case Fld is
when F_Length =>
RFLX.Universal.Length_Base'Size,
when others =>
raise Program_Error),
when F_Length =>
(case Fld is
when F_Data =>
RFLX_Types.Bit_Length (Ctx.Cursors (F_Length).Value.Length_Value) * 8,
when others =>
raise Program_Error),
when F_Data | F_Final =>
0));
function Field_First (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index is
((case Fld is
when F_Option_Type =>
Ctx.First,
when F_Length =>
(if
Ctx.Cursors (Fld).Predecessor = F_Option_Type
and then RFLX_Types.U64 (Ctx.Cursors (F_Option_Type).Value.Option_Type_Value) = RFLX_Types.U64 (To_Base (RFLX.Universal.OT_Data))
then
Ctx.Cursors (Ctx.Cursors (Fld).Predecessor).Last + 1
else
raise Program_Error),
when F_Data =>
(if
Ctx.Cursors (Fld).Predecessor = F_Length
then
Ctx.Cursors (Ctx.Cursors (Fld).Predecessor).Last + 1
else
raise Program_Error)));
function Field_Last (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index is
(Field_First (Ctx, Fld) + Field_Size (Ctx, Fld) - 1);
function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field is
((case Fld is
when F_Initial =>
F_Initial,
when others =>
Ctx.Cursors (Fld).Predecessor));
function Valid_Predecessor (Ctx : Context; Fld : Virtual_Field) return Boolean is
((case Fld is
when F_Initial =>
True,
when F_Option_Type =>
Ctx.Cursors (Fld).Predecessor = F_Initial,
when F_Length =>
(Valid (Ctx.Cursors (F_Option_Type))
and Ctx.Cursors (Fld).Predecessor = F_Option_Type),
when F_Data =>
(Valid (Ctx.Cursors (F_Length))
and Ctx.Cursors (Fld).Predecessor = F_Length),
when F_Final =>
(Structural_Valid (Ctx.Cursors (F_Data))
and Ctx.Cursors (Fld).Predecessor = F_Data)
or (Valid (Ctx.Cursors (F_Option_Type))
and Ctx.Cursors (Fld).Predecessor = F_Option_Type)));
function Valid_Next (Ctx : Context; Fld : Field) return Boolean is
(Valid_Predecessor (Ctx, Fld)
and then Path_Condition (Ctx, Fld));
function Available_Space (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Length is
(Ctx.Last - Field_First (Ctx, Fld) + 1);
function Present (Ctx : Context; Fld : Field) return Boolean is
(Structural_Valid (Ctx.Cursors (Fld))
and then Ctx.Cursors (Fld).First < Ctx.Cursors (Fld).Last + 1);
function Structural_Valid (Ctx : Context; Fld : Field) return Boolean is
((Ctx.Cursors (Fld).State = S_Valid
or Ctx.Cursors (Fld).State = S_Structural_Valid));
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 Structural_Valid_Message (Ctx : Context) return Boolean is
(Valid (Ctx, F_Option_Type)
and then (RFLX_Types.U64 (Ctx.Cursors (F_Option_Type).Value.Option_Type_Value) = RFLX_Types.U64 (To_Base (RFLX.Universal.OT_Null))
or (Valid (Ctx, F_Length)
and then RFLX_Types.U64 (Ctx.Cursors (F_Option_Type).Value.Option_Type_Value) = RFLX_Types.U64 (To_Base (RFLX.Universal.OT_Data))
and then Structural_Valid (Ctx, F_Data))));
function Valid_Message (Ctx : Context) return Boolean is
(Valid (Ctx, F_Option_Type)
and then (RFLX_Types.U64 (Ctx.Cursors (F_Option_Type).Value.Option_Type_Value) = RFLX_Types.U64 (To_Base (RFLX.Universal.OT_Null))
or (Valid (Ctx, F_Length)
and then RFLX_Types.U64 (Ctx.Cursors (F_Option_Type).Value.Option_Type_Value) = RFLX_Types.U64 (To_Base (RFLX.Universal.OT_Data))
and then Valid (Ctx, F_Data))));
function Incomplete_Message (Ctx : Context) return Boolean is
(Incomplete (Ctx, F_Option_Type)
or Incomplete (Ctx, F_Length)
or Incomplete (Ctx, F_Data));
function Get_Option_Type (Ctx : Context) return RFLX.Universal.Option_Type is
(To_Actual (Ctx.Cursors (F_Option_Type).Value.Option_Type_Value));
function Get_Length (Ctx : Context) return RFLX.Universal.Length is
(To_Actual (Ctx.Cursors (F_Length).Value.Length_Value));
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);
end RFLX.Universal.Option;
Raw
rflx-universal-option_types.ads
--
-- Generated by RecordFlux 0.6.0-pre on 2021-10-25
--
-- Copyright (C) 2018-2021 Componolit GmbH
--
-- This file is distributed under the terms of the GNU Affero General Public License version 3.
--
pragma Style_Checks ("N3aAbcdefhiIklnOprStux");
pragma Warnings (Off, "redundant conversion");
pragma SPARK_Mode;
with RFLX.RFLX_Scalar_Sequence;
with RFLX.Universal;
pragma Warnings (Off, "unit ""*RFLX_Types"" is not referenced");
with RFLX.RFLX_Types;
pragma Warnings (On, "unit ""*RFLX_Types"" is not referenced");
package RFLX.Universal.Option_Types is new RFLX.RFLX_Scalar_Sequence (RFLX.Universal.Option_Type, RFLX.Universal.Option_Type_Base, RFLX.Universal.Valid, RFLX.Universal.To_Actual, RFLX.Universal.To_Base);
Raw
rflx-universal-options.ads
--
-- Generated by RecordFlux 0.6.0-pre on 2021-10-25
--
-- Copyright (C) 2018-2021 Componolit GmbH
--
-- This file is distributed under the terms of the GNU Affero General Public License version 3.
--
pragma Style_Checks ("N3aAbcdefhiIklnOprStux");
pragma Warnings (Off, "redundant conversion");
pragma SPARK_Mode;
with RFLX.RFLX_Message_Sequence;
with RFLX.Universal.Option;
pragma Warnings (Off, "unit ""*RFLX_Types"" is not referenced");
with RFLX.RFLX_Types;
pragma Warnings (On, "unit ""*RFLX_Types"" is not referenced");
package RFLX.Universal.Options is new RFLX.RFLX_Message_Sequence (RFLX.Universal.Option.Context, RFLX.Universal.Option.Initialize, RFLX.Universal.Option.Take_Buffer, RFLX.Universal.Option.Has_Buffer, RFLX.Universal.Option.Message_Last, RFLX.Universal.Option.Initialized, RFLX.Universal.Option.Structural_Valid_Message);
Raw
rflx-universal-values.ads
--
-- Generated by RecordFlux 0.6.0-pre on 2021-10-25
--
-- Copyright (C) 2018-2021 Componolit GmbH
--
-- This file is distributed under the terms of the GNU Affero General Public License version 3.
--
pragma Style_Checks ("N3aAbcdefhiIklnOprStux");
pragma Warnings (Off, "redundant conversion");
pragma SPARK_Mode;
with RFLX.RFLX_Scalar_Sequence;
with RFLX.Universal;
pragma Warnings (Off, "unit ""*RFLX_Types"" is not referenced");
with RFLX.RFLX_Types;
pragma Warnings (On, "unit ""*RFLX_Types"" is not referenced");
package RFLX.Universal.Values is new RFLX.RFLX_Scalar_Sequence (RFLX.Universal.Value, RFLX.Universal.Value, RFLX.Universal.Valid, RFLX.Universal.To_Actual, RFLX.Universal.To_Base);
Raw
rflx-universal.ads
--
-- Generated by RecordFlux 0.6.0-pre on 2021-10-25
--
-- Copyright (C) 2018-2021 Componolit GmbH
--
-- This file is distributed under the terms of the GNU Affero General Public License version 3.
--
pragma Style_Checks ("N3aAbcdefhiIklnOprStux");
pragma Warnings (Off, "redundant conversion");
package RFLX.Universal with
SPARK_Mode
is
type Message_Type_Base is mod 2**8;
type Message_Type is (MT_Null, MT_Data, MT_Value, MT_Values, MT_Option_Types, MT_Options, MT_Unconstrained_Data, MT_Unconstrained_Options) with
Size =>
8;
for Message_Type use (MT_Null => 0, MT_Data => 1, MT_Value => 2, MT_Values => 3, MT_Option_Types => 4, MT_Options => 5, MT_Unconstrained_Data => 6, MT_Unconstrained_Options => 7);
function Valid (Val : RFLX.Universal.Message_Type_Base) return Boolean is
((case Val is
when 0 | 1 | 2 | 3 | 4 | 5 | 6 | 7 =>
True,
when others =>
False));
function To_Base (Enum : RFLX.Universal.Message_Type) return RFLX.Universal.Message_Type_Base is
((case Enum is
when MT_Null =>
0,
when MT_Data =>
1,
when MT_Value =>
2,
when MT_Values =>
3,
when MT_Option_Types =>
4,
when MT_Options =>
5,
when MT_Unconstrained_Data =>
6,
when MT_Unconstrained_Options =>
7));
pragma Warnings (Off, "unreachable branch");
function To_Actual (Val : RFLX.Universal.Message_Type_Base) return RFLX.Universal.Message_Type is
((case Val is
when 0 =>
MT_Null,
when 1 =>
MT_Data,
when 2 =>
MT_Value,
when 3 =>
MT_Values,
when 4 =>
MT_Option_Types,
when 5 =>
MT_Options,
when 6 =>
MT_Unconstrained_Data,
when 7 =>
MT_Unconstrained_Options,
when others =>
raise Program_Error))
with
Pre =>
Valid (Val);
pragma Warnings (On, "unreachable branch");
type Length_Base is mod 2**16 with
Annotate =>
(GNATprove, No_Wrap_Around);
type Length is range 0 .. 2**16 - 1 with
Size =>
16;
pragma Warnings (Off, "unused variable ""Val""");
pragma Warnings (Off, "formal parameter ""Val"" is not referenced");
function Valid (Val : RFLX.Universal.Length_Base) return Boolean is
(True);
pragma Warnings (On, "formal parameter ""Val"" is not referenced");
pragma Warnings (On, "unused variable ""Val""");
function To_Base (Val : RFLX.Universal.Length) return RFLX.Universal.Length_Base is
(RFLX.Universal.Length_Base (Val));
function To_Actual (Val : RFLX.Universal.Length_Base) return RFLX.Universal.Length is
(RFLX.Universal.Length (Val))
with
Pre =>
Valid (Val);
type Value is mod 256 with
Size =>
8;
pragma Warnings (Off, "unused variable ""Val""");
pragma Warnings (Off, "formal parameter ""Val"" is not referenced");
function Valid (Val : RFLX.Universal.Value) return Boolean is
(True);
pragma Warnings (On, "formal parameter ""Val"" is not referenced");
pragma Warnings (On, "unused variable ""Val""");
function To_Base (Val : RFLX.Universal.Value) return RFLX.Universal.Value is
(Val);
function To_Actual (Val : RFLX.Universal.Value) return RFLX.Universal.Value is
(Val)
with
Pre =>
Valid (Val);
type Option_Type_Base is mod 2**8;
type Option_Type_Enum is (OT_Null, OT_Data) with
Size =>
8;
for Option_Type_Enum use (OT_Null => 0, OT_Data => 1);
type Option_Type (Known : Boolean := False) is
record
case Known is
when True =>
Enum : Option_Type_Enum;
when False =>
Raw : Option_Type_Base;
end case;
end record;
pragma Warnings (Off, "unused variable ""Val""");
pragma Warnings (Off, "formal parameter ""Val"" is not referenced");
function Valid (Val : RFLX.Universal.Option_Type_Base) return Boolean is
(True);
pragma Warnings (On, "formal parameter ""Val"" is not referenced");
pragma Warnings (On, "unused variable ""Val""");
function To_Base (Enum : RFLX.Universal.Option_Type_Enum) return RFLX.Universal.Option_Type_Base is
((case Enum is
when OT_Null =>
0,
when OT_Data =>
1));
function To_Actual (Enum : Option_Type_Enum) return RFLX.Universal.Option_Type is
((True, Enum));
function To_Actual (Val : RFLX.Universal.Option_Type_Base) return RFLX.Universal.Option_Type is
((case Val is
when 0 =>
(True, OT_Null),
when 1 =>
(True, OT_Data),
when others =>
(False, Val)))
with
Pre =>
Valid (Val);
function To_Base (Val : RFLX.Universal.Option_Type) return RFLX.Universal.Option_Type_Base is
((if Val.Known then To_Base (Val.Enum) else Val.Raw));
end RFLX.Universal;
Raw
rflx.ads
--
-- Generated by RecordFlux 0.6.0-pre on 2021-10-25
--
-- Copyright (C) 2018-2021 Componolit GmbH
--
-- This file is distributed under the terms of the GNU Affero General Public License version 3.
--
package RFLX is
end RFLX;
Raw
test.gpr
with "defaults";
project Test is
for Source_Dirs use (".");
for Main use ("main.adb");
package Builder is
for Default_Switches ("Ada") use Defaults.Builder_Switches;
end Builder;
package Compiler is
for Default_Switches ("Ada") use Defaults.Compiler_Switches;
end Compiler;
package Prove is
for Proof_Dir use "proof";
for Proof_Switches ("Ada") use
Defaults.Proof_Switches & ("--steps=0", "--timeout=90");
end Prove;
end Test;
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment