+ More postconditions

* Added post conditions for the stream conversion functions.

Author: Jellix

artifacts/gnatprove.out

@@ -1,4 +1,4 @@
-date               : 2017-10-19 17:36:46
+date               : 2017-10-23 14:52:55
 gnatprove version  : 2017 (20170515)
 host               : Windows 32 bits
 command line       : gnatprove.exe --assumptions --output-header -P security.gpr
@@ -15,12 +15,12 @@ Data Dependencies                 .            .          .          .
 Flow Dependencies                 .            .          .          .                                       .           .          .
 Initialization                  171          164          .          .                                       .           7          .
 Non-Aliasing                      .            .          .          .                                       .           .          .
-Run-time Checks                 168            .          .          .    168 (CVC4  99%, Z3  1%, altergo  0%)           .          .
+Run-time Checks                 187            .          .          .    187 (CVC4  99%, Z3  1%, altergo  0%)           .          .
 Assertions                       22            .          .          .                  22 (CVC4  98%, Z3  2%)           .          .
-Functional Contracts             20            .          .          .                  20 (CVC4  99%, Z3  1%)           .          .
+Functional Contracts             21            .          .          .                  21 (CVC4  99%, Z3  1%)           .          .
 LSP Verification                  .            .          .          .                                       .           .          .
 -------------------------------------------------------------------------------------------------------------------------------------
-Total                           381    164 (43%)          .          .                               210 (55%)      7 (2%)          .
+Total                           401    164 (41%)          .          .                               230 (57%)      7 (2%)          .
 
 
 Analyzed 2 units
@@ -34,7 +34,7 @@ absence of run-time errors of Crypto.Oadd fully established
 the postcondition of Crypto.Oadd.Add_Carry fully established
 effects on parameters and Global variables of Crypto.Oadd.Add_Carry fully established
 absence of run-time errors of Crypto.Oadd.Add_Carry fully established
-  Crypto.To_Stream at crypto.ads:64 flow analyzed (0 errors and 0 warnings) and proved (9 checks)
+  Crypto.To_Stream at crypto.ads:64 flow analyzed (0 errors and 0 warnings) and proved (21 checks)
 the postcondition of Crypto.To_Stream depends on
   effects on parameters and Global variables of Interfaces.Shift_Right
   absence of run-time errors of Interfaces.Shift_Right
@@ -43,9 +43,15 @@ effects on parameters and Global variables of Crypto.To_Stream depends on
 absence of run-time errors of Crypto.To_Stream depends on
   effects on parameters and Global variables of Interfaces.Shift_Right
   absence of run-time errors of Interfaces.Shift_Right
-  Crypto.To_Unsigned at crypto.ads:75 flow analyzed (0 errors and 0 warnings) and proved (8 checks)
-effects on parameters and Global variables of Crypto.To_Unsigned fully established
-absence of run-time errors of Crypto.To_Unsigned fully established
+  Crypto.To_Unsigned at crypto.ads:79 flow analyzed (0 errors and 0 warnings) and proved (16 checks)
+the postcondition of Crypto.To_Unsigned depends on
+  effects on parameters and Global variables of Interfaces.Shift_Left
+  absence of run-time errors of Interfaces.Shift_Left
+effects on parameters and Global variables of Crypto.To_Unsigned depends on
+  effects on parameters and Global variables of Interfaces.Shift_Left
+absence of run-time errors of Crypto.To_Unsigned depends on
+  effects on parameters and Global variables of Interfaces.Shift_Left
+  absence of run-time errors of Interfaces.Shift_Left
 in unit crypto-phelix, 26 subprograms and packages out of 26 analyzed
   Crypto.Phelix at crypto-phelix.ads:57 flow analyzed (0 errors and 0 warnings) and proved (1 checks)
 absence of run-time errors of Crypto.Phelix fully established
@@ -75,65 +81,85 @@ absence of run-time errors of Crypto.Phelix.Ctx_Msg_Len fully established
     crypto-phelix.adb:163:41: "Destination" is initialized, there's an explicit assignment above
 the postcondition of Crypto.Phelix.Decrypt_Bytes depends on
   effects on parameters and Global variables of Interfaces.Rotate_Left
+  effects on parameters and Global variables of Interfaces.Shift_Left
   effects on parameters and Global variables of Interfaces.Shift_Right
   absence of run-time errors of Interfaces.Rotate_Left
+  absence of run-time errors of Interfaces.Shift_Left
   absence of run-time errors of Interfaces.Shift_Right
 effects on parameters and Global variables of Crypto.Phelix.Decrypt_Bytes depends on
   effects on parameters and Global variables of Interfaces.Rotate_Left
