Regenerate projects with latest Alire (#3)

* Regenerated the cobs and unit_tests projects with Alire 1.2.0.
* Use default style checks generated by Alire in validation builds:
  * Removed explicit 'in' mode.
  * Reduced line lengths to fit in 80 columns.
* Added a nested crate used to run gnatprove.

Author: damaki

.gitignore

@@ -1,3 +1,4 @@
-obj
-lib
-alire
+/obj/
+/lib/
+/alire/
+/config/

alire.toml

@@ -1,21 +1,10 @@
 name = "cobs"
-description = "Encoder and decoder for Consistent Overhead Byte Stuffing (COBS)"
-version = "1.0.1"
+description = "Consistent Overhead Byte Stuffing (COBS) encoder/decoder"
+version = "1.1.0-dev"
 
-licenses = ["MIT"]
+licenses = "MIT"
 authors = ["Daniel King"]
 maintainers = ["Daniel King <damaki.gh@gmail.com>"]
 maintainers-logins = ["damaki"]
 website = "https://github.com/damaki/cobs"
-tags = ["cobs", "spark", "embedded", "nostd"]
-
-[[depends-on]]
-gnat = ">=2020"
-
-[gpr-externals]
-COBS_LIBRARY_TYPE = ["relocatable", "static", "static-pic"]
-COBS_COMPILE_CHECKS = ["enabled", "disabled"]
-COBS_RUNTIME_CHECKS = ["enabled", "disabled"]
-COBS_STYLE_CHECKS = ["enabled", "disabled"]
-COBS_CONTRACTS = ["enabled", "disabled"]
-COBS_BUILD_MODE = ["debug", "optimize"]
+tags = ["cobs", "spark", "embedded", "nostd"]

cobs.gpr

@@ -1,10 +1,11 @@
+with "config/cobs_config.gpr";
 project Cobs is
 
-   for Library_Name use "cobs";
-   for Library_Version use "1.0.1";
+   for Library_Name use "Cobs";
+   for Library_Version use Project'Library_Name & ".so." & Cobs_Config.Crate_Version;
 
-   for Source_Dirs use ("src");
-   for Object_Dir use "obj";
+   for Source_Dirs use ("src/", "config/");
+   for Object_Dir use "obj/" & Cobs_Config.Build_Profile;
    for Create_Missing_Dirs use "True";
    for Library_Dir use "lib";
 
@@ -13,77 +14,29 @@ project Cobs is
      external ("COBS_LIBRARY_TYPE", external ("LIBRARY_TYPE", "static"));
    for Library_Kind use Library_Type;
 
-   type Enabled_Kind is ("enabled", "disabled");
-   Compile_Checks : Enabled_Kind := External ("COBS_COMPILE_CHECKS", "enabled");
-   Runtime_Checks : Enabled_Kind := External ("COBS_RUNTIME_CHECKS", "enabled");
-   Style_Checks : Enabled_Kind := External ("COBS_STYLE_CHECKS", "enabled");
-   Contracts_Checks : Enabled_Kind := External ("COBS_CONTRACTS", "enabled");
-
-   type Build_Kind is ("debug", "optimize");
-   Build_Mode : Build_Kind := External ("COBS_BUILD_MODE", "debug");
-
-   Compile_Checks_Switches := ();
-   case Compile_Checks is
-      when "enabled" =>
-         Compile_Checks_Switches :=
-           ("-gnatwa",  -- All warnings
-            "-gnatVa",  -- All validity checks
-            "-gnatw.X", -- Disable warning may call Last_Chance_Handler
-            "-gnatwe"); -- Warnings as errors
-      when others => null;
-   end case;
-
-   Runtime_Checks_Switches := ();
-   case Runtime_Checks is
-      when "enabled" => null;
-      when others =>
-         Runtime_Checks_Switches :=
-           ("-gnatp"); -- Supress checks
-   end case;
-
-   Style_Checks_Switches := ();
-   case Style_Checks is
-      when "enabled" => null;
-         Style_Checks_Switches :=
-           ("-gnatyg",    -- GNAT Style checks
-            "-gnaty-d",   -- Disable no DOS line terminators
-            "-gnaty-I",   -- Disable check mode IN keywords
-            "-gnatyM100", -- Maximum line length
-            "-gnatyO");   -- Overriding subprograms explicitly marked as such
-      when others => null;
-   end case;
-
-   Contracts_Switches := ();
-   case Contracts_Checks is
-      when "enabled" => null;
-         Contracts_Switches :=
-           ("-gnata"); --  Enable assertions and contracts
-      when others =>
-   end case;
-
-   Compiler_Switches := ();
-   case Build_Mode is
-      when "optimize" =>
-         Compiler_Switches := ("-O3",            -- Optimization
-                               "-funroll-loops", -- Unroll loops
-                               "-gnatn");        -- Enable inlining
-      when "debug" =>
-         Compiler_Switches := ("-g",   -- Debug info
-                               "-Og"); -- No optimization
-   end case;
-
    package Compiler is
-      for Default_Switches ("Ada") use
-        Compile_Checks_Switches &
-        Compiler_Switches &
-        Runtime_Checks_Switches &
-        Style_Checks_Switches &
-        Contracts_Switches &
-        ("-gnatQ");  -- Don't quit. Generate ALI and tree files even if illegalities
+      for Default_Switches ("Ada") use Cobs_Config.Ada_Compiler_Switches;
    end Compiler;
 
    package Binder is
       for Switches ("Ada") use ("-Es"); --  Symbolic traceback
    end Binder;
 
-end Cobs;
+   package Install is
+      for Artifacts (".") use ("share");
+   end Install;
+
+   package Prove is
+      for Proof_Switches ("Ada") use ("--proof=per_path",
+                                      "-j0",
+                                      "--no-global-generation",
+                                      "--no-inlining",
+                                      "--no-loop-unrolling",
+                                      "--prover=cvc4,z3,altergo",
+                                      "--timeout=60",
+                                      "--memlimit=0",
+                                      "--steps=15000",
+                                      "--report=statistics");
+   end Prove;
+
+end Cobs;

prove/.gitignore

@@ -0,0 +1,4 @@
+/obj/
+/bin/
+/alire/
+/config/

prove/alire.toml

@@ -0,0 +1,16 @@
+name = "prove"
+description = "Shiny new project"
+version = "0.1.0-dev"
+
+authors = ["Daniel King"]
+maintainers = ["Daniel King <damaki.gh@gmail.com>"]
+maintainers-logins = ["damaki"]
+
+executables = ["prove"]
+
+[[depends-on]]
+gnatprove = "^11.2.3"
+cobs = "*"
+
+[[pins]]
+cobs = { path = "../" }

src/generic_cobs.adb

@@ -27,9 +27,9 @@ is
    -- Decode --
    ------------
 
-   procedure Decode (Input  : in     Byte_Array;
-                     Output :    out Byte_Array;
-                     Length :    out Byte_Count) is
+   procedure Decode (Input  :     Byte_Array;
+                     Output : out Byte_Array;
+                     Length : out Byte_Count) is
       B          : Byte;
       Code       : Byte := Byte'Last;
       Run_Length : Byte_Count := 0;
@@ -39,8 +39,10 @@ is
 
       for I in 0 .. Index'Base (Input'Length - 1) loop
          pragma Loop_Invariant (Length <= Byte_Count (I));
