verified Scala with Stainless

.gitignore

@@ -1,4 +1,8 @@
+.metals
+.vscode
 .idea
+.bloop
+.scala-build
 /.vs
 /Debug
 /Release

ADA_RTL2/src/adaasn1rtl-encoding-acn.adb

@@ -1428,7 +1428,7 @@ is
       strVal (strVal'Last) := Standard.Ascii.NUL;
    end Acn_Dec_String_Ascii_FixSize;
 
-   procedure Acn_Enc_String_Ascii_Null_Teminated
+   procedure Acn_Enc_String_Ascii_Null_Terminated
      (bs : in out Bitstream; null_characters : OctetBuffer; strVal : String)
    is
       i : Integer := strVal'First;
@@ -1449,9 +1449,9 @@ is
             bs.Current_Bit_Pos'Loop_Entry + (i - null_characters'First) * 8);
          BitStream_AppendByte (bs, null_characters (i), False);
       end loop;
-   end Acn_Enc_String_Ascii_Null_Teminated;
+   end Acn_Enc_String_Ascii_Null_Terminated;
 
-   procedure Acn_Dec_String_Ascii_Null_Teminated
+   procedure Acn_Dec_String_Ascii_Null_Terminated
      (bs     : in out Bitstream; null_characters : OctetBuffer;
       strVal : in out String; Result : out ASN1_RESULT)
    is
@@ -1519,7 +1519,7 @@ is
          I          := I + 1;
       end loop;
 
-   end Acn_Dec_String_Ascii_Null_Teminated;
+   end Acn_Dec_String_Ascii_Null_Terminated;
 
    procedure Acn_Enc_String_Ascii_Internal_Field_Determinant
      (bs                           : in out Bitstream; asn1Min : Asn1Int;
@@ -1597,7 +1597,7 @@ is
    end Acn_Enc_String_Ascii_External_Field_Determinant;
 
    procedure Acn_Dec_String_Ascii_External_Field_Determinant
-     (bs     : in out Bitstream; extSizeDeterminatFld : Asn1Int;
+     (bs     : in out Bitstream; extSizeDeterminantFld : Asn1Int;
       strVal : in out String; Result : out ASN1_RESULT)
    is
       I         : Integer := strVal'First;
@@ -1607,7 +1607,7 @@ is
         ASN1_RESULT'(Success => True, ErrorCode => ERR_INCORRECT_STREAM);
 
       while Result.Success and then I <= strVal'Last - 1
-        and then I <= Integer (extSizeDeterminatFld)
+        and then I <= Integer (extSizeDeterminantFld)
       loop
          pragma Loop_Invariant
            (I >= strVal'First and I <= strVal'Last and
@@ -1649,7 +1649,7 @@ is
 
    procedure Acn_Dec_String_CharIndex_External_Field_Determinant
      (bs : in out Bitstream; charSet : String; nCharSize : Integer;
-      extSizeDeterminatFld :        Asn1Int; strVal : out String;
+      extSizeDeterminantFld :        Asn1Int; strVal : out String;
       Result               :    out ASN1_RESULT)
    is
       I         : Integer          := strVal'First;
@@ -1660,7 +1660,7 @@ is
         ASN1_RESULT'(Success => True, ErrorCode => ERR_INCORRECT_STREAM);
       strVal := (others => Standard.Ascii.NUL);
       while Result.Success and then I <= strVal'Last - 1
-        and then I <= Integer (extSizeDeterminatFld)
+        and then I <= Integer (extSizeDeterminantFld)
       loop
          pragma Loop_Invariant
            (I >= strVal'First and I <= strVal'Last and

ADA_RTL2/src/adaasn1rtl-encoding-acn.ads

@@ -900,7 +900,7 @@ is
       bs.Current_Bit_Pos =
         bs'Old.Current_Bit_Pos + (strVal'Last - strVal'First) * 8;
 
-   procedure Acn_Enc_String_Ascii_Null_Teminated
+   procedure Acn_Enc_String_Ascii_Null_Terminated
      (bs     : in out Bitstream; null_characters : OctetBuffer;
       strVal :        String) with
       Depends => (bs => (bs, strVal, null_characters)),
@@ -919,7 +919,7 @@ is
         bs'Old.Current_Bit_Pos +
           (strVal'Length - 1 + null_characters'Length) * 8;
 
-   procedure Acn_Dec_String_Ascii_Null_Teminated
+   procedure Acn_Dec_String_Ascii_Null_Terminated
      (bs     : in out Bitstream; null_characters : OctetBuffer;
       strVal : in out String; Result : out ASN1_RESULT) with
       Pre => null_characters'Length >= 1 and then null_characters'Length <= 10
@@ -996,10 +996,10 @@ is
         bs'Old.Current_Bit_Pos + ((strVal'Last - strVal'First) * 8);
 
    procedure Acn_Dec_String_Ascii_External_Field_Determinant
-     (bs     : in out Bitstream; extSizeDeterminatFld : Asn1Int;
+     (bs     : in out Bitstream; extSizeDeterminantFld : Asn1Int;
       strVal : in out String; Result : out ASN1_RESULT) with
-      Pre => extSizeDeterminatFld >= 0
-      and then extSizeDeterminatFld <= Asn1Int (Integer'Last)
+      Pre => extSizeDeterminantFld >= 0
+      and then extSizeDeterminantFld <= Asn1Int (Integer'Last)
       and then strVal'Last < Natural'Last and then strVal'Last >= strVal'First
       and then strVal'Last - strVal'First < Natural'Last / 8 - 8
       and then bs.Current_Bit_Pos <
@@ -1032,10 +1032,10 @@ is
 
    procedure Acn_Dec_String_CharIndex_External_Field_Determinant
      (bs : in out Bitstream; charSet : String; nCharSize : Integer;
-      extSizeDeterminatFld :        Asn1Int; strVal : out String;
+      extSizeDeterminantFld :        Asn1Int; strVal : out String;
       Result               :    out ASN1_RESULT) with
-      Pre => extSizeDeterminatFld >= 0
-      and then extSizeDeterminatFld <= Asn1Int (Integer'Last)
+      Pre => extSizeDeterminantFld >= 0
+      and then extSizeDeterminantFld <= Asn1Int (Integer'Last)
       and then nCharSize >= 1 and then nCharSize <= 8
       and then strVal'Last < Natural'Last and then strVal'Last >= strVal'First
       and then charSet'Last < Natural'Last