+  effects on parameters and Global variables of Interfaces.Shift_Left
   effects on parameters and Global variables of Interfaces.Shift_Right
 absence of run-time errors of Crypto.Phelix.Decrypt_Bytes depends on
   effects on parameters and Global variables of Interfaces.Rotate_Left
+  effects on parameters and Global variables of Interfaces.Shift_Left
   effects on parameters and Global variables of Interfaces.Shift_Right
   absence of run-time errors of Interfaces.Rotate_Left
+  absence of run-time errors of Interfaces.Shift_Left
   absence of run-time errors of Interfaces.Shift_Right
   Crypto.Phelix.Decrypt_Packet at crypto-phelix.ads:150 flow analyzed (0 errors and 0 warnings) and proved (10 checks)
    suppressed messages:
     crypto-phelix.adb:210:65: Full assignment is split between Msg_Header, and Msg_Body in Decrypt_Bytes.
 the postcondition of Crypto.Phelix.Decrypt_Packet depends on
   effects on parameters and Global variables of Interfaces.Rotate_Left
+  effects on parameters and Global variables of Interfaces.Shift_Left
   effects on parameters and Global variables of Interfaces.Shift_Right
   absence of run-time errors of Interfaces.Rotate_Left
+  absence of run-time errors of Interfaces.Shift_Left
   absence of run-time errors of Interfaces.Shift_Right
 effects on parameters and Global variables of Crypto.Phelix.Decrypt_Packet depends on
   effects on parameters and Global variables of Interfaces.Rotate_Left
+  effects on parameters and Global variables of Interfaces.Shift_Left
   effects on parameters and Global variables of Interfaces.Shift_Right
 absence of run-time errors of Crypto.Phelix.Decrypt_Packet depends on
   effects on parameters and Global variables of Interfaces.Rotate_Left
+  effects on parameters and Global variables of Interfaces.Shift_Left
   effects on parameters and Global variables of Interfaces.Shift_Right
   absence of run-time errors of Interfaces.Rotate_Left
+  absence of run-time errors of Interfaces.Shift_Left
   absence of run-time errors of Interfaces.Shift_Right
   Crypto.Phelix.Encrypt_Bytes at crypto-phelix.ads:251 flow analyzed (0 errors and 0 warnings) and proved (35 checks)
    suppressed messages:
     crypto-phelix.ads:253:29: Encrypt_Bytes ensures full initialization of "Destination".
     crypto-phelix.adb:265:41: "Destination" is initialized, there's an explicit assignment above
 the postcondition of Crypto.Phelix.Encrypt_Bytes depends on
   effects on parameters and Global variables of Interfaces.Rotate_Left
+  effects on parameters and Global variables of Interfaces.Shift_Left
   effects on parameters and Global variables of Interfaces.Shift_Right
   absence of run-time errors of Interfaces.Rotate_Left
+  absence of run-time errors of Interfaces.Shift_Left
   absence of run-time errors of Interfaces.Shift_Right
 effects on parameters and Global variables of Crypto.Phelix.Encrypt_Bytes depends on
   effects on parameters and Global variables of Interfaces.Rotate_Left
+  effects on parameters and Global variables of Interfaces.Shift_Left
   effects on parameters and Global variables of Interfaces.Shift_Right
 absence of run-time errors of Crypto.Phelix.Encrypt_Bytes depends on
   effects on parameters and Global variables of Interfaces.Rotate_Left
+  effects on parameters and Global variables of Interfaces.Shift_Left
   effects on parameters and Global variables of Interfaces.Shift_Right
   absence of run-time errors of Interfaces.Rotate_Left
+  absence of run-time errors of Interfaces.Shift_Left
   absence of run-time errors of Interfaces.Shift_Right
   Crypto.Phelix.Encrypt_Packet at crypto-phelix.ads:112 flow analyzed (0 errors and 0 warnings) and proved (11 checks)
    suppressed messages:
     crypto-phelix.adb:311:65: Full assignment is split between Msg_Header, and Msg_Body in Encrypt_Bytes.
 the postcondition of Crypto.Phelix.Encrypt_Packet depends on
   effects on parameters and Global variables of Interfaces.Rotate_Left
+  effects on parameters and Global variables of Interfaces.Shift_Left
   effects on parameters and Global variables of Interfaces.Shift_Right
   absence of run-time errors of Interfaces.Rotate_Left
+  absence of run-time errors of Interfaces.Shift_Left
   absence of run-time errors of Interfaces.Shift_Right
 effects on parameters and Global variables of Crypto.Phelix.Encrypt_Packet depends on
   effects on parameters and Global variables of Interfaces.Rotate_Left
+  effects on parameters and Global variables of Interfaces.Shift_Left
   effects on parameters and Global variables of Interfaces.Shift_Right
 absence of run-time errors of Crypto.Phelix.Encrypt_Packet depends on
   effects on parameters and Global variables of Interfaces.Rotate_Left