-         pragma Loop_Invariant (for all J in 0 .. Length - 1 =>
-                                  Output (Output'First + Index'Base (J))'Initialized);
+
+         pragma Loop_Invariant
+           (for all J in 0 .. Length - 1 =>
+              Output (Output'First + Index'Base (J))'Initialized);
 
          B := Input (Input'First + I);
 
@@ -70,9 +72,9 @@ is
    -- Encode --
    ------------
 
-   procedure Encode (Input  : in     Byte_Array;
-                     Output :    out Byte_Array;
-                     Length :    out Byte_Count) is
+   procedure Encode (Input  :     Byte_Array;
+                     Output : out Byte_Array;
+                     Length : out Byte_Count) is
       Block_Length : Positive_Byte_Count;
       Offset       : Byte_Count;
       Remaining    : Byte_Count;
@@ -92,16 +94,23 @@ is
                               Increases => Offset,
                               Increases => Length,
                               Increases => Nb_Overhead_Bytes);
+
          pragma Loop_Invariant (Offset + Remaining = Input'Length);
+
          pragma Loop_Invariant (Length = Offset + Nb_Overhead_Bytes);
-         pragma Loop_Invariant (Nb_Overhead_Bytes < Max_Overhead_Bytes (Offset));
-         pragma Loop_Invariant (for all I in Output'First ..
-                                             Output'First + Index'Base (Length - 1) =>
-                                  Output (I)'Initialized);
 
-         Encode_Block (Input  (Input'First  + Index'Base (Offset) .. Input'Last),
-                       Output (Output'First + Index'Base (Length) .. Output'Last),
-                       Block_Length);
+         pragma Loop_Invariant
+           (Nb_Overhead_Bytes < Max_Overhead_Bytes (Offset));
+
+         pragma Loop_Invariant
+           (for all I in Output'First ..
+                         Output'First + Index'Base (Length - 1) =>
+                Output (I)'Initialized);
+
+         Encode_Block
+           (Input  (Input'First  + Index'Base (Offset) .. Input'Last),
+            Output (Output'First + Index'Base (Length) .. Output'Last),
+            Block_Length);
 
          Nb_Overhead_Bytes := Nb_Overhead_Bytes + 1;
 
@@ -119,9 +128,9 @@ is
    --  Encode_Block  --
    --------------------
 
-   procedure Encode_Block (Input  : in     Byte_Array;
-                           Output :    out Byte_Array;
-                           Length :    out Byte_Count) is
+   procedure Encode_Block (Input  :     Byte_Array;
+                           Output : out Byte_Array;
+                           Length : out Byte_Count) is
       B : Byte;
 
       Code : Positive_Byte_Count  := 1;
@@ -142,14 +151,22 @@ is
       if Input'Length > 0 then
          for I in Byte_Count range 0 .. Input'Length - 1 loop
             pragma Loop_Invariant (Code <= Maximum_Run_Length + 1);
-            pragma Loop_Invariant (Code = Length - Byte_Count (Code_Pos - Output'First));
-            pragma Loop_Invariant (Code_Pos in Output'First ..
-                                               Output'First + Index'Base (Length) - 1);
+
+            pragma Loop_Invariant
+              (Code = Length - Byte_Count (Code_Pos - Output'First));
+
+            pragma Loop_Invariant
+              (Code_Pos in Output'First ..
+                           Output'First + Index'Base (Length) - 1);
+
             pragma Loop_Invariant (Length = Byte_Count (I + 1));
-            pragma Loop_Invariant (for all I in Output'First ..
-                                                Output'First + Index'Base (Length) - 1 =>
-                                     (if I /= Code_Pos then
-                                         Output (I)'Initialized));
+
+            --  All bytes written so far are initialized, except the
+            --  one at Code_Pos which is written later.
+            pragma Loop_Invariant
+              (for all I in Output'First ..
+                            Output'First + Index'Base (Length) - 1 =>
+                   (if I /= Code_Pos then Output (I)'Initialized));
 
             --  Stop when a complete block is reached.
             exit when Code = Maximum_Run_Length + 1;