Add feature test for parameterized messages

Ref. #609

tests/integration/parameterized_messages/INPUT

@@ -0,0 +1 @@
+1 2

tests/integration/parameterized_messages/OUTPUT

@@ -0,0 +1,4 @@
+State: Receive
+Write: 1 2
+State: Reply
+Read: 1 2 3 4

tests/integration/parameterized_messages/PROVE

@@ -0,0 +1,2 @@
+rflx-test
+rflx-test-message

tests/integration/parameterized_messages/generated/rflx-rflx_arithmetic.adb

@@ -0,0 +1,60 @@
+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;

tests/integration/parameterized_messages/generated/rflx-rflx_arithmetic.ads

@@ -0,0 +1,47 @@
+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;

tests/integration/parameterized_messages/generated/rflx-rflx_builtin_types-conversions.ads

@@ -0,0 +1,31 @@
+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;

tests/integration/parameterized_messages/generated/rflx-rflx_builtin_types.ads

@@ -0,0 +1,21 @@
+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;