+  effects on parameters and Global variables of Interfaces.Shift_Left
   effects on parameters and Global variables of Interfaces.Shift_Right
   absence of run-time errors of Interfaces.Rotate_Left
+  absence of run-time errors of Interfaces.Shift_Left
   absence of run-time errors of Interfaces.Shift_Right
   Crypto.Phelix.Exclusive_Or at crypto-phelix.adb:27 flow analyzed (0 errors and 0 warnings) and proved (6 checks)
 the postcondition of Crypto.Phelix.Exclusive_Or fully established
@@ -173,45 +199,72 @@ absence of run-time errors of Crypto.Phelix.MAC_Size_32Predicate fully establish
   Crypto.Phelix.Process_AAD at crypto-phelix.ads:226 flow analyzed (0 errors and 0 warnings) and proved (15 checks)
 the postcondition of Crypto.Phelix.Process_AAD depends on
   effects on parameters and Global variables of Interfaces.Rotate_Left
+  effects on parameters and Global variables of Interfaces.Shift_Left
   absence of run-time errors of Interfaces.Rotate_Left
+  absence of run-time errors of Interfaces.Shift_Left
 effects on parameters and Global variables of Crypto.Phelix.Process_AAD depends on
   effects on parameters and Global variables of Interfaces.Rotate_Left
+  effects on parameters and Global variables of Interfaces.Shift_Left
 absence of run-time errors of Crypto.Phelix.Process_AAD depends on
   effects on parameters and Global variables of Interfaces.Rotate_Left
+  effects on parameters and Global variables of Interfaces.Shift_Left
   absence of run-time errors of Interfaces.Rotate_Left
+  absence of run-time errors of Interfaces.Shift_Left
   Crypto.Phelix.Setup_Key at crypto-phelix.ads:183 flow analyzed (0 errors and 0 warnings) and proved (33 checks)
 the postcondition of Crypto.Phelix.Setup_Key depends on
   effects on parameters and Global variables of Interfaces.Rotate_Left
+  effects on parameters and Global variables of Interfaces.Shift_Left
   absence of run-time errors of Interfaces.Rotate_Left
+  absence of run-time errors of Interfaces.Shift_Left
 effects on parameters and Global variables of Crypto.Phelix.Setup_Key depends on
   effects on parameters and Global variables of Interfaces.Rotate_Left
+  effects on parameters and Global variables of Interfaces.Shift_Left
 absence of run-time errors of Crypto.Phelix.Setup_Key depends on
   effects on parameters and Global variables of Interfaces.Rotate_Left
+  effects on parameters and Global variables of Interfaces.Shift_Left
   absence of run-time errors of Interfaces.Rotate_Left
+  absence of run-time errors of Interfaces.Shift_Left
   Crypto.Phelix.Setup_Key_Called at crypto-phelix.ads:97 flow analyzed (0 errors and 0 warnings) and proved (0 checks)
 effects on parameters and Global variables of Crypto.Phelix.Setup_Key_Called fully established
 absence of run-time errors of Crypto.Phelix.Setup_Key_Called fully established
   Crypto.Phelix.Setup_Nonce at crypto-phelix.ads:202 flow analyzed (0 errors and 0 warnings) and proved (8 checks)
 the postcondition of Crypto.Phelix.Setup_Nonce depends on
   effects on parameters and Global variables of Interfaces.Rotate_Left
+  effects on parameters and Global variables of Interfaces.Shift_Left
   absence of run-time errors of Interfaces.Rotate_Left
+  absence of run-time errors of Interfaces.Shift_Left
 effects on parameters and Global variables of Crypto.Phelix.Setup_Nonce depends on
   effects on parameters and Global variables of Interfaces.Rotate_Left
+  effects on parameters and Global variables of Interfaces.Shift_Left
 absence of run-time errors of Crypto.Phelix.Setup_Nonce depends on
   effects on parameters and Global variables of Interfaces.Rotate_Left
+  effects on parameters and Global variables of Interfaces.Shift_Left
   absence of run-time errors of Interfaces.Rotate_Left
+  absence of run-time errors of Interfaces.Shift_Left
   Crypto.Phelix.Setup_Nonce_Called at crypto-phelix.ads:101 flow analyzed (0 errors and 0 warnings) and proved (0 checks)
 effects on parameters and Global variables of Crypto.Phelix.Setup_Nonce_Called fully established
 absence of run-time errors of Crypto.Phelix.Setup_Nonce_Called fully established
   Crypto.Phelix.To_Unsigned at crypto-phelix.adb:38 flow analyzed (0 errors and 0 warnings) and proved (0 checks)
