procedure Clear (Container : in out List);
- procedure Assign (Target : in out List; Source : List);
+ procedure Assign (Target : in out List; Source : List)
+ with Pre => Target.Capacity >= Length (Source);
function Copy (Source : List; Capacity : Count_Type := 0) return List;
- function Element (Container : List; Position : Cursor) return Element_Type;
+ function Element (Container : List; Position : Cursor) return Element_Type
+ with Pre => Has_Element (Container, Position);
procedure Replace_Element
(Container : in out List;
Position : Cursor;
- New_Item : Element_Type);
+ New_Item : Element_Type)
+ with Pre => Has_Element (Container, Position);
- procedure Move (Target : in out List; Source : in out List);
+ procedure Move (Target : in out List; Source : in out List)
+ with Pre => Target.Capacity >= Length (Source);
procedure Insert
(Container : in out List;
Before : Cursor;
New_Item : Element_Type;
- Count : Count_Type := 1);
+ Count : Count_Type := 1)
+ with Pre => Length (Container) + Count <= Container.Capacity and then
+ (Has_Element (Container, Before) or else Before = No_Element);
procedure Insert
(Container : in out List;
Before : Cursor;
New_Item : Element_Type;
Position : out Cursor;
- Count : Count_Type := 1);
+ Count : Count_Type := 1)
+ with Pre => Length (Container) + Count <= Container.Capacity and then
+ (Has_Element (Container, Before) or else Before = No_Element);
procedure Insert
(Container : in out List;
Before : Cursor;
Position : out Cursor;
- Count : Count_Type := 1);
+ Count : Count_Type := 1)
+ with Pre => Length (Container) + Count <= Container.Capacity and then
+ (Has_Element (Container, Before) or else Before = No_Element);
procedure Prepend
(Container : in out List;
New_Item : Element_Type;
- Count : Count_Type := 1);
+ Count : Count_Type := 1)
+ with Pre => Length (Container) + Count <= Container.Capacity;
procedure Append
(Container : in out List;
New_Item : Element_Type;
- Count : Count_Type := 1);
+ Count : Count_Type := 1)
+ with Pre => Length (Container) + Count <= Container.Capacity;
procedure Delete
(Container : in out List;
Position : in out Cursor;
- Count : Count_Type := 1);
+ Count : Count_Type := 1)
+ with Pre => Has_Element (Container, Position);
procedure Delete_First
(Container : in out List;
- Count : Count_Type := 1);
+ Count : Count_Type := 1)
+ with Pre => not Is_Empty (Container);
procedure Delete_Last
(Container : in out List;
- Count : Count_Type := 1);
+ Count : Count_Type := 1)
+ with Pre => not Is_Empty (Container);
procedure Reverse_Elements (Container : in out List);
procedure Swap
(Container : in out List;
- I, J : Cursor);
+ I, J : Cursor)
+ with Pre => Has_Element (Container, I) and then Has_Element (Container, J);
procedure Swap_Links
(Container : in out List;
- I, J : Cursor);
+ I, J : Cursor)
+ with Pre => Has_Element (Container, I) and then Has_Element (Container, J);
procedure Splice
(Target : in out List;
Before : Cursor;
- Source : in out List);
+ Source : in out List)
+ with Pre => Length (Source) + Length (Target) <= Target.Capacity and then
+ (Has_Element (Target, Before) or else Before = No_Element);
procedure Splice
(Target : in out List;
Before : Cursor;
Source : in out List;
- Position : in out Cursor);
+ Position : in out Cursor)
+ with Pre => Length (Source) + Length (Target) <= Target.Capacity and then
+ (Has_Element (Target, Before) or else Before = No_Element) and then
+ Has_Element (Source, Position);
procedure Splice
(Container : in out List;
Before : Cursor;
- Position : Cursor);
+ Position : Cursor)
+ with Pre => 2 * Length (Container) <= Container.Capacity and then
+ (Has_Element (Container, Before) or else Before = No_Element) and then
+ Has_Element (Container, Position);
function First (Container : List) return Cursor;
- function First_Element (Container : List) return Element_Type;
+ function First_Element (Container : List) return Element_Type
+ with Pre => not Is_Empty (Container);
function Last (Container : List) return Cursor;
- function Last_Element (Container : List) return Element_Type;
+ function Last_Element (Container : List) return Element_Type
+ with Pre => not Is_Empty (Container);
- function Next (Container : List; Position : Cursor) return Cursor;
+ function Next (Container : List; Position : Cursor) return Cursor
+ with Pre => Has_Element (Container, Position) or else Position = No_Element;
- procedure Next (Container : List; Position : in out Cursor);
+ procedure Next (Container : List; Position : in out Cursor)
+ with Pre => Has_Element (Container, Position) or else Position = No_Element;
- function Previous (Container : List; Position : Cursor) return Cursor;
+ function Previous (Container : List; Position : Cursor) return Cursor
+ with Pre => Has_Element (Container, Position) or else Position = No_Element;
- procedure Previous (Container : List; Position : in out Cursor);
+ procedure Previous (Container : List; Position : in out Cursor)
+ with Pre => Has_Element (Container, Position) or else Position = No_Element;
function Find
(Container : List;
Item : Element_Type;
- Position : Cursor := No_Element) return Cursor;
+ Position : Cursor := No_Element) return Cursor
+ with Pre => Has_Element (Container, Position) or else Position = No_Element;
function Reverse_Find
(Container : List;
Item : Element_Type;
- Position : Cursor := No_Element) return Cursor;
+ Position : Cursor := No_Element) return Cursor
+ with Pre => Has_Element (Container, Position) or else Position = No_Element;
function Contains
(Container : List;
-- they are structurally equal (function "=" returns True) and that they
-- have the same set of cursors.
- function Left (Container : List; Position : Cursor) return List;
- function Right (Container : List; Position : Cursor) return List;
+ function Left (Container : List; Position : Cursor) return List
+ with Pre => Has_Element (Container, Position) or else Position = No_Element;
+ function Right (Container : List; Position : Cursor) return List
+ with Pre => Has_Element (Container, Position) or else Position = No_Element;
-- Left returns a container containing all elements preceding Position
-- (excluded) in Container. Right returns a container containing all
-- elements following Position (included) in Container. These two new
-- 6. In addition, the comment must be properly indented if comment
-- indentation checking is active (Style_Check_Indentation non-zero).
-- Either the start column must be a multiple of this indentation,
- -- or the indentation must match that of the next non-blank line.
+ -- or the indentation must match that of the next non-blank line,
+ -- or must match the indentation of the immediately preciding line
+ -- if it is non-blank.
procedure Check_Comment is
S : Source_Ptr;
-- matches that of the next non-blank line in the source, then True is
-- returned, otherwise False.
+ function Same_Column_As_Previous_Line return Boolean;
+ -- Called for a full line comment. If the previous line is blank, then
+ -- returns False. Otherwise, if the indentation of this comment matches
+ -- that of the previous line in the source, then True is returned,
+ -- otherwise False.
+
--------------------
-- Is_Box_Comment --
--------------------
return Get_Column_Number (Scan_Ptr) = Get_Column_Number (P);
end Same_Column_As_Next_Non_Blank_Line;
+ ----------------------------------
+ -- Same_Column_As_Previous_Line --
+ ----------------------------------
+
+ function Same_Column_As_Previous_Line return Boolean is
+ S, P : Source_Ptr;
+
+ begin
+ -- Point S to start of this line, and P to start of previous line
+
+ S := Line_Start (Scan_Ptr);
+ P := S;
+ Backup_Line (P);
+
+ -- Step P to first non-blank character on line
+
+ loop
+ -- If we get back to start of current line, then the previous line
+ -- was blank, and we always return False in that situation.
+
+ if P = S then
+ return False;
+ end if;
+
+ exit when Source (P) /= ' ' and then Source (P) /= ASCII.HT;
+ P := P + 1;
+ end loop;
+
+ -- Compare columns
+
+ return Get_Column_Number (Scan_Ptr) = Get_Column_Number (P);
+ end Same_Column_As_Previous_Line;
+
-- Start of processing for Check_Comment
begin
if Style_Check_Indentation /= 0 then
if Start_Column rem Style_Check_Indentation /= 0 then
- if not Same_Column_As_Next_Non_Blank_Line then
+ if not Same_Column_As_Next_Non_Blank_Line
+ and then not Same_Column_As_Previous_Line
+ then
Error_Msg_S -- CODEFIX
("(style) bad column");
end if;