Add some pre-conditions.

Part of S507-051.

Author: TurboGit

src/http2/aws-http2-frame-continuation.ads

@@ -45,7 +45,10 @@ package AWS.HTTP2.Frame.Continuation is
       Stream_Id   : HTTP2.Stream_Id;
       List        : Headers.List;
       End_Headers : Boolean := True) return Object
-     with Post => (if End_Headers then Create'Result.Flags = End_Headers_Flag);
+     with Pre  => Stream_Id /= 0,
+          Post => (if End_Headers then Create'Result.Flags = End_Headers_Flag)
+                  and then Create'Result.Kind = K_Continuation;
+   --  Create a CONTINUATION frame with given content
 
    overriding procedure Send_Payload
      (Self : Object; Sock : Net.Socket_Type'Class);
@@ -56,11 +59,13 @@ package AWS.HTTP2.Frame.Continuation is
    --  Iterator interface
 
    function Content_Length
-     (Self : Object) return Stream_Element_Count;
+     (Self : Object) return Stream_Element_Count
+     with Pre => Self.Is_Defined;
 
    function Get
      (Self  : Object;
-      Index : Stream_Element_Offset) return Stream_Element;
+      Index : Stream_Element_Offset) return Stream_Element
+     with Pre => Self.Is_Defined;
 
 private
 

src/http2/aws-http2-frame-data.ads

@@ -50,14 +50,16 @@ package AWS.HTTP2.Frame.Data is
    function Create
      (Stream_Id : HTTP2.Stream_Id;
       Content   : String) return Object
-     with Pre => Stream_Id > 0 and then Content'Length > 0;
+     with Pre  => Stream_Id > 0 and then Content'Length > 0,
+          Post => Create'Result.Kind = K_Data;
    --  Create a DATA frame with given content and stream id
 
    function Create
      (Stream_Id  : HTTP2.Stream_Id;
       Content    : Utils.Stream_Element_Array_Access;
       End_Stream : Boolean) return Object
-     with Pre => Stream_Id > 0 and then Content'Length > 0;
+     with Pre  => Stream_Id > 0 and then Content'Length > 0,
+          Post => Create'Result.Kind = K_Data;
    --  Create a DATA frame with given content and stream id
 
    overriding procedure Send_Payload

src/http2/aws-http2-frame-goaway.ads

@@ -45,7 +45,8 @@ package AWS.HTTP2.Frame.GoAway is
 
    function Create
      (Stream_Id : Stream.Id;
-      Error     : Error_Codes) return Object;
+      Error     : Error_Codes) return Object
+     with Post => Create'Result.Kind = K_GoAway;
    --  Create a GOAWAY frame with given content and stream id
 
    function Error (Self : Object) return Error_Codes

src/http2/aws-http2-frame-priority.ads

@@ -48,7 +48,8 @@ package AWS.HTTP2.Frame.Priority is
      (Stream_Id         : HTTP2.Stream_Id;
       Stream_Dependency : HTTP2.Stream_Id;
       Weight            : Byte_1) return Object
-     with Pre => Stream_Id /= Stream_Dependency;
+     with Pre  => Stream_Id /= Stream_Dependency,
+          Post => Create'Result.Kind = K_Priority;
    --  Create a PRIORITY frame (stream id is always 0)
 
    function Read

src/http2/aws-http2-frame-push_promise.ads

@@ -58,14 +58,16 @@ package AWS.HTTP2.Frame.Push_Promise is
       Promise_Stream_Id : HTTP2.Stream_Id;
       List              : AWS.Headers.List;
       End_Headers       : Boolean := True) return Object
-     with Post => (if End_Headers then Create'Result.Flags = End_Headers_Flag);
+     with Post => (if End_Headers then Create'Result.Flags = End_Headers_Flag)
+                  and then Create'Result.Kind = K_Push_Promise;
    --  Create an HEADERS frame with given content and stream id
 
    function Get
      (Self     : Object;
       Table    : not null access HTTP2.HPACK.Table.Object;
       Settings : not null access HTTP2.Connection.Object)
-      return AWS.Headers.List;
+      return AWS.Headers.List
+     with Pre => Self.Is_Defined;
    --  Get the header list out of the HEADERS frame. This reads the content of
    --  the payload and decode using HPACK.
 

src/http2/aws-http2-frame-rst_stream.ads

@@ -47,8 +47,10 @@ package AWS.HTTP2.Frame.RST_Stream is
 
    function Create
      (Error     : Error_Codes;
-      Stream_Id : Stream.Id) return Object;
-   --  Create an RST_Stream frame (stream id is 0)
+      Stream_Id : Stream.Id) return Object
+     with Pre  => Stream_Id /= 0,
+          Post => Create'Result.Kind = K_RST_Stream;
+   --  Create an RST_Stream frame
 
    overriding procedure Send_Payload
      (Self : Object; Sock : Net.Socket_Type'Class)

src/http2/aws-http2-frame.ads

@@ -124,7 +124,8 @@ package AWS.HTTP2.Frame is
      (Self     : Object'Class;
       Settings : Connection.Object;
       Error    : out Error_Codes) return Boolean
-     with Pre => Self.Is_Defined;
+     with Pre  => Self.Is_Defined,
+          Post => Is_Valid'Result = (Error = C_No_Error);
    --  Set Error to appropriate value with Validate routine and return True if
    --  Error became C_No_Error, returns False otherwise.
 

src/http2/aws-http2.ads

@@ -62,11 +62,13 @@ package AWS.HTTP2 is
    --  "PRI * HTTP/2.0" & CRLF & CRLF & "SM" & CRLF & CRLF
 
    function Exception_Message
-     (Error : Error_Codes; Message : String) return String;
+     (Error : Error_Codes; Message : String) return String
+     with Pre => Message /= "";
    --  Build an exception message with the error code endoded at the start of
    --  the message and surrounded with square brackets.
 
-   function Exception_Code (Exception_Message : String) return Error_Codes;
+   function Exception_Code (Exception_Message : String) return Error_Codes
+     with Pre => Exception_Message'Length > 2;
    --  Extract the execption code from an exception message built with the
    --  Exception_Message routine above.