Rename RFLX_Utils to RFLX_Arithmetic

Ref. #294
AdaCore · Jun 19, 2020 · fbea48f · fbea48f
1 parent cb6cf76
commit fbea48f
Show file tree

Hide file tree

Showing 9 changed files with 17 additions and 17 deletions.
diff --git a/README.md b/README.md
@@ -98,17 +98,17 @@ Creating generated/rflx-tlv.ads
 Creating generated/rflx-tlv-generic_message.ads
 Creating generated/rflx-tlv-generic_message.adb
 Creating generated/rflx-tlv-message.ads
+Creating generated/rflx-rflx_arithmetic.ads
 Creating generated/rflx-rflx_builtin_types-conversions.ads
 Creating generated/rflx-rflx_builtin_types.ads
 Creating generated/rflx-rflx_generic_types.ads
 Creating generated/rflx-rflx_message_sequence.ads
 Creating generated/rflx-rflx_scalar_sequence.ads
-Creating generated/rflx-rflx_utils.ads
 Creating generated/rflx-rflx_types.ads
+Creating generated/rflx-rflx_arithmetic.adb
 Creating generated/rflx-rflx_generic_types.adb
 Creating generated/rflx-rflx_message_sequence.adb
 Creating generated/rflx-rflx_scalar_sequence.adb