-effects on parameters and Global variables of Crypto.Phelix.To_Unsigned fully established
-absence of run-time errors of Crypto.Phelix.To_Unsigned fully established
+effects on parameters and Global variables of Crypto.Phelix.To_Unsigned depends on
+  effects on parameters and Global variables of Interfaces.Shift_Left
+absence of run-time errors of Crypto.Phelix.To_Unsigned depends on
+  effects on parameters and Global variables of Interfaces.Shift_Left
+  absence of run-time errors of Interfaces.Shift_Left
   Crypto.Phelix.To_Unsigned at crypto-phelix.adb:46 flow analyzed (0 errors and 0 warnings) and proved (0 checks)
-effects on parameters and Global variables of Crypto.Phelix.To_Unsigned fully established
-absence of run-time errors of Crypto.Phelix.To_Unsigned fully established
+effects on parameters and Global variables of Crypto.Phelix.To_Unsigned depends on
+  effects on parameters and Global variables of Interfaces.Shift_Left
+absence of run-time errors of Crypto.Phelix.To_Unsigned depends on
+  effects on parameters and Global variables of Interfaces.Shift_Left
+  absence of run-time errors of Interfaces.Shift_Left
   Crypto.Phelix.To_Unsigned at crypto-phelix.adb:54 flow analyzed (0 errors and 0 warnings) and proved (0 checks)
-effects on parameters and Global variables of Crypto.Phelix.To_Unsigned fully established
-absence of run-time errors of Crypto.Phelix.To_Unsigned fully established
+effects on parameters and Global variables of Crypto.Phelix.To_Unsigned depends on
+  effects on parameters and Global variables of Interfaces.Shift_Left
+absence of run-time errors of Crypto.Phelix.To_Unsigned depends on
+  effects on parameters and Global variables of Interfaces.Shift_Left
+  absence of run-time errors of Interfaces.Shift_Left
   Crypto.Phelix.To_Unsigned at crypto-phelix.adb:62 flow analyzed (0 errors and 0 warnings) and proved (0 checks)
-effects on parameters and Global variables of Crypto.Phelix.To_Unsigned fully established
-absence of run-time errors of Crypto.Phelix.To_Unsigned fully established
+effects on parameters and Global variables of Crypto.Phelix.To_Unsigned depends on
+  effects on parameters and Global variables of Interfaces.Shift_Left
+absence of run-time errors of Crypto.Phelix.To_Unsigned depends on
+  effects on parameters and Global variables of Interfaces.Shift_Left
+  absence of run-time errors of Interfaces.Shift_Left

src/crypto.ads

@@ -64,7 +64,11 @@ is
    function To_Stream (Value : in Word_32) return General_Stream with
      Global  => null,
      Depends => (To_Stream'Result => Value),
-     Post    => (To_Stream'Result'Length = 4 and To_Stream'Result'First = 0);
+     Post    => ((To_Stream'Result'Length = 4 and To_Stream'Result'First = 0) and then
+                 To_Stream'Result = (0 => Byte (Shift_Right (Value,  0) mod 256),
+                                     1 => Byte (Shift_Right (Value,  8) mod 256),
+                                     2 => Byte (Shift_Right (Value, 16) mod 256),
+                                     3 => Byte (Shift_Right (Value, 24) mod 256)));
 
    --
    --  To_Unsigned
@@ -74,7 +78,11 @@ is
    --
    function To_Unsigned (Value : in General_Stream) return Word_32 with
      Global  => null,
-     Depends => (To_Unsigned'Result => (Value));
+     Depends => (To_Unsigned'Result => (Value)),
+     Post    => (To_Unsigned'Result = (if Value'Length > 0 then (Shift_Left (Word_32 (Value (Value'First)),      0)) else 0) +
+                                      (if Value'Length > 1 then (Shift_Left (Word_32 (Value (Value'First + 1)),  8)) else 0) +
+                                      (if Value'Length > 2 then (Shift_Left (Word_32 (Value (Value'First + 2)), 16)) else 0) +
+                                      (if Value'Length > 3 then (Shift_Left (Word_32 (Value (Value'First + 3)), 24)) else 0));
 
 private
 
@@ -83,10 +91,10 @@ private
    --
    function To_Stream (Value : in Word_32) return General_Stream is
      (General_Stream'
-       (0 => Byte (Shift_Right (Value,  0) mod 256),
-        1 => Byte (Shift_Right (Value,  8) mod 256),
-        2 => Byte (Shift_Right (Value, 16) mod 256),
-        3 => Byte (Shift_Right (Value, 24) mod 256)));
+       (0 => Byte (Value / 2 **  0 mod 256),
+        1 => Byte (Value / 2 **  8 mod 256),
+        2 => Byte (Value / 2 ** 16 mod 256),
+        3 => Byte (Value / 2 ** 24 mod 256)));
 
    --
    --  To_Unsigned