Skip to content

Commit d575d0f

Browse files
mgrojomgrojo
committed
Fix some failing VCs in Messages.Encoding
And removed the type derivation for `Status_Type` in the client session, which doesn't make much sense any longer.
1 parent 1199b02 commit d575d0f

7 files changed

Lines changed: 51 additions & 32 deletions

‎src/coap_spark-client_session.adb‎

Lines changed: 1 addition & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1,18 +1,15 @@
11
with CoAP_SPARK.Log;
22

3-
with RFLX.CoAP_Client.Session_Environment;
43
with RFLX.RFLX_Types;
54
with RFLX.RFLX_Builtin_Types;
65

76
package body CoAP_SPARK.Client_Session
87
with SPARK_Mode
98
is
109

11-
package Session_Environment renames RFLX.CoAP_Client.Session_Environment;
1210
package Types renames RFLX.RFLX_Types;
1311
package Channel renames CoAP_SPARK.Channel;
1412

15-
use type Session_Environment.Status_Type;
1613
use type Types.Index;
1714

1815
procedure Read (Ctx : FSM.Context;
@@ -99,8 +96,7 @@ is
9996

10097
if not CoAP_SPARK.Channel.Is_Valid (Skt) then
10198
CoAP_SPARK.Log.Put_Line ("Communication problems.", CoAP_SPARK.Log.Error);
102-
Ctx.E.Current_Status :=
103-
Session_Environment.Communication_Problems;
99+
Ctx.E.Current_Status := CoAP_SPARK.Communication_Problems;
104100
end if;
105101

106102
end Run_Session_Loop;

‎src/coap_spark-messages-encoding.adb‎

Lines changed: 2 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -183,10 +183,8 @@ is
183183
(Options_And_Payload : Content;
184184
Status : out CoAP_SPARK.Status_Type;
185185
Encoded_Data : out RFLX.RFLX_Types.Bytes;
186-
Encoded_Length : out RFLX.CoAP.Length_16)
186+
Encoded_Length : out RFLX.RFLX_Types.Length)
187187
is
188-
use type RFLX.CoAP.Length_16;
189-
190188
Option_Sequence_Cxt : RFLX.CoAP.Option_Sequence.Context;
191189
Option_Sequence_Buffer : RFLX.RFLX_Types.Bytes_Ptr :=
192190
new RFLX.RFLX_Types.Bytes'
@@ -252,7 +250,7 @@ is
252250
RFLX.CoAP.Option_Sequence.Copy
253251
(Ctx => Option_Sequence_Cxt,
254252
Buffer => Encoded_Data (1 .. Last));
255-
Encoded_Length := RFLX.CoAP.Length_16 (Last);
253+
Encoded_Length := RFLX.RFLX_Types.Length (Last);
256254

257255
Status := OK;
258256
elsif Last = 0 then

‎src/coap_spark-messages-encoding.ads‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,7 @@ is
1010
(Options_And_Payload : Content;
1111
Status : out CoAP_SPARK.Status_Type;
1212
Encoded_Data : out RFLX.RFLX_Types.Bytes;
13-
Encoded_Length : out RFLX.CoAP.Length_16)
13+
Encoded_Length : out RFLX.RFLX_Types.Length)
1414
with Pre => Encoded_Data'First = RFLX.RFLX_Types.Index'First;
1515

1616
procedure Decode_Options_And_Payload

‎src/rflx-coap_client-session.adb‎

Lines changed: 15 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -12,7 +12,7 @@ is
1212
begin
1313

1414
RFLX_Result := State.Method;
15-
State.Current_Status := RFLX.CoAP_Client.Session_Environment.OK;
15+
State.Current_Status := CoAP_SPARK.OK;
1616

1717
end Get_Method;
1818

@@ -71,14 +71,23 @@ is
7171
(State : in out RFLX.CoAP_Client.Session_Environment.State;
7272
RFLX_Result : out RFLX.CoAP_Client.Options_And_Payload_Data.Structure)
7373
is
74+
use type RFLX.RFLX_Types.Length;
75+
Encoded_Length : RFLX.RFLX_Types.Length;
7476
begin
7577

7678
CoAP_SPARK.Messages.Encoding.Encode_Options_And_Payload
7779
(Options_And_Payload => State.Request_Content,
78-
Status => CoAP_SPARK.Status_Type (State.Current_Status),
80+
Status => State.Current_Status,
7981
Encoded_Data => RFLX_Result.Options_And_Payload,
80-
Encoded_Length => RFLX_Result.Length);
82+
Encoded_Length => Encoded_Length);
8183

