Skip to content

Commit

Permalink
Use Pre aspect for some internal procedures in JSON.Types
Browse files Browse the repository at this point in the history
  • Loading branch information
onox committed Jul 28, 2024
1 parent 23d77eb commit db5b3c7
Show file tree
Hide file tree
Showing 2 changed files with 31 additions and 38 deletions.
64 changes: 28 additions & 36 deletions json/src/json-types.adb
Original file line number Diff line number Diff line change
Expand Up @@ -263,22 +263,18 @@ package body JSON.Types is

procedure Append (Object : in out JSON_Value; Value : JSON_Value) is
begin
if Object.Kind = Array_Kind then
declare
Length : constant Natural
:= Natural (Object.Allocator.Array_Levels (Object.Depth).Length);
begin
-- Assert that Object is the last array in a particular level
-- so that its elements form a continuous array
pragma Assert (Length = Object.Offset + Object.Length);
end;

Object.Allocator.Array_Levels (Object.Depth).Append
(Array_Value'(Kind => Value.Kind, Value => Value));
Object.Length := Object.Length + 1;
else
raise Invalid_Type_Error with "Value not an array";
end if;
declare
Length : constant Natural
:= Natural (Object.Allocator.Array_Levels (Object.Depth).Length);
begin
-- Assert that Object is the last array in a particular level
-- so that its elements form a continuous array
pragma Assert (Length = Object.Offset + Object.Length);
end;

Object.Allocator.Array_Levels (Object.Depth).Append
(Array_Value'(Kind => Value.Kind, Value => Value));
Object.Length := Object.Length + 1;
end Append;

procedure Insert
Expand All @@ -287,27 +283,23 @@ package body JSON.Types is
Value : JSON_Value;
Check_Duplicate_Keys : Boolean) is
begin
if Object.Kind = Object_Kind then
if Check_Duplicate_Keys and then Object.Contains (Key.Value) then
raise Constraint_Error with "JSON object already has key '" & Key.Value & "'";
end if;

declare
Length : constant Natural
:= Natural (Object.Allocator.Object_Levels (Object.Depth).Length);
begin
-- Assert that Object is the last object in a particular level
-- so that its key-value pairs form a continuous array
pragma Assert (Length = Object.Offset + Object.Length);
end;
pragma Assert (Key.Kind = String_Kind);

Object.Allocator.Object_Levels (Object.Depth).Append
(Key_Value_Pair'(Kind => Value.Kind, Key => Key, Element => Value));
Object.Length := Object.Length + 1;
else
raise Invalid_Type_Error with "Value not an object";
if Check_Duplicate_Keys and then Object.Contains (Key.Value) then
raise Constraint_Error with "JSON object already has key '" & Key.Value & "'";
end if;

declare
Length : constant Natural
:= Natural (Object.Allocator.Object_Levels (Object.Depth).Length);
begin
-- Assert that Object is the last object in a particular level
-- so that its key-value pairs form a continuous array
pragma Assert (Length = Object.Offset + Object.Length);
end;
pragma Assert (Key.Kind = String_Kind);

Object.Allocator.Object_Levels (Object.Depth).Append
(Key_Value_Pair'(Kind => Value.Kind, Key => Key, Element => Value));
Object.Length := Object.Length + 1;
end Insert;

-----------------------------------------------------------------------------
Expand Down
5 changes: 3 additions & 2 deletions json/src/json-types.ads
Original file line number Diff line number Diff line change
Expand Up @@ -92,15 +92,16 @@ package JSON.Types is

-----------------------------------------------------------------------------

procedure Append (Object : in out JSON_Value; Value : JSON_Value);
procedure Append (Object : in out JSON_Value; Value : JSON_Value)
with Pre => Object.Kind = Array_Kind;
-- Internal procedure

procedure Insert
(Object : in out JSON_Value;
Key : JSON_Value;
Value : JSON_Value;
Check_Duplicate_Keys : Boolean)
with Pre => Key.Kind = String_Kind;
with Pre => Object.Kind = Object_Kind and Key.Kind = String_Kind;
-- Internal procedure

-----------------------------------------------------------------------------
Expand Down

0 comments on commit db5b3c7

Please sign in to comment.