Prevent warnings on suspicious modulus values in SPARK code

Ref. #316

generated/rflx-arrays.ads

@@ -4,7 +4,9 @@ package RFLX.Arrays with
   SPARK_Mode
 is
 
-   type Length is mod 2**8;
+   type Length is mod 2**8 with
+     Size =>
+       8;
 
    pragma Warnings (Off, "precondition is * false");
 
@@ -36,7 +38,9 @@ is
      Pre =>
        Valid (Val);
 
-   type Modular_Integer is mod 2**16;
+   type Modular_Integer is mod 2**16 with
+     Size =>
+       16;
 
    pragma Warnings (Off, "precondition is * false");
 

generated/rflx-ethernet.ads

@@ -4,7 +4,9 @@ package RFLX.Ethernet with
   SPARK_Mode
 is
 
-   type Address is mod 2**48;
+   type Address is mod 2**48 with
+     Size =>
+       48;
 
    pragma Warnings (Off, "precondition is * false");
 
@@ -96,7 +98,9 @@ is
      Pre =>
        Valid (Val);
 
-   type TCI is mod 2**16;
+   type TCI is mod 2**16 with
+     Size =>
+       16;
 
    pragma Warnings (Off, "precondition is * false");
 

generated/rflx-ipv4.ads

@@ -64,7 +64,9 @@ is
      Pre =>
        Valid (Val);
 
-   type DCSP is mod 2**6;
+   type DCSP is mod 2**6 with
+     Size =>
+       6;
 
    pragma Warnings (Off, "precondition is * false");
 
@@ -96,7 +98,9 @@ is
      Pre =>
        Valid (Val);
 
-   type ECN is mod 2**2;
+   type ECN is mod 2**2 with
+     Size =>
+       2;
 
    pragma Warnings (Off, "precondition is * false");
 
@@ -158,7 +162,9 @@ is
      Pre =>
        Valid (Val);
 
-   type Identification is mod 2**16;
+   type Identification is mod 2**16 with
+     Size =>
+       16;
 
    pragma Warnings (Off, "precondition is * false");
 
@@ -190,7 +196,9 @@ is
      Pre =>
        Valid (Val);
 
-   type Fragment_Offset is mod 2**13;
+   type Fragment_Offset is mod 2**13 with
+     Size =>
+       13;
 
    pragma Warnings (Off, "precondition is * false");
 
@@ -222,7 +230,9 @@ is
      Pre =>
        Valid (Val);
 
-   type TTL is mod 2**8;
+   type TTL is mod 2**8 with
+     Size =>
+       8;
 
    pragma Warnings (Off, "precondition is * false");
 
@@ -318,7 +328,9 @@ is
        else
           Val.Raw));
 
-   type Header_Checksum is mod 2**16;
+   type Header_Checksum is mod 2**16 with
+     Size =>
+       16;
 
    pragma Warnings (Off, "precondition is * false");
 
@@ -350,7 +362,9 @@ is
      Pre =>
        Valid (Val);
 
-   type Address is mod 2**32;
+   type Address is mod 2**32 with
+     Size =>
+       32;
 
    pragma Warnings (Off, "precondition is * false");
 
@@ -429,7 +443,9 @@ is
 
    pragma Warnings (On, "unreachable branch");
 
-   type Option_Number is mod 2**5;
+   type Option_Number is mod 2**5 with
+     Size =>
+       5;
 
    pragma Warnings (Off, "precondition is * false");
 

generated/rflx-tlv.ads

@@ -51,7 +51,9 @@ is
 
    pragma Warnings (On, "unreachable branch");
 
-   type Length is mod 2**14;
+   type Length is mod 2**14 with
+     Size =>
+       14;
 
    pragma Warnings (Off, "precondition is * false");
 

generated/rflx-udp.ads

@@ -4,7 +4,9 @@ package RFLX.UDP with
   SPARK_Mode
 is
 
-   type Port is mod 2**16;
+   type Port is mod 2**16 with
+     Size =>
+       16;
 
    pragma Warnings (Off, "precondition is * false");
 
@@ -66,7 +68,9 @@ is
      Pre =>
        Valid (Val);
 
-   type Checksum is mod 2**16;
+   type Checksum is mod 2**16 with
+     Size =>
+       16;
 
    pragma Warnings (Off, "precondition is * false");
 

rflx/ada.py

@@ -408,11 +408,12 @@ def type_definition(self) -> str:
 
 
 class RangeType(TypeDeclaration):
-    def __init__(self, identifier: StrID, first: Expr, last: Expr, size: Expr) -> None:
-        super().__init__(identifier, aspects=[Size(size)])
+    def __init__(
+        self, identifier: StrID, first: Expr, last: Expr, aspects: Sequence[Aspect] = None
+    ) -> None:
+        super().__init__(identifier, aspects=aspects or [])
         self.first = first
         self.last = last
-        self.size = size
 
     @property
     def type_definition(self) -> str:

rflx/generator/core.py

@@ -50,6 +50,9 @@
     RangeSubtype,
     RangeType,
     RecordType,
+)
+from rflx.ada import Size as SizeAspect
+from rflx.ada import (
     SparkMode,
     Statement,
     Subprogram,
@@ -2665,7 +2668,7 @@ def create_file(filename: Path, content: str) -> None:
 
 
 def modular_types(integer: ModularInteger) -> List[TypeDeclaration]:
-    return [ModularType(integer.name, integer.modulus)]
+    return [ModularType(integer.name, integer.modulus, aspects=[SizeAspect(integer.size)])]
 
 
 def range_types(integer: RangeInteger) -> List[TypeDeclaration]:
@@ -2675,7 +2678,7 @@ def range_types(integer: RangeInteger) -> List[TypeDeclaration]:
             Pow(Number(2), integer.size),
             [Annotate("GNATprove", "No_Wrap_Around")],
         ),
-        RangeType(integer.name, integer.first, integer.last, integer.size),
+        RangeType(integer.name, integer.first, integer.last, aspects=[SizeAspect(integer.size)]),
     ]