84+
if Encoded_Length > RFLX.RFLX_Types.Length (RFLX.CoAP.Length_16'Last) then
85+
State.Current_Status := CoAP_SPARK.Capacity_Error;
86+
RFLX_Result.Length := 0;
87+
else
88+
RFLX_Result.Length :=
89+
RFLX.CoAP.Length_16 (Encoded_Length);
90+
end if;
8291
end Get_Options_And_Payload;
8392

8493

@@ -87,7 +96,7 @@ is
8796
Data : RFLX_Types.Bytes;
8897
RFLX_Result : out Boolean)
8998
is
90-
use type CoAP_Client.Session_Environment.Status_Type;
99+
use type CoAP_SPARK.Status_Type;
91100
begin
92101

93102
if not CoAP_SPARK.Messages.Is_Empty (State.Response_Content) then
@@ -97,11 +106,11 @@ is
97106

98107
CoAP_SPARK.Messages.Encoding.Decode_Options_And_Payload
99108
(Data => Data,
100-
Status => CoAP_SPARK.Status_Type (State.Current_Status),
109+
Status => State.Current_Status,
101110
Decoded_Content => State.Response_Content);
102111

103112
RFLX_Result :=
104-
State.Current_Status = RFLX.CoAP_Client.Session_Environment.OK;
113+
State.Current_Status = CoAP_SPARK.OK;
105114

106115
end Put_Options_And_Payload;
107116

‎src/rflx-coap_client-session_environment.adb‎

Lines changed: 8 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -18,7 +18,7 @@ is
1818
Separator : Character;
1919
Number : RFLX.CoAP.Option_Numbers;
2020
Option_List : in out CoAP_SPARK.Options.Lists.Vector;
21-
Status : in out Status_Type) with
21+
Status : in out CoAP_SPARK.Status_Type) with
2222
Always_Terminates,
2323
Pre => CoAP_SPARK.Options.Option_Properties_Table (Number).Repeatable
2424
and then CoAP_SPARK.Options.Option_Properties_Table (Number).Format =
@@ -58,7 +58,7 @@ is
5858
or else CoAP_SPARK.Options.Lists.Length (Option_List) =
5959
CoAP_SPARK.Max_Number_Of_Options
6060
then
61-
Status := Capacity_Error;
61+
Status := CoAP_SPARK.Capacity_Error;
6262
return;
6363
end if;
6464

@@ -75,7 +75,7 @@ is
7575
exit when Segment_Last >= Source'Last;
7676

7777
if Order_Index = CoAP_SPARK.Options.Option_Index'Last then
78-
Status := Capacity_Error;
78+
Status := CoAP_SPARK.Capacity_Error;
7979
return;
8080
end if;
8181

@@ -107,9 +107,10 @@ is
107107
Session_State : out State)
108108
is
109109
use type RFLX.RFLX_Types.Bytes_Ptr;
110+
use type CoAP_SPARK.Status_Type;
110111
begin
111112
Session_State.Method := Method;
112-
Session_State.Current_Status := OK;
113+
Session_State.Current_Status := CoAP_SPARK.OK;
113114
Session_State.Is_First_Message := True;
114115
Session_State.Current_Message_ID := 0;
115116
Session_State.Request_Content :=
@@ -154,7 +155,7 @@ is
154155
Option_List => Session_State.Request_Content.Options,
155156
Status => Session_State.Current_Status);
156157

157-
if Session_State.Current_Status = OK then
158+
if Session_State.Current_Status = CoAP_SPARK.OK then
158159
-- RFC7252: each Uri-Query Option specifies one argument parameterizing the
159160
-- resource.
160161
Split_String_In_Repeatable_Options
@@ -164,15 +165,15 @@ is
164165
Option_List => Session_State.Request_Content.Options,
165166
Status => Session_State.Current_Status);
166167