-Creating generated/rflx-rflx_utils.adb
 Creating generated/rflx.ads
 ```
 

diff --git a/generated/rflx-rflx_utils.adb → generated/rflx-rflx_arithmetic.adb b/generated/rflx-rflx_utils.adb → generated/rflx-rflx_arithmetic.adb
@@ -1,6 +1,6 @@
 pragma Style_Checks ("N3aAbcdefhiIklnOprStux");
 
-package body RFLX.RFLX_Utils with
+package body RFLX.RFLX_Arithmetic with
   SPARK_Mode
 is
 
@@ -60,4 +60,4 @@ is
       return Result;
    end Mod_Pow2;
 
-end RFLX.RFLX_Utils;
+end RFLX.RFLX_Arithmetic;
diff --git a/generated/rflx-rflx_utils.ads → generated/rflx-rflx_arithmetic.ads b/generated/rflx-rflx_utils.ads → generated/rflx-rflx_arithmetic.ads
@@ -1,6 +1,6 @@
 pragma Style_Checks ("N3aAbcdefhiIklnOprStux");
 
-package RFLX.RFLX_Utils with
+package RFLX.RFLX_Arithmetic with
   SPARK_Mode
 is
 
@@ -38,4 +38,4 @@ is
      Post =>
        Mod_Pow2'Result < 2**Exp;
 
-end RFLX.RFLX_Utils;
+end RFLX.RFLX_Arithmetic;
diff --git a/generated/rflx-rflx_generic_types.adb b/generated/rflx-rflx_generic_types.adb
@@ -1,6 +1,6 @@
 pragma Style_Checks ("N3aAbcdefhiIklnOprStux");
 
-with RFLX.RFLX_Utils; use RFLX.RFLX_Utils;
+with RFLX.RFLX_Arithmetic; use RFLX.RFLX_Arithmetic;
 
 package body RFLX.RFLX_Generic_Types with
   SPARK_Mode

diff --git a/rflx/generator/const.py b/rflx/generator/const.py
@@ -3,32 +3,32 @@
 
 REFINEMENT_PACKAGE = ID("Contains")
 
+ARITHMETIC_PACKAGE = ID("RFLX_Arithmetic")
 BUILTIN_TYPES_CONVERSIONS_PACKAGE = ID("RFLX_Builtin_Types.Conversions")
 BUILTIN_TYPES_PACKAGE = ID("RFLX_Builtin_Types")
 GENERIC_TYPES_PACKAGE = ID("RFLX_Generic_Types")
 MESSAGE_SEQUENCE_PACKAGE = ID("RFLX_Message_Sequence")
 SCALAR_SEQUENCE_PACKAGE = ID("RFLX_Scalar_Sequence")
 TYPES_PACKAGE = ID("RFLX_Types")
-UTILS_PACKAGE = ID("RFLX_Utils")
 
 LIBRARY_FILES = [
     file_name(str(p)) + ".ads"
     for p in [
+        ARITHMETIC_PACKAGE,
         BUILTIN_TYPES_CONVERSIONS_PACKAGE,
         BUILTIN_TYPES_PACKAGE,
         GENERIC_TYPES_PACKAGE,
         MESSAGE_SEQUENCE_PACKAGE,
         SCALAR_SEQUENCE_PACKAGE,
         TYPES_PACKAGE,
-        UTILS_PACKAGE,
     ]
 ] + [
     file_name(str(p)) + ".adb"
     for p in [
+        ARITHMETIC_PACKAGE,
         GENERIC_TYPES_PACKAGE,
         MESSAGE_SEQUENCE_PACKAGE,
         SCALAR_SEQUENCE_PACKAGE,
-        UTILS_PACKAGE,
     ]
 ]
 

diff --git a/rflx/templates/rflx_utils.adb → rflx/templates/rflx_arithmetic.adb b/rflx/templates/rflx_utils.adb → rflx/templates/rflx_arithmetic.adb
@@ -1,6 +1,6 @@
 pragma Style_Checks ("N3aAbcdefhiIklnOprStux");
 
-package body {prefix}RFLX_Utils with
+package body {prefix}RFLX_Arithmetic with
   SPARK_Mode
 is
 
@@ -60,4 +60,4 @@ is
       return Result;
    end Mod_Pow2;
 
-end {prefix}RFLX_Utils;
+end {prefix}RFLX_Arithmetic;
diff --git a/rflx/templates/rflx_utils.ads → rflx/templates/rflx_arithmetic.ads b/rflx/templates/rflx_utils.ads → rflx/templates/rflx_arithmetic.ads
@@ -1,6 +1,6 @@
 pragma Style_Checks ("N3aAbcdefhiIklnOprStux");
 
-package {prefix}RFLX_Utils with
+package {prefix}RFLX_Arithmetic with
   SPARK_Mode
 is
 
@@ -38,4 +38,4 @@ is
      Post =>
        Mod_Pow2'Result < 2**Exp;
 
-end {prefix}RFLX_Utils;
+end {prefix}RFLX_Arithmetic;
diff --git a/rflx/templates/rflx_generic_types.adb b/rflx/templates/rflx_generic_types.adb
@@ -1,6 +1,6 @@
 pragma Style_Checks ("N3aAbcdefhiIklnOprStux");
 
-with {prefix}RFLX_Utils; use {prefix}RFLX_Utils;
+with {prefix}RFLX_Arithmetic; use {prefix}RFLX_Arithmetic;
 
 package body {prefix}RFLX_Generic_Types with
   SPARK_Mode

diff --git a/test.gpr b/test.gpr
@@ -34,9 +34,9 @@ project Test is
       for Proof_Switches ("rflx-ethernet-frame.ads") use ("--steps=25000");
       for Proof_Switches ("rflx-ipv4-option.ads") use ("--steps=2000");
       for Proof_Switches ("rflx-ipv4-packet.ads") use ("--steps=14000");
+      for Proof_Switches ("rflx-rflx_arithmetic.adb") use ("--steps=30000");
+      for Proof_Switches ("rflx-rflx_arithmetic.ads") use ("--steps=30000");
       for Proof_Switches ("rflx-rflx_types.ads") use ("--steps=80000", "--prover=altergo,cvc4,z3");
-      for Proof_Switches ("rflx-rflx_utils.adb") use ("--steps=30000");
-      for Proof_Switches ("rflx-rflx_utils.ads") use ("--steps=30000");
       for Proof_Switches ("rflx-udp-datagram.ads") use ("--steps=4000");
 
       case AUnit is