167-
if Session_State.Current_Status = OK
168+
if Session_State.Current_Status = CoAP_SPARK.OK
168169
and then
169170
Session_State.Request_Content.Payload /= null
170171
then
171172
if CoAP_SPARK.Options.Lists.Length
172173
(Session_State.Request_Content.Options)
173174
= CoAP_SPARK.Max_Number_Of_Options
174175
then
175-
Session_State.Current_Status := Capacity_Error;
176+
Session_State.Current_Status := CoAP_SPARK.Capacity_Error;
176177
else
177178
CoAP_SPARK.Options.New_UInt_Option
178179
(Number => RFLX.CoAP.Content_Format,

‎src/rflx-coap_client-session_environment.ads‎

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -10,11 +10,9 @@ package RFLX.CoAP_Client.Session_Environment with
1010
SPARK_Mode
1111
is
1212

13-
type Status_Type is new CoAP_SPARK.Status_Type;
14-
1513
type State is record
1614
Method : RFLX.CoAP.Method_Code := RFLX.CoAP.Get;
17-
Current_Status : Status_Type := OK;
15+
Current_Status : CoAP_SPARK.Status_Type := CoAP_SPARK.OK;
1816
Is_First_Message : Boolean := True;
1917
Current_Message_ID : RFLX.CoAP.Message_ID_Type := 0;
2018
Request_Content : CoAP_SPARK.Messages.Content;

‎src/rflx-coap_server-main_loop.adb‎

Lines changed: 23 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -13,6 +13,7 @@ with CoAP_SPARK.Log;
1313

1414
with RFLX.CoAP;
1515
with RFLX.CoAP.CoAP_Message;
16+
with RFLX.RFLX_Types;
1617

1718
package body RFLX.CoAP_Server.Main_Loop
1819
with SPARK_Mode
@@ -77,12 +78,14 @@ is
7778
else
7879
Handle_Request :
7980
declare
81+
use type RFLX.RFLX_Types.Length;
8082
Opt_Payload_Length : constant RFLX_Types.Length :=
8183
RFLX_Types.To_Length
8284
(RFLX.CoAP.CoAP_Message.Field_Size
8385
(Context, RFLX.CoAP.CoAP_Message.F_Options_And_Payload));
8486
Opt_Payload_Buffer : RFLX_Types.Bytes
8587
(1 .. RFLX.RFLX_Types.Index'Base (Opt_Payload_Length));
88+
Encoded_Length : RFLX.RFLX_Types.Length;
8689
begin
8790
RFLX.CoAP.CoAP_Message.Get_Options_And_Payload
8891
(Context, Opt_Payload_Buffer);
@@ -121,9 +124,15 @@ is
121124
Status => State.Current_Status,
122125
Encoded_Data =>
123126
RFLX_Result.Options_And_Payload_Options_And_Payload,
124-
Encoded_Length =>
125-
RFLX.CoAP.Length_16
126-
(RFLX_Result.Options_And_Payload_Length));
127+
Encoded_Length => Encoded_Length);
128+
129+
if Encoded_Length > RFLX.RFLX_Types.Length (RFLX.CoAP.Length_16'Last) then
130+
State.Current_Status := CoAP_SPARK.Capacity_Error;
131+
RFLX_Result.Options_And_Payload_Length := 0;
132+
else
133+
RFLX_Result.Options_And_Payload_Length :=
134+
RFLX.CoAP.Length_16 (Encoded_Length);
135+
end if;
127136

128137
RFLX_Result.Success_Code := RFLX.CoAP.Success_Response'Last;
129138
RFLX_Result.Client_Error_Code :=
@@ -187,6 +196,7 @@ is
187196
RFLX_Result : out RFLX.CoAP_Server.Options_And_Payload_Data.Structure)
188197
is
189198
use type CoAP_SPARK.Status_Type;
199+
use type RFLX.RFLX_Types.Length;
190200

191201
Status_Image : constant String :=
192202
CoAP_SPARK.Status_Type'Image (State.Current_Status);
@@ -195,7 +205,7 @@ is
195205
Context : RFLX.CoAP.CoAP_Message.Context;
196206

197207
Response_Content : CoAP_SPARK.Messages.Content;
198-
208+
Encoded_Length : RFLX.RFLX_Types.Length;
199209
begin
200210
RFLX.CoAP.CoAP_Message.Initialize
201211
(Ctx => Context,
@@ -220,8 +230,15 @@ is
220230
(Options_And_Payload => Response_Content,
221231
Status => State.Current_Status,
222232
Encoded_Data => RFLX_Result.Options_And_Payload,
223-
Encoded_Length => RFLX.CoAP.Length_16
224-
(RFLX_Result.Length));
233+
Encoded_Length => Encoded_Length);
234+
235+
if Encoded_Length > RFLX.RFLX_Types.Length (RFLX.CoAP.Length_16'Last) then
236+
State.Current_Status := CoAP_SPARK.Capacity_Error;
237+
RFLX_Result.Length := 0;
238+
else
239+
RFLX_Result.Length :=
240+
RFLX.CoAP.Length_16 (Encoded_Length);
241+
end if;
225242

226243
CoAP_SPARK.Messages.Finalize (Response_Content);
227244
pragma Assert (CoAP_SPARK.Messages.Is_Empty (Response_Content));

0 commit comments

Comments
 (0)