-------------------------------------------------------------------------------
-- (C) Altran Praxis Limited
-------------------------------------------------------------------------------
--
-- The SPARK toolset is free software; you can redistribute it and/or modify it
-- under terms of the GNU General Public License as published by the Free
-- Software Foundation; either version 3, or (at your option) any later
-- version. The SPARK toolset is distributed in the hope that it will be
-- useful, but WITHOUT ANY WARRANTY; without even the implied warranty of
-- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General
-- Public License for more details. You should have received a copy of the GNU
-- General Public License distributed with the SPARK toolset; see file
-- COPYING3. If not, go to http://www.gnu.org/licenses for a complete copy of
-- the license.
--
--=============================================================================

with Ada.Characters.Handling;
with Ada.Characters.Latin_1;
with Ada.Command_Line;
with CommandLineData;
with FileSystem;
with ScreenEcho;
with SPARK_IO;
with ExaminerConstants;

use type CommandLineData.Concurrency_Profiles;
use type CommandLineData.Flow_Analysis_Options;
use type CommandLineData.Info_Flow_Policies;
use type CommandLineData.Language_Profiles;
use type SPARK_IO.File_Status;

package body CommandLineHandler is

   type Command_Line_Errors is (ES_Index,
                                ES_IndexName,
                                ES_NoIndex,
                                ES_SourceExt,
                                ES_ListingExt,
                                ES_NoReport,
                                ES_Report,
                                ES_ReportName,
                                ES_Rules,
                                ES_RuleUnknown,
                                ES_NoEcho,
                                ES_NoDict,
                                ES_NoDuration,
                                ES_Dict,
                                ES_InvalidOption,
                                ES_ListingFile,
                                ES_NoComma,
                                ES_Source,
                                EW_Overlap,
                                EW_Listing,
                                EW_Index,
                                EW_Report,
                                EW_Source,
                                ES_VCGandFDL,
                                ES_DPCandFDL,
                                ES_VCGRepeated,
                                ES_DPCRepeated,
                                ES_NoMorePFS,
                                ES_NoMoreRTC,
                                ES_NoMoreEXP,
                                ES_NoMoreReal,
                                ES_ErrorExplanations,
                                EW_Too_Many,
                                ES_Warning,
                                ES_WarningName,
                                ES_NoWarning,
                                EW_Warning,
                                ES_OutputDir,
                                ES_OutputDirRepeated,
                                ES_OutputDirNotFound,
                                SOFstyle,
                                ES_Syntax,
                                ES_Statistics,
                                ES_NoStatistics,
                                ES_FDLoption,
                                ES_InformationFlow,
                                ES_TargetData,
                                ES_TargetDataName,
                                ES_NoTargetData,
                                EW_Target,
                                ES_ConfigFile,
                                ES_ConfigFileName,
                                ES_NoConfigFile,
                                EW_Config,
                                ES_LanguageRepeated,
                                ES_LanguageProfile,
                                ES_NoRavenscarInSPARK83,
                                ES_NoSPARKLibInSPARK83,
                                ES_NoAutoFlowInSPARK83,
                                ES_Debug,
                                ES_Casing,
                                ES_Anno,
                                ES_Html,
                                ES_PlainOutput,
                                ES_Brief,
                                ES_BriefOption,
                                ES_XML,
                                ES_XMLandHTML,
                                ES_XMLnorep,
                                ES_HTMLnorep,
                                ES_DataFlowAndInfoFlowPolicy,
                                ES_OriginalFlowErrors,
                                ES_ErrorExplanationOption,
                                ES_JustificationRepeated,
                                ES_JustificationOption,
                                ES_Profile,
                                ES_ProfileOption,
                                ES_NoListings,
                                ES_DataAndConfig,
                                ES_Makefile,
                                ES_Makefile_Repeated);

   function Is_White_Space (Space_Char : Character) return Boolean is
   begin
      return (Space_Char = ' ') or else (Space_Char = Ada.Characters.Latin_1.HT) or else (Space_Char = Ada.Characters.Latin_1.CR);
   end Is_White_Space;

   procedure Output_Error (E : in Command_Line_Errors)
   --# global in     CommandLineData.Content;
   --#        in out SPARK_IO.File_Sys;
   --# derives SPARK_IO.File_Sys from *,
   --#                                CommandLineData.Content,
   --#                                E;
   is
      Check_Msg : constant String := " (check default switch file)";
   begin
      case E is
         when ES_Index =>
            ScreenEcho.Put_String ("Index option already specified or NoIndex option already specified" & Check_Msg);

         when ES_IndexName =>
            ScreenEcho.Put_String ("Index option incorrectly specified");

         when ES_Source =>
            ScreenEcho.Put_String ("Source file incorrectly specified");

         when ES_NoIndex =>
            ScreenEcho.Put_String ("NoIndex option already specified or Index option already specified" & Check_Msg);

         when ES_SourceExt =>
            ScreenEcho.Put_String ("Source extension option already specified or incorrectly specified");

         when ES_ListingExt =>
            ScreenEcho.Put_String ("Listing extension option already specified or incorrectly specified");

         when ES_NoReport =>
            ScreenEcho.Put_String ("NoReport option already specified, or contradictory report option found" & Check_Msg);

         when ES_Report =>
            ScreenEcho.Put_String ("Report option already specified or NoReport option already specified" & Check_Msg);

         when ES_ReportName =>
            ScreenEcho.Put_String ("Report option incorrectly specified");

         when ES_Rules =>
            ScreenEcho.Put_String ("Rules option may not appear more than once" & Check_Msg);

         when ES_RuleUnknown =>
            ScreenEcho.Put_String
              ("Rules option not recognised: legal values are: " &
                 CommandLineData.Option_Rules_None &
                 ", " &
                 CommandLineData.Option_Rules_Lazy &
                 ", " &
                 CommandLineData.Option_Rules_Keen &
                 ", " &
                 CommandLineData.Option_Rules_All);

         when ES_NoEcho =>
            ScreenEcho.Put_String ("NoEcho option may not appear more than once" & Check_Msg);

         when ES_NoDict =>
            ScreenEcho.Put_String
              ("NoDictionary option already specified or Dictionary option already specified (check default switch file)");

         when ES_NoDuration =>
            ScreenEcho.Put_String ("NoDuration option may not appear more than once" & Check_Msg);

         when ES_Dict =>
            ScreenEcho.Put_String
              ("Dictionary option already specified or NoDictionary option already specified (check default switch file)");

         when ES_InvalidOption =>
            ScreenEcho.Put_String ("Invalid command line option:");

         when ES_ListingFile =>
            ScreenEcho.Put_String ("Listing file option incorrect");

         when ES_NoComma =>
            ScreenEcho.Put_String ("Comma missing in line");

         when ES_VCGandFDL =>
            ScreenEcho.Put_String
              ("-" &
                 CommandLineData.Option_Vcg &
                 " and -" &
                 CommandLineData.Option_Fdl_Identifiers &
                 "=" &
                 CommandLineData.Option_Fdl_Identifiers_Accept &
                 " cannot be used together" &
                 Check_Msg);

         when ES_DPCandFDL =>
            ScreenEcho.Put_String
              ("-" &
                 CommandLineData.Option_Dpc &
                 " and -" &
                 CommandLineData.Option_Fdl_Identifiers &
                 "=" &
                 CommandLineData.Option_Fdl_Identifiers_Accept &
                 " cannot be used together" &
                 Check_Msg);

         when ES_VCGRepeated =>
            ScreenEcho.Put_String ("-" & CommandLineData.Option_Vcg & " already specified" & Check_Msg);

         when ES_DPCRepeated =>
            ScreenEcho.Put_String ("-" & CommandLineData.Option_Dpc & " already specified" & Check_Msg);

         when ES_NoMorePFS =>
            ScreenEcho.Put_String ("PFS option is no longer supported" & Check_Msg);

         when ES_NoMoreRTC =>
            ScreenEcho.Put_String
              ("RTC option is no longer supported. Please use -" & CommandLineData.Option_Vcg & " instead " & Check_Msg);

         when ES_NoMoreEXP =>
            ScreenEcho.Put_String
              ("EXP option is no longer supported. Please use -" & CommandLineData.Option_Vcg & " instead " & Check_Msg);

         when ES_NoMoreReal =>
            ScreenEcho.Put_String
              ("Real_RTCs option is no longer supported. Please use -" & CommandLineData.Option_Vcg & " instead " & Check_Msg);

         when ES_ErrorExplanations =>
            ScreenEcho.Put_String ("Error_Explanations option may not appear more than once" & Check_Msg);

         when EW_Overlap =>
            ScreenEcho.Put_String ("File argument is repeated:");

         when EW_Listing =>
            ScreenEcho.Put_String ("Cannot create file");

         when EW_Index =>
            ScreenEcho.Put_String ("Cannot open index file");

         when EW_Report =>
            ScreenEcho.Put_String ("Cannot create file");

         when EW_Source =>
            ScreenEcho.Put_String ("Cannot open source file");

         when EW_Too_Many =>
            ScreenEcho.Put_String ("Too many source files on command line");

         when ES_WarningName =>
            ScreenEcho.Put_String ("Warning option incorrectly specified");

         when ES_Warning =>
            ScreenEcho.Put_String ("Warning option already specified" & Check_Msg);

         when ES_NoWarning =>
            ScreenEcho.Put_String ("NoWarning option already specifies" & Check_Msg);

         when EW_Warning =>
            ScreenEcho.Put_String ("Cannot open warning control file");

         when ES_OutputDir =>
            ScreenEcho.Put_String ("Output directory option must have exactly one argument");

         when ES_OutputDirRepeated =>
            ScreenEcho.Put_String ("Output directory option already specified" & Check_Msg);

         when ES_OutputDirNotFound =>
            ScreenEcho.Put_String ("Cannot find or write to output directory");

         when SOFstyle =>
            ScreenEcho.Put_String ("-concat is no longer supported. -tree is now the default and only option" & Check_Msg);

         when ES_Syntax =>
            ScreenEcho.Put_String ("Syntax check option may not appear more than once" & Check_Msg);

         when ES_Statistics =>
            ScreenEcho.Put_String ("Statistics option already specified, or NoStatistics option already specified" & Check_Msg);

         when ES_NoStatistics =>
            ScreenEcho.Put_String ("NoStatistics option already specified, or Statistics option already specified" & Check_Msg);

         when ES_FDLoption =>
            ScreenEcho.Put_String ("FDL identifier option already specified, or contradictory option found" & Check_Msg);

         when ES_InformationFlow =>
            ScreenEcho.Put_String ("Flow analysis option already specified or incorrectly specified:");

         when ES_TargetDataName =>
            ScreenEcho.Put_String ("Target compiler data option incorrectly specified");

         when ES_TargetData =>
            ScreenEcho.Put_String
              ("Target compiler data option already specified or NoTarget compiler data option already specified" & Check_Msg);

         when ES_NoTargetData =>
            ScreenEcho.Put_String
              ("NoTarget compiler data option already specified or Target compiler data option already specified" & Check_Msg);

         when EW_Target =>
            ScreenEcho.Put_String ("Cannot open target data file");

         when ES_ConfigFileName =>
            ScreenEcho.Put_String ("Configuration file incorrectly specified");

         when ES_ConfigFile =>
            ScreenEcho.Put_String ("Configuration file already specified or NoConfiguration file already specified" & Check_Msg);

         when ES_NoConfigFile =>
            ScreenEcho.Put_String ("NoConfiguration file already specified or Configuration file already specified" & Check_Msg);

         when EW_Config =>
            ScreenEcho.Put_String ("Cannot open configuration file");

         when ES_LanguageRepeated =>
            ScreenEcho.Put_String ("Language profile already specified" & Check_Msg);

         when ES_LanguageProfile =>
            ScreenEcho.Put_String
              ("Language profile incorrect. Value must be one of " &
                 CommandLineData.Option_Language_83 &
                 ", " &
                 CommandLineData.Option_Language_95 &
                 ", ");
            if CommandLineData.Content.Distribution_Is_Pro then
               ScreenEcho.Put_String (CommandLineData.Option_Language_2005 & ", or " & CommandLineData.Option_Language_KCG);
            else
               ScreenEcho.Put_String ("or " & CommandLineData.Option_Language_2005);
            end if;

         when ES_NoRavenscarInSPARK83 =>
            ScreenEcho.Put_String ("Ravenscar concurrency profile is not permitted in SPARK83");

         when ES_NoSPARKLibInSPARK83 =>
            ScreenEcho.Put_String ("-sparklib is not permitted in SPARK83");

         when ES_NoAutoFlowInSPARK83 =>
            ScreenEcho.Put_String ("-flow=auto is not permitted in SPARK83");

         when ES_Debug =>
            ScreenEcho.Put_String ("Debugging option already specified, or incorrectly specified" & Check_Msg);

         when ES_Casing =>
            ScreenEcho.Put_String ("Casing option already specified, or incorrectly specified" & Check_Msg);

         when ES_Anno =>
            ScreenEcho.Put_String ("Annotation character option may not appear more than once" & Check_Msg);

         when ES_Html =>
            ScreenEcho.Put_String ("HTML option may not appear more than once" & Check_Msg);

         when ES_PlainOutput =>
            ScreenEcho.Put_String ("Plain output option may not appear more than once" & Check_Msg);

         when ES_Brief =>
            ScreenEcho.Put_String ("Brief output option may not appear more than once" & Check_Msg);

         when ES_BriefOption =>
            ScreenEcho.Put_String
              ("Brief option value must be one of: " &
                 CommandLineData.Option_Brief_No_Path &
                 " or " &
                 CommandLineData.Option_Brief_Full_Path);

         when ES_OriginalFlowErrors =>
            ScreenEcho.Put_String ("OriginalFlowErrors output option may not appear more than once" & Check_Msg);

         when ES_Profile =>
            ScreenEcho.Put_String ("Analysis profile option may not appear more than once" & Check_Msg);

         when ES_ProfileOption =>
            ScreenEcho.Put_String ("Analysis profile option incorrect:");

         when ES_ErrorExplanationOption =>
            ScreenEcho.Put_String ("Error_Explanation option incorrect:");

         when ES_DataAndConfig =>
            ScreenEcho.Put_String ("Target data and config file cannot be specified together" & Check_Msg);

         when ES_XML =>
            ScreenEcho.Put_String ("XML option may not appear more than once" & Check_Msg);

         when ES_XMLandHTML =>
            ScreenEcho.Put_String ("XML and HTML cannot be specified together" & Check_Msg);

         when ES_HTMLnorep =>
            ScreenEcho.Put_String ("HTML and noreport cannot be specified together" & Check_Msg);

         when ES_XMLnorep =>
            ScreenEcho.Put_String ("XML and noreport cannot be specified together" & Check_Msg);

         when ES_NoListings =>
            ScreenEcho.Put_String ("No listings option may not be specified more than once" & Check_Msg);

         when ES_DataFlowAndInfoFlowPolicy =>
            ScreenEcho.Put_String
              ("Information flow policy requires " &
                 CommandLineData.Option_Flow_Analysis &
                 "=" &
                 CommandLineData.Option_Flow_Analysis_Information);

         when ES_JustificationRepeated =>
            ScreenEcho.Put_String ("Justification_Option may not appear more than once" & Check_Msg);

         when ES_JustificationOption =>
            ScreenEcho.Put_String
              ("Justification_Option value must be one of: " &
                 CommandLineData.Option_Justification_Option_Ignore &
                 ", " &
                 CommandLineData.Option_Justification_Option_Full &
                 ", or " &
                 CommandLineData.Option_Justification_Option_Brief);

         when ES_Makefile =>
            ScreenEcho.Put_String
              ("The -" &
                 CommandLineData.Option_Makefile_Mode &
                 " option requires -" &
                 CommandLineData.Option_Brief &
                 " and is incompatible with -" &
                 CommandLineData.Option_No_Echo &
                 ".");

         when ES_Makefile_Repeated =>
            ScreenEcho.Put_String
              ("The -" & CommandLineData.Option_Makefile_Mode & " option may not be specified more than once" & Check_Msg);

      end case;
   end Output_Error;

   procedure Possible_Error (E : in Command_Line_Errors)
   --# global in     CommandLineData.Content;
   --#        in out SPARK_IO.File_Sys;
   --# derives SPARK_IO.File_Sys from *,
   --#                                CommandLineData.Content,
   --#                                E;
   is
   begin
      if not CommandLineData.Content.Valid then
         Output_Error (E => E);
         ScreenEcho.New_Line (1);
      end if;
   end Possible_Error;

   procedure Possible_Error2 (E : in Command_Line_Errors;
                              F : in E_Strings.T)
   --# global in     CommandLineData.Content;
   --#        in out SPARK_IO.File_Sys;
   --# derives SPARK_IO.File_Sys from *,
   --#                                CommandLineData.Content,
   --#                                E,
   --#                                F;
   is
   begin
      if not CommandLineData.Content.Valid then
         Output_Error (E => E);
         ScreenEcho.Put_Char (' ');
         if CommandLineData.Content.Plain_Output then
            ScreenEcho.Put_ExaminerLine (E_Strings.Lower_Case (E_Str => F));
         else
            ScreenEcho.Put_ExaminerLine (F);
         end if;
      end if;
   end Possible_Error2;

   procedure Read_Default_Switches (Default_Switches_Found : out Boolean;
                                    Cmd_Line               : out E_Strings.T)
   --# global in out SPARK_IO.File_Sys;
   --# derives Cmd_Line,
   --#         Default_Switches_Found,
   --#         SPARK_IO.File_Sys      from SPARK_IO.File_Sys;
   -- post (not Default_Switches_Found and Cmd_Line_Ptr = 1) or
   --      (Default_Switches_Found and Cmd_Line_Ptr = Cmd_Line'Last + 2);
   is

      Switch_File_Found : Boolean;
      Switch_File       : SPARK_IO.File_Type;
      Cmd_Line_Local    : E_Strings.T;
      Unused            : SPARK_IO.File_Status;

      procedure Open_File (Switch_File_Found : out Boolean;
                           Switch_File       : out SPARK_IO.File_Type)
      --# global in out SPARK_IO.File_Sys;
      --# derives SPARK_IO.File_Sys,
      --#         Switch_File,
      --#         Switch_File_Found from SPARK_IO.File_Sys;
      is
         Switch_File_Local : SPARK_IO.File_Type := SPARK_IO.Null_File;
         File_Status       : SPARK_IO.File_Status;
      begin
         SPARK_IO.Open (Switch_File_Local, SPARK_IO.In_File, 8, "spark.sw", "", File_Status);
         if File_Status = SPARK_IO.Ok then
            Switch_File_Found := True;
            Switch_File       := Switch_File_Local;
         else
            Switch_File_Found := False;
            Switch_File       := SPARK_IO.Null_File;
         end if;
      end Open_File;

      procedure Process_Switch_File (Switch_File : in     SPARK_IO.File_Type;
                                     Cmd_Line    : in out E_Strings.T)
      --# global in out SPARK_IO.File_Sys;
      --# derives Cmd_Line,
      --#         SPARK_IO.File_Sys from *,
      --#                                SPARK_IO.File_Sys,
      --#                                Switch_File;
      is
         Current_Line     : E_Strings.T;
         In_Quoted_String : Boolean;

         function Strip_Leading_Spaces (S : E_Strings.T) return E_Strings.T is
            Ptr : E_Strings.Positions := 1;
         begin
            loop
               exit when Ptr > E_Strings.Get_Length (E_Str => S);
               exit when not Is_White_Space (Space_Char => E_Strings.Get_Element (E_Str => S,
                                                                                  Pos   => Ptr));
               Ptr := Ptr + 1;
            end loop;
            return E_Strings.Section (E_Str     => S,
                                      Start_Pos => Ptr,
                                      Length    => (E_Strings.Get_Length (E_Str => S) - Ptr) + 1);
         end Strip_Leading_Spaces;

         function Strip_Comments (S : E_Strings.T) return E_Strings.T is
            Res : E_Strings.T;
         begin
            if E_Strings.Get_Element (E_Str => S,
                                      Pos   => 1) = '-'
              and then E_Strings.Get_Element (E_Str => S,
                                              Pos   => 2) = '-' then
               Res := E_Strings.Empty_String;
            else
               Res := S;
            end if;
            return Res;
         end Strip_Comments;

         function Line_Is_Empty (S : E_Strings.T) return Boolean is
         begin
            return E_Strings.Get_Length (E_Str => S) = 0;
         end Line_Is_Empty;

      begin -- Process_Switch_File
         In_Quoted_String := False;

         loop -- look for non-empty lines in switch file and process them
            exit when SPARK_IO.End_Of_File (Switch_File);

            E_Strings.Get_Line (File  => Switch_File,
                                E_Str => Current_Line);
            Current_Line := Strip_Comments (S => Strip_Leading_Spaces (S => Current_Line));
            if not Line_Is_Empty (S => Current_Line) then
               for I in E_Strings.Lengths range 1 .. E_Strings.Get_Length (E_Str => Current_Line) loop
                  -- premature exit if comment found in line
                  exit when E_Strings.Get_Element (E_Str => Current_Line,
                                                   Pos   => I) = '-'
                    and then I < E_Strings.Get_Length (E_Str => Current_Line)
                    and then E_Strings.Get_Element (E_Str => Current_Line,
                                                    Pos   => I + 1) = '-';

                  if E_Strings.Get_Element (E_Str => Current_Line,
                                            Pos   => I) = Ada.Characters.Latin_1.Quotation then
                     In_Quoted_String := not In_Quoted_String;
                  end if;

                  if In_Quoted_String then
                     --  In a quoted string, we leave the character
                     --  alone.
                     E_Strings.Append_Char (E_Str => Cmd_Line,
                                            Ch    => E_Strings.Get_Element (E_Str => Current_Line,
                                                                            Pos   => I));
                  elsif Is_White_Space (Space_Char => E_Strings.Get_Element (E_Str => Current_Line,
                                                                             Pos   => I)) then
                     --  Not in a quoted string, so whitespace gets
                     --  replaced by the host's preferred argument
                     --  separator character
                     E_Strings.Append_Char (E_Str => Cmd_Line,
                                            Ch    => FileSystem.Argument_Separator);
                  else
                     --  We just append the character as is in any
                     --  other case.
                     E_Strings.Append_Char (E_Str => Cmd_Line,
                                            Ch    => E_Strings.Get_Element (E_Str => Current_Line,
                                                                            Pos   => I));
                  end if;
               end loop;
               E_Strings.Append_Char (E_Str => Cmd_Line,
                                      Ch    => FileSystem.Argument_Separator);
            end if;
         end loop;
      end Process_Switch_File;

   begin -- Read_Default_Switches
      Cmd_Line_Local := E_Strings.Empty_String;

      Open_File (Switch_File_Found => Switch_File_Found,
                 Switch_File       => Switch_File);
      if Switch_File_Found then
         Process_Switch_File (Switch_File => Switch_File,
                              Cmd_Line    => Cmd_Line_Local);
         --# accept F, 10, Unused, "Returned status not used here" &
         --#        F, 10, Switch_File, "Returned handle not used here";
         SPARK_IO.Close (Switch_File, Unused); --expect flow error
      end if;

      Default_Switches_Found := Switch_File_Found;
      Cmd_Line               := Cmd_Line_Local;
      --# accept F, 33, Unused, "Unused not referenced here";
   end Read_Default_Switches;

   procedure Skip_Spaces (Command_String : in out Command_Strings) is
   begin
      loop
         exit when Command_String.Current_Position > E_Strings.Get_Length (E_Str => Command_String.Contents);

         exit when not ((E_Strings.Get_Element (E_Str => Command_String.Contents,
                                                Pos   => Command_String.Current_Position) = ' ')
                        or else (E_Strings.Get_Element (E_Str => Command_String.Contents,
                                                        Pos   => Command_String.Current_Position) =
                                   FileSystem.Argument_Separator));

         Command_String.Current_Position := Command_String.Current_Position + 1;
      end loop;
   end Skip_Spaces;

   procedure Read_The_String (Command_String : in out Command_Strings;
                              Next_Symbol    : in out Symbols) is
      Current_Ch : Character;
   begin
      Next_Symbol.The_String := E_Strings.Empty_String;
      Current_Ch             := E_Strings.Get_Element (E_Str => Command_String.Contents,
                                                       Pos   => Command_String.Current_Position);

      loop
         -- Skip over quotes, but allow spaces in the string
         if Current_Ch /= Ada.Characters.Latin_1.Quotation then
            E_Strings.Append_Char (E_Str => Next_Symbol.The_String,
                                   Ch    => Current_Ch);
         end if;

         Command_String.Current_Position := Command_String.Current_Position + 1;
         Current_Ch                      :=
           E_Strings.Get_Element (E_Str => Command_String.Contents,
                                  Pos   => Command_String.Current_Position);

         exit when Command_String.Current_Position > E_Strings.Get_Length (E_Str => Command_String.Contents)
           or else FileSystem.Is_An_Argument_Terminator (Ch => Current_Ch);
      end loop;
   end Read_The_String;

   procedure Get_Next_Symbol (Command_String : in out Command_Strings;
                              Next_Symbol    :    out Symbols)
   --# derives Command_String,
   --#         Next_Symbol    from Command_String;
   is
      Local_Next_Symbol : Symbols;
   begin
      -- This procedure is intended to return Next_Symbol; however, if the
      -- symbol is not a string then the string field is not set.  Although
      -- it is not used in these circumstances its lack of definition
      -- causes so many flow errors its is better to use an aggregate to
      -- initialize Next_Symbol here, and then assign the final value
      -- to Next_Symbol (for compatibility with the Ada83 "out parameter" rule
      Local_Next_Symbol := Symbols'(Typ        => S_Empty,
                                    The_String => E_Strings.Empty_String);

      Skip_Spaces (Command_String => Command_String);

      if Command_String.Current_Position <= E_Strings.Get_Length (E_Str => Command_String.Contents) then
         case E_Strings.Get_Element (E_Str => Command_String.Contents,
                                     Pos   => Command_String.Current_Position) is
            when '=' =>
               Local_Next_Symbol.Typ           := S_Equal;
               Command_String.Current_Position := Command_String.Current_Position + 1;
            when ',' =>
               --this condition is invariant for any particular system, we are actually
               --simulating conditional compilation for different target platforms.
               --Intended behaviour is correct despite flow error that will result.
               --# accept F, 22, "Stable expression here OK";
               if FileSystem.Use_Unix_Command_Line then
                  Local_Next_Symbol.Typ := S_String;
                  Read_The_String (Command_String => Command_String,
                                   Next_Symbol    => Local_Next_Symbol);
               else -- Windows
                  Local_Next_Symbol.Typ           := S_Comma;
                  Command_String.Current_Position := Command_String.Current_Position + 1;
               end if;
               --# end accept;
            when '-' =>
               --  On all platforms '-' is the switch character.
               Local_Next_Symbol.Typ           := S_Switch_Character;
               Command_String.Current_Position := Command_String.Current_Position + 1;
            when others =>
               Local_Next_Symbol.Typ := S_String;
               Read_The_String (Command_String => Command_String,
                                Next_Symbol    => Local_Next_Symbol);
         end case;
      else
         -- Exceeded maximum command line length
         Local_Next_Symbol.Typ := S_Empty;
      end if;

      Next_Symbol := Local_Next_Symbol;
   end Get_Next_Symbol;

   procedure Read_Option
     (Opt_Name       :    out E_Strings.T;
      Opt_Name_OK    :    out Boolean;
      Opt_Val        :    out E_Strings.T;
      Opt_Val_OK     :    out Boolean;
      Command_String : in out Command_Strings;
      Next_Symbol    :    out Symbols)
   --# derives Command_String,
   --#         Next_Symbol,
   --#         Opt_Name,
   --#         Opt_Name_OK,
   --#         Opt_Val,
   --#         Opt_Val_OK     from Command_String;
   --  pre  Next_Symbol.Typ = SSlash;
   is
      Opt_Name_OK_Local : Boolean;
      Local_Next_Symbol : Symbols;
   begin
      Opt_Val := E_Strings.Empty_String;
      Get_Next_Symbol (Command_String => Command_String,
                       Next_Symbol    => Local_Next_Symbol);
      Opt_Name_OK_Local := Local_Next_Symbol.Typ = S_String;
      Opt_Name          := Local_Next_Symbol.The_String;
      Get_Next_Symbol (Command_String => Command_String,
                       Next_Symbol    => Local_Next_Symbol);
      if Opt_Name_OK_Local and Local_Next_Symbol.Typ = S_Equal then
         Get_Next_Symbol (Command_String => Command_String,
                          Next_Symbol    => Local_Next_Symbol);
         Opt_Val_OK := Local_Next_Symbol.Typ = S_String;
         Opt_Val    := Local_Next_Symbol.The_String;
         Get_Next_Symbol (Command_String => Command_String,
                          Next_Symbol    => Local_Next_Symbol);
      else
         Opt_Val_OK := False;
      end if;
      Opt_Name_OK := Opt_Name_OK_Local;
      Next_Symbol := Local_Next_Symbol;
   end Read_Option;

   function Check_Option_Name (Opt_Name : E_Strings.T;
                               Str      : String) return Boolean is
      OK : Boolean := False;
   begin
      if E_Strings.Get_Length (E_Str => Opt_Name) <= Str'Length then
         for I in E_Strings.Lengths range 1 .. E_Strings.Get_Length (E_Str => Opt_Name) loop
            OK := Ada.Characters.Handling.To_Lower (E_Strings.Get_Element (E_Str => Opt_Name,
                                                                           Pos   => I)) =
              Ada.Characters.Handling.To_Lower (Str (I));
            exit when not OK;
         end loop;
      end if;
      return OK;
   end Check_Option_Name;

   procedure Parse_Command_Options (Command_String : in out Command_Strings;
                                    Next_Symbol    : in out Symbols)
   --# global in out CommandLineData.Content;
   --#        in out SPARK_IO.File_Sys;
   --# derives CommandLineData.Content,
   --#         Command_String,
   --#         Next_Symbol,
   --#         SPARK_IO.File_Sys       from *,
   --#                                      CommandLineData.Content,
   --#                                      Command_String,
   --#                                      Next_Symbol;
   is
      IndexFound               : Boolean := False;
      OutputDirectoryFound     : Boolean := False;
      WarningFound             : Boolean := False;
      NoWarningFound           : Boolean := False;
      SourceFound              : Boolean := False;
      ListingFound             : Boolean := False;
      OutputFound              : Boolean := False;
      ReportFound              : Boolean := False;
      ErrorExplanationsFound   : Boolean := False;
      JustificationOptionFound : Boolean := False;
      RulesFound               : Boolean := False;
      VCGFound                 : Boolean := False;
      DPCFound                 : Boolean := False;
      NoReportOptionFound      : Boolean := False;
      SyntaxCheckFound         : Boolean := False;
      StatisticsFound          : Boolean := False;
      FDLreserveOptionFound    : Boolean := False;
      FDLignoreOptionFound     : Boolean := False;
      FlowOptionFound          : Boolean := False;
      TargetDataFound          : Boolean := False;
      ConfigFileFound          : Boolean := False;
      LanguageProfileFound     : Boolean := False;
      DebugEnabledFound        : Boolean := False;
      CasingEnabledFound       : Boolean := False;
      AnnotationCharacterFound : Boolean := False;
      HTMLFound                : Boolean := False;
      PlainOutputFound         : Boolean := False;
      NoDurationFound          : Boolean := False;
      BriefFound               : Boolean := False;
      XMLFound                 : Boolean := False;
      OriginalFlowErrorsFound  : Boolean := False;
      NoListingsFound          : Boolean := False;
      DictFound                : Boolean := False;
      ConcurrencyProfileFound  : Boolean := False;
      Makefile_Found           : Boolean := False;

      Opt_Name, Opt_Val       : E_Strings.T;
      Opt_Name_OK, Opt_Val_OK : Boolean;

      procedure Process_A
      --# global in     FlowOptionFound;
      --#        in     Opt_Name;
      --#        in     Opt_Val;
      --#        in out AnnotationCharacterFound;
      --#        in out CommandLineData.Content;
      --#        in out LanguageProfileFound;
      --#        in out SPARK_IO.File_Sys;
      --# derives AnnotationCharacterFound,
      --#         LanguageProfileFound     from *,
      --#                                       Opt_Name &
      --#         CommandLineData.Content  from *,
      --#                                       AnnotationCharacterFound,
      --#                                       FlowOptionFound,
      --#                                       LanguageProfileFound,
      --#                                       Opt_Name,
      --#                                       Opt_Val &
      --#         SPARK_IO.File_Sys        from *,
      --#                                       AnnotationCharacterFound,
      --#                                       CommandLineData.Content,
      --#                                       LanguageProfileFound,
      --#                                       Opt_Name;
      is
      begin
         --# accept W, 169, CommandLineData.Content.Valid, "Direct updates OK here" &
         --#        W, 169, CommandLineData.Content.Flow_Option, "Direct updates OK here" &
         --#        W, 169, CommandLineData.Content.Language_Profile, "Direct updates OK here" &
         --#        W, 169, CommandLineData.Content.Anno_Char, "Direct updates OK here";
         case Ada.Characters.Handling.To_Lower (E_Strings.Get_Element (E_Str => Opt_Name,
                                                                       Pos   => 2)) is
            when 'd' => -- 2nd letter
               if Check_Option_Name (Opt_Name => Opt_Name,
                                     Str      => "ada83") then
                  CommandLineData.Content.Valid := not LanguageProfileFound;
                  Possible_Error (E => ES_LanguageRepeated);
                  LanguageProfileFound                     := True;
                  CommandLineData.Content.Language_Profile := CommandLineData.SPARK83;
                  if not FlowOptionFound then
                     CommandLineData.Content.Flow_Option := CommandLineData.Info_Flow;
                  end if;
               else
                  CommandLineData.Content.Valid := False;
                  Possible_Error2 (E => ES_InvalidOption,
                                   F => Opt_Name);
               end if;

            when 'n' => -- 2nd letter
               if Check_Option_Name (Opt_Name => Opt_Name,
                                     Str      => CommandLineData.Option_Annotation_Character) then
                  CommandLineData.Content.Valid := not AnnotationCharacterFound;
                  Possible_Error (E => ES_Anno);
                  AnnotationCharacterFound          := True;
                  CommandLineData.Content.Anno_Char := E_Strings.Get_Element (E_Str => Opt_Val,
                                                                              Pos   => 1);
               else
                  CommandLineData.Content.Valid := False;
                  Possible_Error2 (E => ES_InvalidOption,
                                   F => Opt_Name);
               end if;

            when others =>
               CommandLineData.Content.Valid := False;
               Possible_Error2 (E => ES_InvalidOption,
                                F => Opt_Name);
         end case;
         --# end accept;
      end Process_A;

      procedure Process_B
      --# global in     Opt_Name;
      --#        in     Opt_Val;
      --#        in     Opt_Val_OK;
      --#        in out BriefFound;
      --#        in out CommandLineData.Content;
      --#        in out SPARK_IO.File_Sys;
      --# derives BriefFound              from *,
      --#                                      Opt_Name &
      --#         CommandLineData.Content,
      --#         SPARK_IO.File_Sys       from *,
      --#                                      BriefFound,
      --#                                      CommandLineData.Content,
      --#                                      Opt_Name,
      --#                                      Opt_Val,
      --#                                      Opt_Val_OK;
      is
      begin
         --# accept W, 169, CommandLineData.Content.Valid, "Direct updates OK here" &
         --#        W, 169, CommandLineData.Content.Brief_Option, "Direct updates OK here" &
         --#        W, 169, CommandLineData.Content.Brief, "Direct updates OK here";
         if Check_Option_Name (Opt_Name => Opt_Name,
                               Str      => CommandLineData.Option_Brief) then
            CommandLineData.Content.Valid := not BriefFound;
            Possible_Error (E => ES_Brief);
            BriefFound                    := True;
            CommandLineData.Content.Brief := True;

            if Opt_Val_OK then
               -- Overriding the default the default brief option: "-brief=something"
               case Ada.Characters.Handling.To_Lower (E_Strings.Get_Element (E_Str => Opt_Val,
                                                                             Pos   => 1)) is
                  when 'n' => -- 1st letter of option
                     if Check_Option_Name (Opt_Name => Opt_Val,
                                           Str      => CommandLineData.Option_Brief_No_Path) then
                        CommandLineData.Content.Brief_Option := CommandLineData.No_Path;
                     else -- error involving 'nopath'
                        CommandLineData.Content.Valid := False;
                        Possible_Error (E => ES_BriefOption);
                     end if;
                  when 'f' => -- 1st letter of option
                     if Check_Option_Name (Opt_Name => Opt_Val,
                                           Str      => CommandLineData.Option_Brief_Full_Path) then
                        CommandLineData.Content.Brief_Option := CommandLineData.Full_Path;
                     else               -- error involving 'fullpath'
                        CommandLineData.Content.Valid := False;
                        Possible_Error (E => ES_BriefOption);
                     end if;
                  when others =>
                     CommandLineData.Content.Valid := False;
                     Possible_Error (E => ES_BriefOption);
               end case;
            end if;
         else
            CommandLineData.Content.Valid := False;
            Possible_Error2 (E => ES_InvalidOption,
                             F => Opt_Name);
         end if;
         --# end accept;
      end Process_B;

      procedure Process_C
      --# global in     Opt_Name;
      --#        in     Opt_Val;
      --#        in     Opt_Val_OK;
      --#        in     TargetDataFound;
      --#        in out CasingEnabledFound;
      --#        in out CommandLineData.Content;
      --#        in out ConfigFileFound;
      --#        in out SPARK_IO.File_Sys;
      --# derives CasingEnabledFound      from *,
      --#                                      Opt_Name &
      --#         CommandLineData.Content,
      --#         SPARK_IO.File_Sys       from *,
      --#                                      CasingEnabledFound,
      --#                                      CommandLineData.Content,
      --#                                      ConfigFileFound,
      --#                                      Opt_Name,
      --#                                      Opt_Val,
      --#                                      Opt_Val_OK,
      --#                                      TargetDataFound &
      --#         ConfigFileFound         from *,
      --#                                      Opt_Name,
      --#                                      Opt_Val_OK,
      --#                                      TargetDataFound;
      is
         File_Name : E_Strings.T;
      begin
         --# accept W, 169, CommandLineData.Content.Valid, "Direct updates OK here" &
         --#        W, 169, CommandLineData.Content.Casing_Standard, "Direct updates OK here" &
         --#        W, 169, CommandLineData.Content.Casing_Identifier, "Direct updates OK here" &
         --#        W, 169, CommandLineData.Content.Target_Config, "Direct updates OK here" &
         --#        W, 169, CommandLineData.Content.Target_Config_File, "Direct updates OK here";

         case Ada.Characters.Handling.To_Lower (E_Strings.Get_Element (E_Str => Opt_Name,
                                                                       Pos   => 2)) is
            when 'a' =>
               if Check_Option_Name (Opt_Name => Opt_Name,
                                     Str      => CommandLineData.Option_Casing) then
                  CommandLineData.Content.Valid := not CasingEnabledFound;
                  Possible_Error (E => ES_Casing);
                  CasingEnabledFound := True;
                  if Opt_Val_OK then
                     for I in Integer range 1 .. E_Strings.Get_Length (E_Str => Opt_Val) loop
                        case Ada.Characters.Handling.To_Lower (E_Strings.Get_Element (E_Str => Opt_Val,
                                                                                      Pos   => I)) is
                           when CommandLineData.Option_Casing_Standard =>
                              if CommandLineData.Content.Casing_Standard then
                                 CommandLineData.Content.Valid := False;
                                 Possible_Error (E => ES_Casing);
                              else
                                 CommandLineData.Content.Casing_Standard := True;
                              end if;
                           when CommandLineData.Option_Casing_Identifier =>
                              if CommandLineData.Content.Casing_Identifier then
                                 CommandLineData.Content.Valid := False;
                                 Possible_Error (E => ES_Casing);
                              else
                                 CommandLineData.Content.Casing_Identifier := True;
                              end if;
                           when others =>
                              CommandLineData.Content.Valid := False;
                              Possible_Error (E => ES_Casing);
                        end case;
                     end loop;
                  else
                     CommandLineData.Content.Casing_Standard   := True;
                     CommandLineData.Content.Casing_Identifier := True;
                  end if;
               else
                  CommandLineData.Content.Valid := False;
                  Possible_Error2 (E => ES_InvalidOption,
                                   F => Opt_Name);
               end if;
            when 'o' => -- 2nd letter
               case Ada.Characters.Handling.To_Lower (E_Strings.Get_Element (E_Str => Opt_Name,
                                                                             Pos   => 3)) is -- 3rd letter
                  when 'n' =>
                     case Ada.Characters.Handling.To_Lower (E_Strings.Get_Element (E_Str => Opt_Name,
                                                                                   Pos   => 4)) is -- 4th letter
                        when 'f' =>
                           if Check_Option_Name (Opt_Name => Opt_Name,
                                                 Str      => CommandLineData.Option_Config_File) then
                              if TargetDataFound then
                                 CommandLineData.Content.Valid := False;
                                 Possible_Error (E => ES_DataAndConfig);
                              else
                                 CommandLineData.Content.Valid := Opt_Val_OK;
                                 Possible_Error (E => ES_ConfigFileName);
                                 if Opt_Val_OK then
                                    CommandLineData.Content.Valid := not ConfigFileFound;
                                    Possible_Error (E => ES_ConfigFile);
                                 end if;
                                 if CommandLineData.Content.Valid then
                                    ConfigFileFound                       := True;
                                    CommandLineData.Content.Target_Config := True;
                                    File_Name                             := Opt_Val;
                                    FileSystem.Check_Extension
                                      (Fn  => File_Name,
                                       Ext => E_Strings.Copy_String (Str => CommandLineData.Default_Config_Extension));
                                    CommandLineData.Content.Target_Config_File := File_Name;
                                 end if;
                              end if;
                           else
                              CommandLineData.Content.Valid := False;
                              Possible_Error2 (E => ES_InvalidOption,
                                               F => Opt_Name);
                           end if;
                        when 'c' => -- 4th letter

                           -- -concat is removed in release 8.1.1 and above, but
                           -- recognize it here and warn the user.
                           if Check_Option_Name (Opt_Name => Opt_Name,
                                                 Str      => "concatenate") then
                              CommandLineData.Content.Valid := False;
                              Possible_Error (E => SOFstyle);
                           else
                              CommandLineData.Content.Valid := False;
                              Possible_Error2 (E => ES_InvalidOption,
                                               F => Opt_Name);
                           end if;
                        when others =>
                           CommandLineData.Content.Valid := False;
                           Possible_Error2 (E => ES_InvalidOption,
                                            F => Opt_Name);
                     end case;
                  when others =>
                     CommandLineData.Content.Valid := False;
                     Possible_Error2 (E => ES_InvalidOption,
                                      F => Opt_Name);
               end case;
            when others =>
               CommandLineData.Content.Valid := False;
               Possible_Error2 (E => ES_InvalidOption,
                                F => Opt_Name);
         end case;
         --# end accept;
      end Process_C;

      procedure Process_D
      --# global in     FDLignoreOptionFound;
      --#        in     Opt_Name;
      --#        in     Opt_Val;
      --#        in     Opt_Val_OK;
      --#        in out CommandLineData.Content;
      --#        in out DebugEnabledFound;
      --#        in out DictFound;
      --#        in out DPCFound;
      --#        in out SPARK_IO.File_Sys;
      --# derives CommandLineData.Content,
      --#         SPARK_IO.File_Sys       from *,
      --#                                      CommandLineData.Content,
      --#                                      DebugEnabledFound,
      --#                                      DictFound,
      --#                                      DPCFound,
      --#                                      FDLignoreOptionFound,
      --#                                      Opt_Name,
      --#                                      Opt_Val,
      --#                                      Opt_Val_OK &
      --#         DebugEnabledFound,
      --#         DPCFound                from *,
      --#                                      Opt_Name &
      --#         DictFound               from *,
      --#                                      Opt_Name,
      --#                                      Opt_Val_OK;
      is
         Default_Dict_Extension : constant String := "dic";
         File_Name              : E_Strings.T;
      begin
         --# accept W, 169, CommandLineData.Content.DPC, "Direct updates OK here" &
         --#        W, 169, CommandLineData.Content.Valid, "Direct updates OK here" &
         --#        W, 169, CommandLineData.Content.Write_Dict, "Direct updates OK here" &
         --#        W, 169, CommandLineData.Content.Dict_File_Name, "Direct updates OK here" &
         --#        W, 169, CommandLineData.Content.Debug.Enabled, "Direct updates OK here" &
         --#        W, 169, CommandLineData.Content.Debug.HTML, "Direct updates OK here" &
         --#        W, 169, CommandLineData.Content.Debug.Expressions, "Direct updates OK here" &
         --#        W, 169, CommandLineData.Content.Debug.Lookup_Trace, "Direct updates OK here" &
         --#        W, 169, CommandLineData.Content.Debug.File_Names, "Direct updates OK here" &
         --#        W, 169, CommandLineData.Content.Debug.Units, "Direct updates OK here" &
         --#        W, 169, CommandLineData.Content.Debug.Invariants, "Direct updates OK here" &
         --#        W, 169, CommandLineData.Content.Debug.Components, "Direct updates OK here" &
         --#        W, 169, CommandLineData.Content.Debug.Rho, "Direct updates OK here" &
         --#        W, 169, CommandLineData.Content.Debug.FDL_Ranking, "Direct updates OK here" &
         --#        W, 169, CommandLineData.Content.Debug.VCG, "Direct updates OK here" &
         --#        W, 169, CommandLineData.Content.Debug.Parser, "Direct updates OK here" &
         --#        W, 169, CommandLineData.Content.Debug.SLI, "Direct updates OK here" &
         --#        W, 169, CommandLineData.Content.Debug.VCG_All, "Direct updates OK here" &
         --#        W, 169, CommandLineData.Content.Debug.Extra_Stats, "Direct updates OK here" &
         --#        W, 169, CommandLineData.Content.Debug.DAG, "Direct updates OK here";
         case Ada.Characters.Handling.To_Lower (E_Strings.Get_Element (E_Str => Opt_Name,
                                                                       Pos   => 2)) is
            when 'i' => -- 2nd letter
               if Check_Option_Name (Opt_Name => Opt_Name,
                                     Str      => CommandLineData.Option_Dictionary_File) then
                  CommandLineData.Content.Valid := Opt_Val_OK and then not DictFound;
                  Possible_Error (E => ES_Dict);

                  if CommandLineData.Content.Valid then
                     DictFound                          := True;
                     CommandLineData.Content.Write_Dict := True;
                     File_Name                          := Opt_Val;
                     FileSystem.Check_Extension (Fn  => File_Name,
                                                 Ext => E_Strings.Copy_String (Str => Default_Dict_Extension));
                     CommandLineData.Content.Dict_File_Name := File_Name;
                  end if;
               else
                  CommandLineData.Content.Valid := False;
                  Possible_Error2 (E => ES_InvalidOption,
                                   F => Opt_Name);
               end if;
            when 'e' => -- 2nd letter
               if Check_Option_Name (Opt_Name => Opt_Name,
                                     Str      => CommandLineData.Option_Debug) then
                  CommandLineData.Content.Valid := not DebugEnabledFound;
                  Possible_Error (E => ES_Debug);
                  DebugEnabledFound                     := True;
                  CommandLineData.Content.Debug.Enabled := True;

                  -- The -debug switch may also have a parameter which
                  -- is a list of character-codes for specific debug
                  -- options.  These are:
                  --   c  -  Print component manager state
                  --   e  -  Debug Expresion syntax and tree walking
                  --   f  -  Trace filename storage/open/create
                  --   h  -  Debug HTML generation
                  --   i  -  Print default loop invariants
                  --   k  -  Trace ranking and printing of FDL declarations
                  --   l  -  Trace dictionary Look-Ups
                  --   p  -  Print parser state on detection of syntax Error
                  --   r  -  Print computed Rho relation for each subprogram
                  --   u  -  Trace required units and index lookups
                  --   v  -  Print VCG State and BPG after DAG.BuildGraph
                  --   V  -  As v, but also print BPG during iteration of Graph.GenVCs
                  --   x  -  Print cross-reference debug
                  --   d  -  Print FDL DAG following BuildExpnDAG or
                  --         BuildAnnotationExpnDAG
                  -- These codes may be combined, so
                  --   -debug=eh and
                  --   -debug=he are both allowed and are equivalent

                  if Opt_Val_OK then
                     for I in Integer range 1 .. E_Strings.Get_Length (E_Str => Opt_Val) loop
                        case E_Strings.Get_Element (E_Str => Opt_Val,
                                                    Pos   => I) is
                           when CommandLineData.Option_Debug_C =>
                              CommandLineData.Content.Debug.Components := True;
                           when CommandLineData.Option_Debug_D =>
                              CommandLineData.Content.Debug.DAG := True;
                           when CommandLineData.Option_Debug_E =>
                              CommandLineData.Content.Debug.Expressions := True;
                           when CommandLineData.Option_Debug_F =>
                              CommandLineData.Content.Debug.File_Names := True;
                           when CommandLineData.Option_Debug_H =>
                              CommandLineData.Content.Debug.HTML := True;
                           when CommandLineData.Option_Debug_I =>
                              CommandLineData.Content.Debug.Invariants := True;
                           when CommandLineData.Option_Debug_K =>
                              CommandLineData.Content.Debug.FDL_Ranking := True;
                           when CommandLineData.Option_Debug_L =>
                              CommandLineData.Content.Debug.Lookup_Trace := True;
                           when CommandLineData.Option_Debug_P =>
                              CommandLineData.Content.Debug.Parser := True;
                           when CommandLineData.Option_Debug_R =>
                              CommandLineData.Content.Debug.Rho := True;
                           when CommandLineData.Option_Debug_T =>
                              CommandLineData.Content.Debug.Extra_Stats := True;
                           when CommandLineData.Option_Debug_U =>
                              CommandLineData.Content.Debug.Units := True;
                           when CommandLineData.Option_Debug_V =>
                              CommandLineData.Content.Debug.VCG := True;
                           when CommandLineData.Option_Debug_V_Upper =>
                              CommandLineData.Content.Debug.VCG     := True;
                              CommandLineData.Content.Debug.VCG_All := True;
                           when CommandLineData.Option_Debug_X =>
                              CommandLineData.Content.Debug.SLI := True;
                           when others =>
                              CommandLineData.Content.Valid := False;
                        end case;
                     end loop;
                     Possible_Error (E => ES_Debug);
                  end if;
               else
                  CommandLineData.Content.Valid := False;
                  Possible_Error2 (E => ES_InvalidOption,
                                   F => Opt_Name);
               end if;

            when 'p' => -- 2nd letter
               if Check_Option_Name (Opt_Name => Opt_Name,
                                     Str      => CommandLineData.Option_Dpc) then
                  if DPCFound then
                     CommandLineData.Content.Valid := False;
                     Possible_Error (E => ES_DPCRepeated);
                  elsif FDLignoreOptionFound and then E_Strings.Is_Empty (E_Str => CommandLineData.Content.FDL_Mangle) then
                     CommandLineData.Content.Valid := False;
                     Possible_Error (E => ES_DPCandFDL);
                  else
                     CommandLineData.Content.Valid := True;
                  end if;
                  DPCFound                    := True;
                  CommandLineData.Content.DPC := True;
               else
                  CommandLineData.Content.Valid := False;
                  Possible_Error2 (E => ES_InvalidOption,
                                   F => Opt_Name);
               end if;

            when others =>
               -- starts "d" but not valid
               CommandLineData.Content.Valid := False;
               Possible_Error2 (E => ES_InvalidOption,
                                F => Opt_Name);
         end case;
         --# end accept;
      end Process_D;

      procedure Process_E
      --# global in     Opt_Name;
      --#        in     Opt_Val;
      --#        in out CommandLineData.Content;
      --#        in out ErrorExplanationsFound;
      --#        in out SPARK_IO.File_Sys;
      --# derives CommandLineData.Content,
      --#         SPARK_IO.File_Sys       from *,
      --#                                      CommandLineData.Content,
      --#                                      ErrorExplanationsFound,
      --#                                      Opt_Name,
      --#                                      Opt_Val &
      --#         ErrorExplanationsFound  from *,
      --#                                      Opt_Name;
      is
      begin
         --# accept W, 169, CommandLineData.Content.Valid, "Direct updates OK here" &
         --#        W, 169, CommandLineData.Content.Error_Explanation, "Direct updates OK here";
         case Ada.Characters.Handling.To_Lower (E_Strings.Get_Element (E_Str => Opt_Name,
                                                                       Pos   => 2)) is
            when 'x' => -- 2nd letter
               CommandLineData.Content.Valid := False;
               if Check_Option_Name (Opt_Name => Opt_Name,
                                     Str      => "exp_checks") then
                  Possible_Error (E => ES_NoMoreEXP);
               else
                  Possible_Error2 (E => ES_InvalidOption,
                                   F => Opt_Name);
               end if;
            when 'r' => -- 2nd letter
               if Check_Option_Name (Opt_Name => Opt_Name,
                                     Str      => CommandLineData.Option_Error_Explanations) then
                  CommandLineData.Content.Valid := not ErrorExplanationsFound;
                  Possible_Error (E => ES_ErrorExplanations);
                  if CommandLineData.Content.Valid then
                     ErrorExplanationsFound := True;
                     -- now check argument - must be one of Off, FirstOccurrence, EveryOccurrence
                     case Ada.Characters.Handling.To_Lower (E_Strings.Get_Element (E_Str => Opt_Val,
                                                                                   Pos   => 1)) is
                        when 'o' => -- 1st letter of option
                           if Check_Option_Name (Opt_Name => Opt_Val,
                                                 Str      => CommandLineData.Option_Error_Explanations_Off) then
                              CommandLineData.Content.Error_Explanation := CommandLineData.Off;
                           else -- error involving 'off'
                              CommandLineData.Content.Valid := False;
                              Possible_Error2 (E => ES_ErrorExplanationOption,
                                               F => Opt_Val);
                           end if;
                        when 'f' => -- 1st letter of option
                           if Check_Option_Name
                             (Opt_Name => Opt_Val,
                              Str      => CommandLineData.Option_Error_Explanations_First_Occurrence) then
                              CommandLineData.Content.Error_Explanation := CommandLineData.First_Occurrence;
                           else -- error involving 'first_occurrence'
                              CommandLineData.Content.Valid := False;
                              Possible_Error2 (E => ES_ErrorExplanationOption,
                                               F => Opt_Val);
                           end if;
                        when 'e' => -- 1st letter of option
                           if Check_Option_Name
                             (Opt_Name => Opt_Val,
                              Str      => CommandLineData.Option_Error_Explanations_Every_Occurrence) then
                              CommandLineData.Content.Error_Explanation := CommandLineData.Every_Occurrence;
                           else -- error involving 'every_occurrence'
                              CommandLineData.Content.Valid := False;
                              Possible_Error2 (E => ES_ErrorExplanationOption,
                                               F => Opt_Val);
                           end if;
                        when others =>
                           CommandLineData.Content.Valid := False;
                           Possible_Error2 (E => ES_ErrorExplanationOption,
                                            F => Opt_Val);
                     end case;
                  end if;
               else
                  CommandLineData.Content.Valid := False;
                  Possible_Error2 (E => ES_InvalidOption,
                                   F => Opt_Name);
               end if;
            when others =>
               CommandLineData.Content.Valid := False;
               Possible_Error2 (E => ES_InvalidOption,
                                F => Opt_Name);
         end case;
         --# end accept;
      end Process_E;

      procedure Process_F
      --# global in     DPCFound;
      --#        in     Opt_Name;
      --#        in     Opt_Val;
      --#        in     Opt_Val_OK;
      --#        in     VCGFound;
      --#        in out CommandLineData.Content;
      --#        in out FDLignoreOptionFound;
      --#        in out FDLreserveOptionFound;
      --#        in out FlowOptionFound;
      --#        in out SPARK_IO.File_Sys;
      --# derives CommandLineData.Content,
      --#         SPARK_IO.File_Sys       from *,
      --#                                      CommandLineData.Content,
      --#                                      DPCFound,
      --#                                      FDLignoreOptionFound,
      --#                                      FDLreserveOptionFound,
      --#                                      FlowOptionFound,
      --#                                      Opt_Name,
      --#                                      Opt_Val,
      --#                                      Opt_Val_OK,
      --#                                      VCGFound &
      --#         FDLignoreOptionFound,
      --#         FDLreserveOptionFound   from *,
      --#                                      Opt_Name,
      --#                                      Opt_Val,
      --#                                      Opt_Val_OK &
      --#         FlowOptionFound         from *,
      --#                                      Opt_Name,
      --#                                      Opt_Val_OK;
      is
      begin
         --# accept W, 169, CommandLineData.Content.Valid, "Direct updates OK here" &
         --#        W, 169, CommandLineData.Content.FDL_Mangle, "Direct updates OK here" &
         --#        W, 169, CommandLineData.Content.FDL_Reserved, "Direct updates OK here" &
         --#        W, 169, CommandLineData.Content.Flow_Option, "Direct updates OK here";
         case Ada.Characters.Handling.To_Lower (E_Strings.Get_Element (E_Str => Opt_Name,
                                                                       Pos   => 2)) is
            when 'd' => -- 2nd letter
               if Check_Option_Name (Opt_Name => Opt_Name,
                                     Str      => CommandLineData.Option_Fdl_Identifiers) then
                  CommandLineData.Content.Valid := not (FDLreserveOptionFound or FDLignoreOptionFound);
                  Possible_Error (E => ES_FDLoption);
                  if Opt_Val_OK then
                     if Check_Option_Name (Opt_Name => Opt_Val,
                                           Str      => CommandLineData.Option_Fdl_Identifiers_Accept) then
                        CommandLineData.Content.FDL_Reserved := False;
                        CommandLineData.Content.Valid        := not VCGFound and not DPCFound;
                        if VCGFound then
                           Possible_Error (E => ES_VCGandFDL);
                        elsif DPCFound then
                           Possible_Error (E => ES_DPCandFDL);
                        end if;
                        FDLignoreOptionFound := True;
                     else
                        if Check_Option_Name (Opt_Name => Opt_Val,
                                              Str      => CommandLineData.Option_Fdl_Identifiers_Reject) then
                           CommandLineData.Content.FDL_Reserved := True;
                           FDLreserveOptionFound                := True;
                        else
                           CommandLineData.Content.FDL_Reserved := False; -- Will not reject fdl reserved words
                           CommandLineData.Content.FDL_Mangle   := Opt_Val;  -- But will mangle them
                           FDLignoreOptionFound                 := True;
                        end if;
                     end if;
                  else
                     ScreenEcho.Put_Line ("Warning: The -fdl option is now deprecated. Please use -fdl=reject");
                     FDLreserveOptionFound                := True;
                     CommandLineData.Content.FDL_Reserved := True;
                  end if;
               else
                  CommandLineData.Content.Valid := False;
                  Possible_Error2 (E => ES_InvalidOption,
                                   F => Opt_Name);
               end if;

            when 'l' => -- 2nd letter
               if Check_Option_Name (Opt_Name => Opt_Name,
                                     Str      => CommandLineData.Option_Flow_Analysis) then
                  CommandLineData.Content.Valid := Opt_Val_OK and then not FlowOptionFound;
                  Possible_Error2 (E => ES_InformationFlow,
                                   F => Opt_Val);
                  if CommandLineData.Content.Valid then --go on to check selection
                     FlowOptionFound := True;
                     case Ada.Characters.Handling.To_Lower (E_Strings.Get_Element (E_Str => Opt_Val,
                                                                                   Pos   => 1)) is
                        when 'a' =>
                           if Check_Option_Name (Opt_Name => Opt_Val,
                                                 Str      => CommandLineData.Option_Flow_Analysis_Auto) then
                              CommandLineData.Content.Flow_Option := CommandLineData.Auto_Flow;
                           else -- something which begins with 'a' other than auto
                              CommandLineData.Content.Valid := False;
                              Possible_Error2 (E => ES_InformationFlow,
                                               F => Opt_Val);
                           end if;

                        when 'i' =>
                           if Check_Option_Name
                             (Opt_Name => Opt_Val,
                              Str      => CommandLineData.Option_Flow_Analysis_Information) then
                              CommandLineData.Content.Flow_Option := CommandLineData.Info_Flow;
                           else -- something which begins with 'i' other than information
                              CommandLineData.Content.Valid := False;
                              Possible_Error2 (E => ES_InformationFlow,
                                               F => Opt_Val);
                           end if;

                        when 'd' =>
                           if Check_Option_Name (Opt_Name => Opt_Val,
                                                 Str      => CommandLineData.Option_Flow_Analysis_Data) then
                              -- Here we have a potentially valid selection flow_analysis=data.
                              -- This is only allowed if information flow integrity checking has
                              -- not been selected
                              if (CommandLineData.Content.Info_Flow_Policy = CommandLineData.None) then
                                 CommandLineData.Content.Flow_Option := CommandLineData.Data_Flow;
                              else
                                 CommandLineData.Content.Valid := False;
                                 Possible_Error (E => ES_DataFlowAndInfoFlowPolicy);
                              end if;
                           else -- something which begins with 'd' other than data
                              CommandLineData.Content.Valid := False;
                              Possible_Error2 (E => ES_InformationFlow,
                                               F => Opt_Val);
                           end if;

                        when others => -- doesn't begin with 'i' or 'd'
                           CommandLineData.Content.Valid := False;
                           Possible_Error2 (E => ES_InformationFlow,
                                            F => Opt_Val);
                     end case;
                  end if;
               else -- begins with 'f' but not fdl... or flow...
                  CommandLineData.Content.Valid := False;
                  Possible_Error2 (E => ES_InvalidOption,
                                   F => Opt_Name);
               end if;

            when others =>
               CommandLineData.Content.Valid := False;
               Possible_Error2 (E => ES_InvalidOption,
                                F => Opt_Name);
         end case;
         --# end accept;
      end Process_F;

      procedure Process_G
      --# global in     Opt_Name;
      --#        in out CommandLineData.Content;
      --#        in out SPARK_IO.File_Sys;
      --# derives CommandLineData.Content,
      --#         SPARK_IO.File_Sys       from *,
      --#                                      CommandLineData.Content,
      --#                                      Opt_Name;
      is
      begin
         --# accept W, 169, CommandLineData.Content.Valid, "Direct updates OK here" &
         --#        W, 169, CommandLineData.Content.Distribution_Is_Pro, "Direct updates OK here" &
         --#        W, 169, CommandLineData.Content.GPL_Switch, "Direct updates OK here";
         if Check_Option_Name (Opt_Name => Opt_Name,
                               Str      => CommandLineData.Option_GPL) then
            CommandLineData.Content.Valid               := True;
            CommandLineData.Content.Distribution_Is_Pro := False;
            CommandLineData.Content.GPL_Switch          := True;
         else
            CommandLineData.Content.Valid := False;
            Possible_Error2 (E => ES_InvalidOption,
                             F => Opt_Name);
         end if;
      end Process_G;

      procedure Process_H
      --# global in     NoReportOptionFound;
      --#        in     Opt_Name;
      --#        in     Opt_Val;
      --#        in     Opt_Val_OK;
      --#        in     XMLFound;
      --#        in out CommandLineData.Content;
      --#        in out HTMLFound;
      --#        in out SPARK_IO.File_Sys;
      --# derives CommandLineData.Content from *,
      --#                                      HTMLFound,
      --#                                      NoReportOptionFound,
      --#                                      Opt_Name,
      --#                                      Opt_Val,
      --#                                      Opt_Val_OK,
      --#                                      XMLFound &
      --#         HTMLFound               from *,
      --#                                      Opt_Name &
      --#         SPARK_IO.File_Sys       from *,
      --#                                      CommandLineData.Content,
      --#                                      HTMLFound,
      --#                                      NoReportOptionFound,
      --#                                      Opt_Name,
      --#                                      XMLFound;
      is
      begin
         --# accept W, 169, CommandLineData.Content.Valid, "Direct updates OK here" &
         --#        W, 169, CommandLineData.Content.HTML, "Direct updates OK here" &
         --#        W, 169, CommandLineData.Content.HTML_Directory, "Direct updates OK here" &
         --#        W, 169, CommandLineData.Content.Plain_Output, "Direct updates OK here" &
         --#        W, 169, CommandLineData.Content.Help_Requested, "Direct updates OK here";
         case Ada.Characters.Handling.To_Lower (E_Strings.Get_Element (E_Str => Opt_Name,
                                                                       Pos   => 2)) is
            when 't' => -- 2nd letter
               if Check_Option_Name (Opt_Name => Opt_Name,
                                     Str      => CommandLineData.Option_Html) then
                  CommandLineData.Content.Valid := not (HTMLFound or else NoReportOptionFound or else XMLFound);

                  if XMLFound then
                     Possible_Error (E => ES_XMLandHTML);
                  elsif NoReportOptionFound then
                     Possible_Error (E => ES_HTMLnorep);
                  else
                     Possible_Error (E => ES_Html);
                  end if;

                  HTMLFound                    := True;
                  CommandLineData.Content.HTML := True;
                  if Opt_Val_OK then
                     CommandLineData.Content.HTML_Directory := Opt_Val;
                  end if;

               else
                  CommandLineData.Content.Valid := False;
                  Possible_Error2 (E => ES_InvalidOption,
                                   F => Opt_Name);
               end if;
            when 'e' => -- 2nd letter
               if Check_Option_Name (Opt_Name => Opt_Name,
                                     Str      => CommandLineData.Option_Help) then
                  -- Examiner Help requested, so abandon all further
                  -- option processing by setting Valid = False.
                  CommandLineData.Content.Valid          := False;
                  CommandLineData.Content.Help_Requested := True;
                  -- Override setting of PlainOutput so Help information
                  -- always appears with Examiner version number and date.
                  CommandLineData.Content.Plain_Output := False;
               else
                  CommandLineData.Content.Valid := False;
                  Possible_Error2 (E => ES_InvalidOption,
                                   F => Opt_Name);
               end if;
            when others =>
               CommandLineData.Content.Valid := False;
               Possible_Error2 (E => ES_InvalidOption,
                                F => Opt_Name);
         end case;
         --# end accept;
      end Process_H;

      procedure Process_I
      --# global in     Opt_Name;
      --#        in     Opt_Val;
      --#        in     Opt_Val_OK;
      --#        in out CommandLineData.Content;
      --#        in out IndexFound;
      --#        in out SPARK_IO.File_Sys;
      --# derives CommandLineData.Content from *,
      --#                                      IndexFound,
      --#                                      Opt_Name,
      --#                                      Opt_Val,
      --#                                      Opt_Val_OK &
      --#         IndexFound              from *,
      --#                                      Opt_Name,
      --#                                      Opt_Val_OK &
      --#         SPARK_IO.File_Sys       from *,
      --#                                      CommandLineData.Content,
      --#                                      IndexFound,
      --#                                      Opt_Name,
      --#                                      Opt_Val_OK;
      is
         File_Name : E_Strings.T;
      begin
         --# accept W, 169, CommandLineData.Content.Valid, "Direct updates OK here" &
         --#        W, 169, CommandLineData.Content.Index, "Direct updates OK here" &
         --#        W, 169, CommandLineData.Content.Index_File_Name, "Direct updates OK here";
         if Check_Option_Name (Opt_Name => Opt_Name,
                               Str      => CommandLineData.Option_Index_File) then
            CommandLineData.Content.Valid := Opt_Val_OK;
            Possible_Error (E => ES_IndexName);
            if Opt_Val_OK then
               CommandLineData.Content.Valid := not IndexFound;
               Possible_Error (E => ES_Index);
            end if;

            if CommandLineData.Content.Valid then
               IndexFound                    := True;
               CommandLineData.Content.Index := True;
               File_Name                     := Opt_Val;

               FileSystem.Check_Extension
                 (Fn  => File_Name,
                  Ext => E_Strings.Copy_String (Str => CommandLineData.Default_Index_Extension));
               CommandLineData.Content.Index_File_Name := File_Name;
            end if;
         else
            CommandLineData.Content.Valid := False;
            Possible_Error2 (E => ES_InvalidOption,
                             F => Opt_Name);
         end if;
         --# end accept;
      end Process_I;

      procedure Process_J
      --# global in     Opt_Name;
      --#        in     Opt_Val;
      --#        in out CommandLineData.Content;
      --#        in out JustificationOptionFound;
      --#        in out SPARK_IO.File_Sys;
      --# derives CommandLineData.Content,
      --#         SPARK_IO.File_Sys        from *,
      --#                                       CommandLineData.Content,
      --#                                       JustificationOptionFound,
      --#                                       Opt_Name,
      --#                                       Opt_Val &
      --#         JustificationOptionFound from *,
      --#                                       Opt_Name;
      is
      begin
         --# accept W, 169, CommandLineData.Content.Valid, "Direct updates OK here" &
         --#        W, 169, CommandLineData.Content.Justification_Option, "Direct updates OK here";
         if Check_Option_Name (Opt_Name => Opt_Name,
                               Str      => CommandLineData.Option_Justification_Option) then
            CommandLineData.Content.Valid := not JustificationOptionFound;
            Possible_Error (E => ES_JustificationRepeated);
            if CommandLineData.Content.Valid then
               JustificationOptionFound := True;
               -- now check argument - must be one of Ignore, Full, or Brief
               case Ada.Characters.Handling.To_Lower (E_Strings.Get_Element (E_Str => Opt_Val,
                                                                             Pos   => 1)) is
                  when 'i' => -- 1st letter of option
                     if Check_Option_Name (Opt_Name => Opt_Val,
                                           Str      => CommandLineData.Option_Justification_Option_Ignore) then
                        CommandLineData.Content.Justification_Option := CommandLineData.Ignore;
                     else -- error involving 'ignore'
                        CommandLineData.Content.Valid := False;
                        Possible_Error (E => ES_JustificationOption);
                     end if;
                  when 'f' => -- 1st letter of option
                     if Check_Option_Name (Opt_Name => Opt_Val,
                                           Str      => CommandLineData.Option_Justification_Option_Full) then
                        CommandLineData.Content.Justification_Option := CommandLineData.Full;
                     else -- error involving 'full'
                        CommandLineData.Content.Valid := False;
                        Possible_Error (E => ES_JustificationOption);
                     end if;
                  when 'b' => -- 1st letter of option
                     if Check_Option_Name (Opt_Name => Opt_Val,
                                           Str      => CommandLineData.Option_Justification_Option_Brief) then
                        CommandLineData.Content.Justification_Option := CommandLineData.Brief;
                     else -- error involving 'brief'
                        CommandLineData.Content.Valid := False;
                        Possible_Error (E => ES_JustificationOption);
                     end if;
                  when others =>
                     CommandLineData.Content.Valid := False;
                     Possible_Error (E => ES_JustificationOption);
               end case;
            end if;
         else
            CommandLineData.Content.Valid := False;
            Possible_Error2 (E => ES_InvalidOption,
                             F => Opt_Name);
         end if;
         --# end accept;
      end Process_J;

      procedure Process_L
      --# global in     FlowOptionFound;
      --#        in     Opt_Name;
      --#        in     Opt_Val;
      --#        in     Opt_Val_OK;
      --#        in out CommandLineData.Content;
      --#        in out LanguageProfileFound;
      --#        in out ListingFound;
      --#        in out SPARK_IO.File_Sys;
      --# derives CommandLineData.Content from *,
      --#                                      FlowOptionFound,
      --#                                      LanguageProfileFound,
      --#                                      ListingFound,
      --#                                      Opt_Name,
      --#                                      Opt_Val,
      --#                                      Opt_Val_OK &
      --#         LanguageProfileFound,
      --#         ListingFound            from *,
      --#                                      Opt_Name &
      --#         SPARK_IO.File_Sys       from *,
      --#                                      CommandLineData.Content,
      --#                                      LanguageProfileFound,
      --#                                      ListingFound,
      --#                                      Opt_Name,
      --#                                      Opt_Val,
      --#                                      Opt_Val_OK;
      is
      begin
         --# accept W, 169, CommandLineData.Content.Valid, "Direct updates OK here" &
         --#        W, 169, CommandLineData.Content.Flow_Option, "Direct updates OK here" &
         --#        W, 169, CommandLineData.Content.Language_Profile, "Direct updates OK here" &
         --#        W, 169, CommandLineData.Content.Listing_Extension, "Direct updates OK here";
         case Ada.Characters.Handling.To_Lower (E_Strings.Get_Element (E_Str => Opt_Name,
                                                                       Pos   => 2)) is
            when 'i' => -- 2nd letter
               if Check_Option_Name (Opt_Name => Opt_Name,
                                     Str      => CommandLineData.Option_Listing_Extension) then
                  CommandLineData.Content.Valid := Opt_Val_OK and then not ListingFound;
                  Possible_Error (E => ES_ListingExt);
                  ListingFound                              := True;
                  CommandLineData.Content.Listing_Extension := Opt_Val;
               else
                  CommandLineData.Content.Valid := False;
                  Possible_Error2 (E => ES_InvalidOption,
                                   F => Opt_Name);
               end if;

            when 'a' => -- 2nd letter
               if Check_Option_Name (Opt_Name => Opt_Name,
                                     Str      => CommandLineData.Option_Language) then
                  CommandLineData.Content.Valid := not LanguageProfileFound;
                  Possible_Error (E => ES_LanguageRepeated);
                  if CommandLineData.Content.Valid then
                     LanguageProfileFound := True;
                     -- now check argument - must be one of 83, 95, 2005, or KCG
                     case Ada.Characters.Handling.To_Lower (E_Strings.Get_Element (E_Str => Opt_Val,
                                                                                   Pos   => 1)) is
                        when '8' => -- 1st letter of option
                           if Check_Option_Name (Opt_Name => Opt_Val,
                                                 Str      => CommandLineData.Option_Language_83) then
                              CommandLineData.Content.Language_Profile := CommandLineData.SPARK83;
                              if not FlowOptionFound then
                                 CommandLineData.Content.Flow_Option := CommandLineData.Info_Flow;
                              end if;
                           else -- error involving '83'
                              CommandLineData.Content.Valid := False;
                              Possible_Error (E => ES_LanguageProfile);
                           end if;
                        when '9' =>
                           if Check_Option_Name (Opt_Name => Opt_Val,
                                                 Str      => CommandLineData.Option_Language_95) then
                              CommandLineData.Content.Language_Profile := CommandLineData.SPARK95;
                           else -- error involving '95'
                              CommandLineData.Content.Valid := False;
                              Possible_Error (E => ES_LanguageProfile);
                           end if;
                        when '2' =>
                           if Check_Option_Name (Opt_Name => Opt_Val,
                                                 Str      => CommandLineData.Option_Language_2005) then
                              CommandLineData.Content.Language_Profile := CommandLineData.SPARK2005;
                           else -- error involving '2005'
                              CommandLineData.Content.Valid := False;
                              Possible_Error (E => ES_LanguageProfile);
                           end if;
                        when 'k' =>
                           if Check_Option_Name (Opt_Name => Opt_Val,
                                                 Str      => CommandLineData.Option_Language_KCG)
                             and then CommandLineData.Content.Distribution_Is_Pro then
                              CommandLineData.Content.Language_Profile := CommandLineData.KCG;
                           else -- error involving 'KCG'
                              CommandLineData.Content.Valid := False;
                              Possible_Error (E => ES_LanguageProfile);
                           end if;
                        when others =>
                           CommandLineData.Content.Valid := False;
                           Possible_Error (E => ES_LanguageProfile);
                     end case;
                  end if;
               else
                  CommandLineData.Content.Valid := False;
                  Possible_Error2 (E => ES_InvalidOption,
                                   F => Opt_Name);
               end if;
            when others =>
               CommandLineData.Content.Valid := False;
               Possible_Error2 (E => ES_InvalidOption,
                                F => Opt_Name);
         end case;

         --# end accept;
      end Process_L;

      procedure Process_M
      --# global in     Opt_Name;
      --#        in out CommandLineData.Content;
      --#        in out Makefile_Found;
      --#        in out SPARK_IO.File_Sys;
      --# derives CommandLineData.Content,
      --#         SPARK_IO.File_Sys       from *,
      --#                                      CommandLineData.Content,
      --#                                      Makefile_Found,
      --#                                      Opt_Name &
      --#         Makefile_Found          from *,
      --#                                      Opt_Name;
      is
      begin
         --# accept W, 169, CommandLineData.Content.Valid, "Direct updates OK here" &
         --#        W, 169, CommandLineData.Content.Makefile_Mode, "Direct updates OK here";

         --  There is only a single option starting with m.
         if Check_Option_Name (Opt_Name => Opt_Name,
                               Str      => CommandLineData.Option_Makefile_Mode) then

            CommandLineData.Content.Valid := not Makefile_Found;
            Possible_Error (E => ES_Makefile_Repeated);

            if CommandLineData.Content.Valid then
               Makefile_Found                        := True;
               CommandLineData.Content.Makefile_Mode := True;
            end if;
         else
            CommandLineData.Content.Valid := False;
            Possible_Error2 (E => ES_InvalidOption,
                             F => Opt_Name);
         end if;
      end Process_M;

      procedure Process_N
      --# global in     DPCFound;
      --#        in     FDLreserveOptionFound;
      --#        in     HTMLFound;
      --#        in     Opt_Name;
      --#        in     VCGFound;
      --#        in     XMLFound;
      --#        in out CommandLineData.Content;
      --#        in out ConfigFileFound;
      --#        in out DictFound;
      --#        in out FDLignoreOptionFound;
      --#        in out IndexFound;
      --#        in out NoDurationFound;
      --#        in out NoListingsFound;
      --#        in out NoReportOptionFound;
      --#        in out NoWarningFound;
      --#        in out OutputFound;
      --#        in out ReportFound;
      --#        in out SPARK_IO.File_Sys;
      --#        in out StatisticsFound;
      --#        in out TargetDataFound;
      --# derives CommandLineData.Content,
      --#         SPARK_IO.File_Sys       from *,
      --#                                      CommandLineData.Content,
      --#                                      ConfigFileFound,
      --#                                      DictFound,
      --#                                      DPCFound,
      --#                                      FDLignoreOptionFound,
      --#                                      FDLreserveOptionFound,
      --#                                      HTMLFound,
      --#                                      IndexFound,
      --#                                      NoDurationFound,
      --#                                      NoListingsFound,
      --#                                      NoWarningFound,
      --#                                      Opt_Name,
      --#                                      OutputFound,
      --#                                      ReportFound,
      --#                                      StatisticsFound,
      --#                                      TargetDataFound,
      --#                                      VCGFound,
      --#                                      XMLFound &
      --#         ConfigFileFound,
      --#         DictFound,
      --#         FDLignoreOptionFound,
      --#         IndexFound,
      --#         NoDurationFound,
      --#         NoListingsFound,
      --#         NoReportOptionFound,
      --#         NoWarningFound,
      --#         OutputFound,
      --#         ReportFound,
      --#         StatisticsFound,
      --#         TargetDataFound         from *,
      --#                                      Opt_Name;
      is
      begin
         --# accept W, 169, CommandLineData.Content.Valid, "Direct updates OK here" &
         --#        W, 169, CommandLineData.Content.Index, "Direct updates OK here" &
         --#        W, 169, CommandLineData.Content.Warning, "Direct updates OK here" &
         --#        W, 169, CommandLineData.Content.Echo, "Direct updates OK here" &
         --#        W, 169, CommandLineData.Content.Generate_SLI, "Direct updates OK here" &
         --#        W, 169, CommandLineData.Content.Report, "Direct updates OK here" &
         --#        W, 169, CommandLineData.Content.No_Duration, "Direct updates OK here" &
         --#        W, 169, CommandLineData.Content.Write_Dict, "Direct updates OK here" &
         --#        W, 169, CommandLineData.Content.Write_Statistics, "Direct updates OK here" &
         --#        W, 169, CommandLineData.Content.FDL_Reserved, "Direct updates OK here" &
         --#        W, 169, CommandLineData.Content.Target_Data , "Direct updates OK here" &
         --#        W, 169, CommandLineData.Content.Target_Config, "Direct updates OK here" &
         --#        W, 169, CommandLineData.Content.No_Listings, "Direct updates OK here";
         case Ada.Characters.Handling.To_Lower (E_Strings.Get_Element (E_Str => Opt_Name,
                                                                       Pos   => 3)) is
            when 'i' => -- 3rd letter
               if Check_Option_Name (Opt_Name => Opt_Name,
                                     Str      => "no" & CommandLineData.Option_Index_File) then
                  CommandLineData.Content.Valid := not IndexFound;
                  Possible_Error (E => ES_NoIndex);
                  IndexFound                    := True;
                  CommandLineData.Content.Index := False;
               else
                  CommandLineData.Content.Valid := False;
                  Possible_Error2 (E => ES_InvalidOption,
                                   F => Opt_Name);
               end if;

            when 'w' => -- 3rd letter
               if Check_Option_Name (Opt_Name => Opt_Name,
                                     Str      => "no" & CommandLineData.Option_Warning_File) then
                  CommandLineData.Content.Valid := not NoWarningFound;
                  Possible_Error (E => ES_NoWarning);
                  NoWarningFound                  := True;
                  CommandLineData.Content.Warning := False;
               else
                  CommandLineData.Content.Valid := False;
                  Possible_Error2 (E => ES_InvalidOption,
                                   F => Opt_Name);
               end if;

            when 'e' => -- 3rd letter
               if Check_Option_Name (Opt_Name => Opt_Name,
                                     Str      => CommandLineData.Option_No_Echo) then
                  CommandLineData.Content.Valid := not OutputFound;
                  Possible_Error (E => ES_NoEcho);
                  OutputFound                  := True;
                  CommandLineData.Content.Echo := False;
               else
                  CommandLineData.Content.Valid := False;
                  Possible_Error2 (E => ES_InvalidOption,
                                   F => Opt_Name);
               end if;
            when 'r' => -- 3rd letter
               if Check_Option_Name (Opt_Name => Opt_Name,
                                     Str      => "no" & CommandLineData.Option_Report_File) then
                  CommandLineData.Content.Valid := not (ReportFound or else HTMLFound or else XMLFound);
                  Possible_Error (E => ES_NoReport);
                  ReportFound                    := True;
                  NoReportOptionFound            := True;
                  CommandLineData.Content.Report := False;
               else
                  CommandLineData.Content.Valid := False;
                  Possible_Error2 (E => ES_InvalidOption,
                                   F => Opt_Name);
               end if;
            when 'd' => -- 3rd letter
               case Ada.Characters.Handling.To_Lower (E_Strings.Get_Element (E_Str => Opt_Name,
                                                                             Pos   => 4)) is
                  when 'i' => -- 4th letter
                     if Check_Option_Name (Opt_Name => Opt_Name,
                                           Str      => CommandLineData.Option_No_Dictionary) then
                        CommandLineData.Content.Valid := not DictFound;
                        Possible_Error (E => ES_NoDict);
                        DictFound                          := True;
                        CommandLineData.Content.Write_Dict := False;
                     else
                        CommandLineData.Content.Valid := False;
                        Possible_Error2 (E => ES_InvalidOption,
                                         F => Opt_Name);
                     end if;
                  when 'u' => -- 4th letter
                     if Check_Option_Name (Opt_Name => Opt_Name,
                                           Str      => CommandLineData.Option_No_Duration) then
                        CommandLineData.Content.Valid := not NoDurationFound;
                        Possible_Error (E => ES_NoDuration);
                        NoDurationFound                     := True;
                        CommandLineData.Content.No_Duration := True;
                     else
                        CommandLineData.Content.Valid := False;
                        Possible_Error2 (E => ES_InvalidOption,
                                         F => Opt_Name);
                     end if;
                  when others =>
                     CommandLineData.Content.Valid := False;
                     Possible_Error2 (E => ES_InvalidOption,
                                      F => Opt_Name);
               end case;
            when 's' => -- 3rd letter
               case Ada.Characters.Handling.To_Lower (E_Strings.Get_Element (E_Str => Opt_Name,
                                                                             Pos   => 4)) is
                  when 'l' => -- 4th letter
                     if Check_Option_Name (Opt_Name => Opt_Name,
                                           Str      => CommandLineData.Option_No_Sli) then
                        CommandLineData.Content.Generate_SLI := False;
                     else
                        CommandLineData.Content.Valid := False;
                        Possible_Error2 (E => ES_InvalidOption,
                                         F => Opt_Name);
                     end if;
                  when 't' => -- 4th letter
                     if Check_Option_Name (Opt_Name => Opt_Name,
                                           Str      => "no" & CommandLineData.Option_Statistics) then
                        CommandLineData.Content.Valid := not StatisticsFound;
                        Possible_Error (E => ES_NoStatistics);
                        StatisticsFound                          := True;
                        CommandLineData.Content.Write_Statistics := False;
                     else
                        CommandLineData.Content.Valid := False;
                        Possible_Error2 (E => ES_InvalidOption,
                                         F => Opt_Name);
                     end if;
                  when 'w' => -- 4th Letter

                     -- -noswitch
                     --
                     -- Already processed by Ignore_Default_Switch_File below,
                     -- so allow but ignore here.
                     if Check_Option_Name (Opt_Name => Opt_Name,
                                           Str      => CommandLineData.Option_No_Switch) then
                        null;
                     else
                        CommandLineData.Content.Valid := False;
                        Possible_Error2 (E => ES_InvalidOption,
                                         F => Opt_Name);
                     end if;
                  when others =>
                     CommandLineData.Content.Valid := False;
                     Possible_Error2 (E => ES_InvalidOption,
                                      F => Opt_Name);
               end case;
            when 'f' => -- 3rd letter
               if Check_Option_Name (Opt_Name => Opt_Name,
                                     Str      => "no" & CommandLineData.Option_Fdl_Identifiers) then
                  CommandLineData.Content.Valid :=
                    not (FDLreserveOptionFound or else FDLignoreOptionFound or else DPCFound or else VCGFound);
                  Possible_Error (E => ES_FDLoption);
                  FDLignoreOptionFound                 := True;
                  CommandLineData.Content.FDL_Reserved := False;
                  ScreenEcho.Put_Line ("Warning: the -nofdl option is now deprecated. Please use -fdl=accept");
               else
                  CommandLineData.Content.Valid := False;
                  Possible_Error2 (E => ES_InvalidOption,
                                   F => Opt_Name);
               end if;

            when 't' => -- 3rd letter
               if Check_Option_Name (Opt_Name => Opt_Name,
                                     Str      => "no" & CommandLineData.Option_Target_Compiler_Data) then
                  CommandLineData.Content.Valid := not TargetDataFound;
                  Possible_Error (E => ES_NoTargetData);
                  TargetDataFound                     := True;
                  CommandLineData.Content.Target_Data := False;
               else
                  CommandLineData.Content.Valid := False;
                  Possible_Error2 (E => ES_InvalidOption,
                                   F => Opt_Name);
               end if;

            when 'c' => -- 3rd letter
               if Check_Option_Name (Opt_Name => Opt_Name,
                                     Str      => "no" & CommandLineData.Option_Config_File) then
                  CommandLineData.Content.Valid := not ConfigFileFound;
                  Possible_Error (E => ES_NoConfigFile);
                  ConfigFileFound                       := True;
                  CommandLineData.Content.Target_Config := False;
               else
                  CommandLineData.Content.Valid := False;
                  Possible_Error2 (E => ES_InvalidOption,
                                   F => Opt_Name);
               end if;

            when 'l' => -- 3rd letter
               if Check_Option_Name (Opt_Name => Opt_Name,
                                     Str      => CommandLineData.Option_No_Listings) then
                  CommandLineData.Content.Valid := not NoListingsFound;
                  Possible_Error (E => ES_NoListings);
                  NoListingsFound                     := True;
                  CommandLineData.Content.No_Listings := True;
               else
                  CommandLineData.Content.Valid := False;
                  Possible_Error2 (E => ES_InvalidOption,
                                   F => Opt_Name);
               end if;

            when others =>
               CommandLineData.Content.Valid := False;
               Possible_Error2 (E => ES_InvalidOption,
                                F => Opt_Name);
         end case;
         --# end accept;
      end Process_N;

      procedure Process_O
      --# global in     Opt_Name;
      --#        in     Opt_Val;
      --#        in     Opt_Val_OK;
      --#        in out CommandLineData.Content;
      --#        in out OriginalFlowErrorsFound;
      --#        in out OutputDirectoryFound;
      --#        in out SPARK_IO.File_Sys;
      --# derives CommandLineData.Content from *,
      --#                                      Opt_Name,
      --#                                      Opt_Val,
      --#                                      Opt_Val_OK,
      --#                                      OriginalFlowErrorsFound,
      --#                                      OutputDirectoryFound &
      --#         OriginalFlowErrorsFound from *,
      --#                                      Opt_Name &
      --#         OutputDirectoryFound    from *,
      --#                                      Opt_Name,
      --#                                      Opt_Val_OK &
      --#         SPARK_IO.File_Sys       from *,
      --#                                      CommandLineData.Content,
      --#                                      Opt_Name,
      --#                                      Opt_Val_OK,
      --#                                      OriginalFlowErrorsFound,
      --#                                      OutputDirectoryFound;
      is
      begin
         --# accept W, 169, CommandLineData.Content.Valid, "Direct updates OK here" &
         --#        W, 169, CommandLineData.Content.Output_Directory, "Direct updates OK here" &
         --#        W, 169, CommandLineData.Content.Output_Directory_Name, "Direct updates OK here" &
         --#        W, 169, CommandLineData.Content.Legacy_Errors, "Direct updates OK here";
         case Ada.Characters.Handling.To_Lower (E_Strings.Get_Element (E_Str => Opt_Name,
                                                                       Pos   => 2)) is
            when 'r' => -- 2nd letter
               if Check_Option_Name (Opt_Name => Opt_Name,
                                     Str      => CommandLineData.Option_Original_Flow_Errors) then
                  CommandLineData.Content.Valid := not OriginalFlowErrorsFound;
                  Possible_Error (E => ES_OriginalFlowErrors);
                  OriginalFlowErrorsFound               := True;
                  CommandLineData.Content.Legacy_Errors := True;
               else
                  CommandLineData.Content.Valid := False;
                  Possible_Error2 (E => ES_InvalidOption,
                                   F => Opt_Name);
               end if;
            when 'u' => -- 2nd letter
               if Check_Option_Name (Opt_Name => Opt_Name,
                                     Str      => CommandLineData.Option_Output_Directory) then
                  CommandLineData.Content.Valid := Opt_Val_OK;
                  Possible_Error (E => ES_OutputDir);
                  if Opt_Val_OK then
                     CommandLineData.Content.Valid := not OutputDirectoryFound;
                     Possible_Error (E => ES_OutputDirRepeated);
                  end if;

                  if CommandLineData.Content.Valid then
                     OutputDirectoryFound                          := True;
                     CommandLineData.Content.Output_Directory      := True;
                     CommandLineData.Content.Output_Directory_Name := Opt_Val;
                  end if;
               else
                  CommandLineData.Content.Valid := False;
                  Possible_Error2 (E => ES_InvalidOption,
                                   F => Opt_Name);
               end if;
            when others =>
               CommandLineData.Content.Valid := False;
               Possible_Error2 (E => ES_InvalidOption,
                                F => Opt_Name);
         end case;
         --# end accept;
      end Process_O;

      procedure Process_P
      --# global in     Opt_Name;
      --#        in     Opt_Val;
      --#        in out CommandLineData.Content;
      --#        in out ConcurrencyProfileFound;
      --#        in out PlainOutputFound;
      --#        in out SPARK_IO.File_Sys;
      --# derives CommandLineData.Content,
      --#         SPARK_IO.File_Sys       from *,
      --#                                      CommandLineData.Content,
      --#                                      ConcurrencyProfileFound,
      --#                                      Opt_Name,
      --#                                      Opt_Val,
      --#                                      PlainOutputFound &
      --#         ConcurrencyProfileFound,
      --#         PlainOutputFound        from *,
      --#                                      Opt_Name;
      is
      begin
         --# accept W, 169, CommandLineData.Content.Valid, "Direct updates OK here" &
         --#        W, 169, CommandLineData.Content.Plain_Output, "Direct updates OK here" &
         --#        W, 169, CommandLineData.Content.Info_Flow_Policy, "Direct updates OK here" &
         --#        W, 169, CommandLineData.Content.Concurrency_Profile, "Direct updates OK here";
         case Ada.Characters.Handling.To_Lower (E_Strings.Get_Element (E_Str => Opt_Name,
                                                                       Pos   => 2)) is
            when 'f' => -- 2nd letter
               CommandLineData.Content.Valid := False;
               if Check_Option_Name (Opt_Name => Opt_Name,
                                     Str      => "pfs") then
                  Possible_Error (E => ES_NoMorePFS);
               else
                  Possible_Error2 (E => ES_InvalidOption,
                                   F => Opt_Name);
               end if;

            when 'l' => -- 2nd letter
               if Check_Option_Name (Opt_Name => Opt_Name,
                                     Str      => CommandLineData.Option_Plain_Output) then
                  CommandLineData.Content.Valid := not PlainOutputFound;
                  Possible_Error (E => ES_PlainOutput);
                  PlainOutputFound                     := True;
                  CommandLineData.Content.Plain_Output := True;
               else
                  CommandLineData.Content.Valid := False;
                  Possible_Error2 (E => ES_InvalidOption,
                                   F => Opt_Name);
               end if;

            when 'r' => -- 2nd letter
               if Check_Option_Name (Opt_Name => Opt_Name,
                                     Str      => CommandLineData.Option_Profile) then
                  CommandLineData.Content.Valid := not ConcurrencyProfileFound;
                  Possible_Error (E => ES_Profile);
                  if CommandLineData.Content.Valid then
                     ConcurrencyProfileFound := True;
                     case Ada.Characters.Handling.To_Lower (E_Strings.Get_Element (E_Str => Opt_Val,
                                                                                   Pos   => 1)) is
                        when 'r' => -- 1st letter of option
                           if Check_Option_Name (Opt_Name => Opt_Val,
                                                 Str      => CommandLineData.Option_Profile_Ravenscar) then
                              CommandLineData.Content.Concurrency_Profile := CommandLineData.Ravenscar;
                           else -- other error involving ravenscar
                              CommandLineData.Content.Valid := False;
                              Possible_Error2 (E => ES_ProfileOption,
                                               F => Opt_Val);
                           end if;

                        when 's' => -- 1st letter of option
                           if Check_Option_Name (Opt_Name => Opt_Val,
                                                 Str      => CommandLineData.Option_Profile_Sequential) then
                              CommandLineData.Content.Concurrency_Profile := CommandLineData.Sequential;
                           else
                              CommandLineData.Content.Valid := False;
                              Possible_Error2 (E => ES_ProfileOption,
                                               F => Opt_Val);
                           end if;

                        when others =>
                           CommandLineData.Content.Valid := False;
                           Possible_Error2 (E => ES_ProfileOption,
                                            F => Opt_Val);
                     end case;
                  end if;
               else -- begins with "pr" but not "profile"
                  CommandLineData.Content.Valid := False;
                  Possible_Error2 (E => ES_InvalidOption,
                                   F => Opt_Name);
               end if;

            when 'o' => -- 2nd letter
               if Check_Option_Name (Opt_Name => Opt_Name,
                                     Str      => CommandLineData.Option_Policy) then
                  CommandLineData.Content.Valid := CommandLineData.Content.Flow_Option = CommandLineData.Info_Flow;
                  Possible_Error (E => ES_DataFlowAndInfoFlowPolicy);
                  if CommandLineData.Content.Valid then
                     case Ada.Characters.Handling.To_Lower (E_Strings.Get_Element (E_Str => Opt_Val,
                                                                                   Pos   => 1)) is
                        when 's' => -- 1st letter of option
                           case Ada.Characters.Handling.To_Lower (E_Strings.Get_Element (E_Str => Opt_Val,
                                                                                         Pos   => 2)) is
                              when 'e' =>
                                 if Check_Option_Name (Opt_Name => Opt_Val,
                                                       Str      => CommandLineData.Option_Policy_Security) then
                                    CommandLineData.Content.Info_Flow_Policy := CommandLineData.Security;
                                 else
                                    CommandLineData.Content.Valid := False;
                                    Possible_Error2 (E => ES_ProfileOption,
                                                     F => Opt_Val);
                                 end if;
                              when 'a' =>
                                 if Check_Option_Name (Opt_Name => Opt_Val,
                                                       Str      => CommandLineData.Option_Policy_Safety) then
                                    CommandLineData.Content.Info_Flow_Policy := CommandLineData.Safety;
                                 else
                                    CommandLineData.Content.Valid := False;
                                    Possible_Error2 (E => ES_ProfileOption,
                                                     F => Opt_Val);
                                 end if;
                              when others =>
                                 CommandLineData.Content.Valid := False;
                                 Possible_Error2 (E => ES_ProfileOption,
                                                  F => Opt_Val);
                           end case;
                        when others =>
                           CommandLineData.Content.Valid := False;
                           Possible_Error2 (E => ES_ProfileOption,
                                            F => Opt_Val);
                     end case;
                  end if;
               end if;

               -- begin with "p" but not a valid option
            when others =>
               CommandLineData.Content.Valid := False;
               Possible_Error2 (E => ES_InvalidOption,
                                F => Opt_Name);
         end case;
         --# end accept;
      end Process_P;

      procedure Process_R
      --# global in     Opt_Name;
      --#        in     Opt_Val;
      --#        in     Opt_Val_OK;
      --#        in out CommandLineData.Content;
      --#        in out ReportFound;
      --#        in out RulesFound;
      --#        in out SPARK_IO.File_Sys;
      --# derives CommandLineData.Content,
      --#         SPARK_IO.File_Sys       from *,
      --#                                      CommandLineData.Content,
      --#                                      Opt_Name,
      --#                                      Opt_Val,
      --#                                      Opt_Val_OK,
      --#                                      ReportFound,
      --#                                      RulesFound &
      --#         ReportFound             from *,
      --#                                      Opt_Name,
      --#                                      Opt_Val_OK &
      --#         RulesFound              from *,
      --#                                      Opt_Name;
      is
         Default_Report_Extension : constant String := "rep";
         File_Name                : E_Strings.T;
      begin
         --# accept W, 169, CommandLineData.Content.Valid, "Direct updates OK here" &
         --#        W, 169, CommandLineData.Content.Report, "Direct updates OK here" &
         --#        W, 169, CommandLineData.Content.Report_File_Name, "Direct updates OK here" &
         --#        W, 169, CommandLineData.Content.Constant_Rules, "Direct updates OK here";
         case Ada.Characters.Handling.To_Lower (E_Strings.Get_Element (E_Str => Opt_Name,
                                                                       Pos   => 2)) is
            when 'e' => -- 2nd letter
               case Ada.Characters.Handling.To_Lower (E_Strings.Get_Element (E_Str => Opt_Name,
                                                                             Pos   => 3)) is
                  when 'p' => -- 3rd letter
                     if Check_Option_Name (Opt_Name => Opt_Name,
                                           Str      => CommandLineData.Option_Report_File) then
                        CommandLineData.Content.Valid := Opt_Val_OK;
                        Possible_Error (E => ES_ReportName);
                        if Opt_Val_OK then
                           CommandLineData.Content.Valid := not ReportFound;
                           Possible_Error (E => ES_Report);
                        end if;
                        if CommandLineData.Content.Valid then
                           ReportFound                    := True;
                           CommandLineData.Content.Report := True;
                           File_Name                      := Opt_Val;
                           FileSystem.Check_Extension
                             (Fn  => File_Name,
                              Ext => E_Strings.Copy_String (Str => Default_Report_Extension));
                           CommandLineData.Content.Report_File_Name := File_Name;
                        end if;
                     else -- starts "rep" but is not valid
                        CommandLineData.Content.Valid := False;
                        Possible_Error2 (E => ES_InvalidOption,
                                         F => Opt_Name);
                     end if;

                  when 'a' => -- 3rd letter
                     CommandLineData.Content.Valid := False;
                     if Check_Option_Name (Opt_Name => Opt_Name,
                                           Str      => "realrtcs") then
                        Possible_Error (E => ES_NoMoreReal);
                     else
                        Possible_Error2 (E => ES_InvalidOption,
                                         F => Opt_Name);
                     end if;

                  when others =>
                     -- starts "re" but isn't valid
                     CommandLineData.Content.Valid := False;
                     Possible_Error2 (E => ES_InvalidOption,
                                      F => Opt_Name);
               end case; -- 3rd letter

            when 't' => -- 2nd letter
               CommandLineData.Content.Valid := False;
               if Check_Option_Name (Opt_Name => Opt_Name,
                                     Str      => "rtc") then
                  Possible_Error (E => ES_NoMoreRTC);
               else
                  Possible_Error2 (E => ES_InvalidOption,
                                   F => Opt_Name);
               end if;
            when 'u' => -- 2nd letter u - should be "rules" switch
               if Check_Option_Name (Opt_Name => Opt_Name,
                                     Str      => CommandLineData.Option_Rules) then
                  if RulesFound then
                     CommandLineData.Content.Valid := False;
                     Possible_Error (E => ES_Rules);
                  else
                     RulesFound                    := True;
                     CommandLineData.Content.Valid := Opt_Val_OK;
                     if CommandLineData.Content.Valid then
                        case Ada.Characters.Handling.To_Lower (E_Strings.Get_Element (E_Str => Opt_Val,
                                                                                      Pos   => 1)) is
                           when 'n' => -- 1st letter of option
                              if Check_Option_Name (Opt_Name => Opt_Val,
                                                    Str      => CommandLineData.Option_Rules_None) then
                                 CommandLineData.Content.Constant_Rules := CommandLineData.No_Rules;
                              else
                                 CommandLineData.Content.Valid := False;
                                 Possible_Error (E => ES_RuleUnknown);
                              end if;

                           when 'l' => -- 1st letter of option
                              if Check_Option_Name (Opt_Name => Opt_Val,
                                                    Str      => CommandLineData.Option_Rules_Lazy) then
                                 CommandLineData.Content.Constant_Rules := CommandLineData.Lazy;
                              else
                                 CommandLineData.Content.Valid := False;
                                 Possible_Error (E => ES_RuleUnknown);
                              end if;

                           when 'k' => -- 1st letter of option
                              if Check_Option_Name (Opt_Name => Opt_Val,
                                                    Str      => CommandLineData.Option_Rules_Keen) then
                                 CommandLineData.Content.Constant_Rules := CommandLineData.Keen;
                              else
                                 CommandLineData.Content.Valid := False;
                                 Possible_Error (E => ES_RuleUnknown);
                              end if;

                           when 'a' => -- 1st letter of option
                              if Check_Option_Name (Opt_Name => Opt_Val,
                                                    Str      => CommandLineData.Option_Rules_All) then
                                 CommandLineData.Content.Constant_Rules := CommandLineData.All_Rules;
                              else
                                 CommandLineData.Content.Valid := False;
                                 Possible_Error (E => ES_RuleUnknown);
                              end if;
                           when others =>
                              CommandLineData.Content.Valid := False;
                              Possible_Error (E => ES_RuleUnknown);
                        end case;
                     else
                        CommandLineData.Content.Valid := False;
                        Possible_Error (E => ES_RuleUnknown);
                     end if;
                  end if;
               else
                  CommandLineData.Content.Valid := False;
                  Possible_Error2 (E => ES_InvalidOption,
                                   F => Opt_Name);
               end if;

            when others =>
               -- starts "r" but not valid
               CommandLineData.Content.Valid := False;
               Possible_Error2 (E => ES_InvalidOption,
                                F => Opt_Name);
         end case;
         --# end accept;
      end Process_R;

      procedure Process_S
      --# global in     Opt_Name;
      --#        in     Opt_Val;
      --#        in     Opt_Val_OK;
      --#        in out CommandLineData.Content;
      --#        in out SourceFound;
      --#        in out SPARK_IO.File_Sys;
      --#        in out StatisticsFound;
      --#        in out SyntaxCheckFound;
      --# derives CommandLineData.Content from *,
      --#                                      Opt_Name,
      --#                                      Opt_Val,
      --#                                      Opt_Val_OK,
      --#                                      SourceFound,
      --#                                      StatisticsFound,
      --#                                      SyntaxCheckFound &
      --#         SourceFound,
      --#         StatisticsFound,
      --#         SyntaxCheckFound        from *,
      --#                                      Opt_Name &
      --#         SPARK_IO.File_Sys       from *,
      --#                                      CommandLineData.Content,
      --#                                      Opt_Name,
      --#                                      Opt_Val_OK,
      --#                                      SourceFound,
      --#                                      StatisticsFound,
      --#                                      SyntaxCheckFound;
      is
      begin
         --# accept W, 169, CommandLineData.Content.Write_Statistics, "Direct updates OK here" &
         --#        W, 169, CommandLineData.Content.Source_Extension, "Direct updates OK here" &
         --#        W, 169, CommandLineData.Content.SPARK_Lib,        "Direct updates OK here" &
         --#        W, 169, CommandLineData.Content.Syntax_Only,      "Direct updates OK here" &
         --#        W, 169, CommandLineData.Content.Valid,            "Direct updates OK here";
         case Ada.Characters.Handling.To_Lower (E_Strings.Get_Element (E_Str => Opt_Name,
                                                                       Pos   => 2)) is
            when 'o' =>
               if Check_Option_Name (Opt_Name => Opt_Name,
                                     Str      => CommandLineData.Option_Source_Extension) then
                  CommandLineData.Content.Valid := Opt_Val_OK and then not SourceFound;
                  Possible_Error (E => ES_SourceExt);
                  SourceFound                              := True;
                  CommandLineData.Content.Source_Extension := Opt_Val;
               else
                  CommandLineData.Content.Valid := False;
                  Possible_Error2 (E => ES_InvalidOption,
                                   F => Opt_Name);
               end if;

            when 'p' =>
               if Check_Option_Name (Opt_Name => Opt_Name,
                                     Str      => CommandLineData.Option_SPARK_Lib) then
                  CommandLineData.Content.SPARK_Lib := True;
               else
                  CommandLineData.Content.Valid := False;
                  Possible_Error2 (E => ES_InvalidOption,
                                   F => Opt_Name);
               end if;

            when 't' =>
               if Check_Option_Name (Opt_Name => Opt_Name,
                                     Str      => CommandLineData.Option_Statistics) then
                  CommandLineData.Content.Valid := not StatisticsFound;
                  Possible_Error (E => ES_Statistics);
                  StatisticsFound                          := True;
                  CommandLineData.Content.Write_Statistics := True;
               else
                  CommandLineData.Content.Valid := False;
                  Possible_Error2 (E => ES_InvalidOption,
                                   F => Opt_Name);
               end if;

            when 'y' =>
               if Check_Option_Name (Opt_Name => Opt_Name,
                                     Str      => CommandLineData.Option_Syntax_Check) then
                  CommandLineData.Content.Valid := not SyntaxCheckFound;
                  Possible_Error (E => ES_Syntax);
                  SyntaxCheckFound                    := True;
                  CommandLineData.Content.Syntax_Only := True;
               else
                  CommandLineData.Content.Valid := False;
                  Possible_Error2 (E => ES_InvalidOption,
                                   F => Opt_Name);
               end if;

            when others =>
               CommandLineData.Content.Valid := False;
               Possible_Error2 (E => ES_InvalidOption,
                                F => Opt_Name);
         end case;
         --# end accept;
      end Process_S;

      procedure Process_T
      --# global in     ConfigFileFound;
      --#        in     Opt_Name;
      --#        in     Opt_Val;
      --#        in     Opt_Val_OK;
      --#        in out CommandLineData.Content;
      --#        in out SPARK_IO.File_Sys;
      --#        in out TargetDataFound;
      --# derives CommandLineData.Content from *,
      --#                                      ConfigFileFound,
      --#                                      Opt_Name,
      --#                                      Opt_Val,
      --#                                      Opt_Val_OK,
      --#                                      TargetDataFound &
      --#         SPARK_IO.File_Sys       from *,
      --#                                      CommandLineData.Content,
      --#                                      ConfigFileFound,
      --#                                      Opt_Name,
      --#                                      Opt_Val_OK,
      --#                                      TargetDataFound &
      --#         TargetDataFound         from *,
      --#                                      ConfigFileFound,
      --#                                      Opt_Name,
      --#                                      Opt_Val_OK;
      is
         File_Name : E_Strings.T;
      begin
         --# accept W, 169, CommandLineData.Content.Valid, "Direct updates OK here" &
         --#        W, 169, CommandLineData.Content.Target_Data, "Direct updates OK here" &
         --#        W, 169, CommandLineData.Content.Target_Data_File, "Direct updates OK here";
         case Ada.Characters.Handling.To_Lower (E_Strings.Get_Element (E_Str => Opt_Name,
                                                                       Pos   => 2)) is
            -- -tree is removed in release 8.1.1 and above, but it remains
            -- the default, so at least recognize it here and take no action
            -- for backward compatiblility with users' existing scripts.
            when 'r' => -- 2nd letter
               if not Check_Option_Name (Opt_Name => Opt_Name,
                                         Str      => "tree") then
                  CommandLineData.Content.Valid := False;
                  Possible_Error2 (E => ES_InvalidOption,
                                   F => Opt_Name);
               end if;

            when 'a' => -- 2nd letter
               if Check_Option_Name (Opt_Name => Opt_Name,
                                     Str      => CommandLineData.Option_Target_Compiler_Data) then
                  if ConfigFileFound then
                     CommandLineData.Content.Valid := False;
                     Possible_Error (E => ES_DataAndConfig);
                  else
                     CommandLineData.Content.Valid := Opt_Val_OK;
                     Possible_Error (E => ES_TargetDataName);
                     if Opt_Val_OK then
                        CommandLineData.Content.Valid := not TargetDataFound;
                        Possible_Error (E => ES_TargetData);
                     end if;

                     if CommandLineData.Content.Valid then
                        TargetDataFound                     := True;
                        CommandLineData.Content.Target_Data := True;
                        File_Name                           := Opt_Val;
                        FileSystem.Check_Extension
                          (Fn  => File_Name,
                           Ext => E_Strings.Copy_String (Str => CommandLineData.Default_Data_Extension));
                        CommandLineData.Content.Target_Data_File := File_Name;
                     end if;
                  end if;
               else
                  CommandLineData.Content.Valid := False;
                  Possible_Error2 (E => ES_InvalidOption,
                                   F => Opt_Name);
               end if;

            when others =>
               CommandLineData.Content.Valid := False;
               Possible_Error2 (E => ES_InvalidOption,
                                F => Opt_Name);
         end case;
         --# end accept;
      end Process_T;

      procedure Process_V
      --# global in     FDLignoreOptionFound;
      --#        in     Opt_Name;
      --#        in out CommandLineData.Content;
      --#        in out SPARK_IO.File_Sys;
      --#        in out VCGFound;
      --# derives CommandLineData.Content,
      --#         SPARK_IO.File_Sys       from *,
      --#                                      CommandLineData.Content,
      --#                                      FDLignoreOptionFound,
      --#                                      Opt_Name,
      --#                                      VCGFound &
      --#         VCGFound                from *,
      --#                                      Opt_Name;
      is
      begin
         --# accept W, 169, CommandLineData.Content.Valid, "Direct updates OK here" &
         --#        W, 169, CommandLineData.Content.VCG, "Direct updates OK here" &
         --#        W, 169, CommandLineData.Content.Plain_Output, "Direct updates OK here" &
         --#        W, 169, CommandLineData.Content.Version_Requested, "Direct updates OK here";
         case Ada.Characters.Handling.To_Lower (E_Strings.Get_Element (E_Str => Opt_Name,
                                                                       Pos   => 2)) is
            when 'c' => -- 2nd letter
               if Check_Option_Name (Opt_Name => Opt_Name,
                                     Str      => CommandLineData.Option_Vcg) then
                  if VCGFound then
                     CommandLineData.Content.Valid := False;
                     Possible_Error (E => ES_VCGRepeated);
                  elsif FDLignoreOptionFound and then E_Strings.Is_Empty (E_Str => CommandLineData.Content.FDL_Mangle) then
                     CommandLineData.Content.Valid := False;
                     Possible_Error (E => ES_VCGandFDL);
                  else
                     CommandLineData.Content.Valid := True;
                  end if;
                  VCGFound                    := True;
                  CommandLineData.Content.VCG := True;
               else
                  CommandLineData.Content.Valid := False;
                  Possible_Error2 (E => ES_InvalidOption,
                                   F => Opt_Name);
               end if;
            when 'e' => -- 2nd letter
               if Check_Option_Name (Opt_Name => Opt_Name,
                                     Str      => CommandLineData.Option_Version) then
                  -- Examiner version requested, so abandon all further
                  -- option processing by setting Valid = False.
                  CommandLineData.Content.Valid             := False;
                  CommandLineData.Content.Version_Requested := True;
                  CommandLineData.Content.Plain_Output      := False;
               else
                  CommandLineData.Content.Valid := False;
                  Possible_Error2 (E => ES_InvalidOption,
                                   F => Opt_Name);
               end if;
            when others =>
               CommandLineData.Content.Valid := False;
               Possible_Error2 (E => ES_InvalidOption,
                                F => Opt_Name);
         end case;
         --# end accept;
      end Process_V;

      procedure Process_W
      --# global in     Opt_Name;
      --#        in     Opt_Val;
      --#        in     Opt_Val_OK;
      --#        in out CommandLineData.Content;
      --#        in out SPARK_IO.File_Sys;
      --#        in out WarningFound;
      --# derives CommandLineData.Content from *,
      --#                                      Opt_Name,
      --#                                      Opt_Val,
      --#                                      Opt_Val_OK,
      --#                                      WarningFound &
      --#         SPARK_IO.File_Sys       from *,
      --#                                      CommandLineData.Content,
      --#                                      Opt_Name,
      --#                                      Opt_Val_OK,
      --#                                      WarningFound &
      --#         WarningFound            from *,
      --#                                      Opt_Name,
      --#                                      Opt_Val_OK;
      is
         File_Name : E_Strings.T;
      begin
         --# accept W, 169, CommandLineData.Content.Valid, "Direct updates OK here" &
         --#        W, 169, CommandLineData.Content.Warning, "Direct updates OK here" &
         --#        W, 169, CommandLineData.Content.Warning_File_Name, "Direct updates OK here";
         if Check_Option_Name (Opt_Name => Opt_Name,
                               Str      => CommandLineData.Option_Warning_File) then
            CommandLineData.Content.Valid := Opt_Val_OK;
            Possible_Error (E => ES_WarningName);
            if Opt_Val_OK then
               CommandLineData.Content.Valid := not WarningFound;
               Possible_Error (E => ES_Warning);
            end if;
            if CommandLineData.Content.Valid then
               WarningFound                    := True;
               CommandLineData.Content.Warning := True;
               File_Name                       := Opt_Val;
               FileSystem.Check_Extension
                 (Fn  => File_Name,
                  Ext => E_Strings.Copy_String (Str => CommandLineData.Default_Warning_Extension));
               CommandLineData.Content.Warning_File_Name := File_Name;
            end if;
         else
            CommandLineData.Content.Valid := False;
            Possible_Error2 (E => ES_InvalidOption,
                             F => Opt_Name);
         end if;
         --# end accept;
      end Process_W;

      procedure Process_X
      --# global in     HTMLFound;
      --#        in     NoReportOptionFound;
      --#        in     Opt_Name;
      --#        in out CommandLineData.Content;
      --#        in out SPARK_IO.File_Sys;
      --#        in out XMLFound;
      --# derives CommandLineData.Content,
      --#         SPARK_IO.File_Sys       from *,
      --#                                      CommandLineData.Content,
      --#                                      HTMLFound,
      --#                                      NoReportOptionFound,
      --#                                      Opt_Name,
      --#                                      XMLFound &
      --#         XMLFound                from *,
      --#                                      Opt_Name;
      is
      begin
         --# accept W, 169, CommandLineData.Content.Valid, "Direct updates OK here" &
         --#        W, 169, CommandLineData.Content.XML, "Direct updates OK here";
         if Check_Option_Name (Opt_Name => Opt_Name,
                               Str      => CommandLineData.Option_Xml) then
            CommandLineData.Content.Valid := not (XMLFound or else NoReportOptionFound or else HTMLFound);
            if HTMLFound then
               Possible_Error (E => ES_XMLandHTML);
            elsif XMLFound then
               Possible_Error (E => ES_XML);
            else
               Possible_Error (E => ES_XMLnorep);
            end if;

            XMLFound := True;
            if CommandLineData.Content.Valid then
               CommandLineData.Content.XML := True;
            end if;
         else
            CommandLineData.Content.Valid := False;
            Possible_Error2 (E => ES_InvalidOption,
                             F => Opt_Name);
         end if;
         --# end accept;
      end Process_X;

   begin
      --# accept W, 169, CommandLineData.Content.Valid, "Direct updates OK here";
      loop
         exit when Next_Symbol.Typ /= S_Switch_Character;
         Read_Option
           (Opt_Name       => Opt_Name,
            Opt_Name_OK    => Opt_Name_OK,
            Opt_Val        => Opt_Val,
            Opt_Val_OK     => Opt_Val_OK,
            Command_String => Command_String,
            Next_Symbol    => Next_Symbol);

         if Opt_Name_OK then
            case Ada.Characters.Handling.To_Lower (E_Strings.Get_Element (E_Str => Opt_Name,
                                                                          Pos   => 1)) is
               when 'a' =>
                  Process_A;
               when 'b' =>
                  Process_B;
               when 'c' =>
                  Process_C;
               when 'd' =>
                  Process_D;
               when 'e' =>
                  Process_E;
               when 'f' =>
                  Process_F;
               when 'h' =>
                  Process_H;
               when 'g' =>
                  Process_G;
               when 'i' =>
                  Process_I;
               when 'j' =>
                  Process_J;
               when 'l' =>
                  Process_L;
               when 'm' =>
                  Process_M;
               when 'n' =>
                  Process_N;
               when 'o' =>
                  Process_O;
               when 'p' =>
                  Process_P;
               when 'r' =>
                  Process_R;
               when 's' =>
                  Process_S;
               when 't' =>
                  Process_T;
               when 'v' =>
                  Process_V;
               when 'w' =>
                  Process_W;
               when 'x' =>
                  Process_X;
               when others =>
                  CommandLineData.Content.Valid := False;
                  Possible_Error2 (E => ES_InvalidOption,
                                   F => Opt_Name);
            end case;
         else
            CommandLineData.Content.Valid := False;
            Possible_Error2 (E => ES_InvalidOption,
                             F => Opt_Name);
         end if;
         exit when not CommandLineData.Content.Valid;
      end loop;
      --# end accept;
   end Parse_Command_Options;

   procedure Parse_Command_Line (Command_String : in Command_Strings)
   --# global in out CommandLineData.Content;
   --#        in out SPARK_IO.File_Sys;
   --# derives CommandLineData.Content,
   --#         SPARK_IO.File_Sys       from *,
   --#                                      CommandLineData.Content,
   --#                                      Command_String;
   is
      Next_Symbol          : Symbols;
      Local_Command_String : Command_Strings;

      procedure Parse_Arguments (Command_String : in Command_Strings;
                                 Next_Symbol    : in Symbols)
      --# global in out CommandLineData.Content;
      --#        in out SPARK_IO.File_Sys;
      --# derives CommandLineData.Content,
      --#         SPARK_IO.File_Sys       from *,
      --#                                      CommandLineData.Content,
      --#                                      Command_String,
      --#                                      Next_Symbol;
      --  pre Next_Symbol.Typ in {SString, SEmpty};
      is
         Local_Next_Symbol    : Symbols;
         Local_Command_String : Command_Strings;

         procedure Parse_File_Entry (Command_String : in out Command_Strings;
                                     Next_Symbol    : in out Symbols)
         --# global in out CommandLineData.Content;
         --#        in out SPARK_IO.File_Sys;
         --# derives CommandLineData.Content,
         --#         SPARK_IO.File_Sys       from *,
         --#                                      CommandLineData.Content,
         --#                                      Command_String,
         --#                                      Next_Symbol &
         --#         Command_String,
         --#         Next_Symbol             from Command_String,
         --#                                      Next_Symbol;
         --  pre  Next_Symbol.Typ = SString;
         --  post Next_Symbol.Typ in {SComma, SEmpty};
         is
            File_Name : E_Strings.T;

            procedure Parse_Argument_Option (Command_String : in out Command_Strings;
                                             Next_Symbol    : in out Symbols)
            --# global in out CommandLineData.Content;
            --#        in out SPARK_IO.File_Sys;
            --# derives CommandLineData.Content,
            --#         SPARK_IO.File_Sys       from *,
            --#                                      CommandLineData.Content,
            --#                                      Command_String,
            --#                                      Next_Symbol &
            --#         Command_String,
            --#         Next_Symbol             from Command_String,
            --#                                      Next_Symbol;
            is
               File_Name : E_Strings.T;
               Do_List   : Boolean;
               OK        : Boolean;

               procedure Read_Argument_Option
                 (Listing_File_Name :    out E_Strings.T;
                  Listing           :    out Boolean;
                  OK                :    out Boolean;
                  Command_String    : in out Command_Strings;
                  Next_Symbol       :    out Symbols)
               --# global in     CommandLineData.Content;
               --#        in out SPARK_IO.File_Sys;
               --# derives Command_String,
               --#         Listing,
               --#         Listing_File_Name,
               --#         Next_Symbol,
               --#         OK                from Command_String &
               --#         SPARK_IO.File_Sys from *,
               --#                                CommandLineData.Content,
               --#                                Command_String;
               --  pre  Next_Symbol.Typ = SSlash;
               --  post Next_Symbol.Typ in {SComma, SEmpty};
               is
                  Opt_Name    : E_Strings.T;
                  Opt_Val     : E_Strings.T;
                  Opt_Name_OK : Boolean;
                  Opt_Val_OK  : Boolean;
               begin
                  Listing_File_Name := E_Strings.Empty_String;
                  Listing           := False;

                  Read_Option
                    (Opt_Name       => Opt_Name,
                     Opt_Name_OK    => Opt_Name_OK,
                     Opt_Val        => Opt_Val,
                     Opt_Val_OK     => Opt_Val_OK,
                     Command_String => Command_String,
                     Next_Symbol    => Next_Symbol);
                  case Ada.Characters.Handling.To_Lower (E_Strings.Get_Element (E_Str => Opt_Name,
                                                                                Pos   => 1)) is
                     when 'l' =>
                        if Check_Option_Name (Opt_Name => Opt_Name,
                                              Str      => CommandLineData.Option_Listing_File) then
                           OK                := Opt_Name_OK and then Opt_Val_OK;
                           Listing           := True;
                           Listing_File_Name := Opt_Val;
                        else
                           OK      := False;
                           Listing := False;
                           Output_Error (E => ES_InvalidOption);
                           ScreenEcho.New_Line (1);
                        end if;
                     when 'n' =>
                        if Check_Option_Name (Opt_Name => Opt_Name,
                                              Str      => CommandLineData.Option_No_Listing_File) then
                           OK := Opt_Name_OK and then not Opt_Val_OK;
                        else
                           OK := False;
                           Output_Error (E => ES_InvalidOption);
                           ScreenEcho.New_Line (1);
                        end if;
                        Listing := False;
                     when others =>
                        OK := False;
                  end case;
               end Read_Argument_Option;

            begin
               --# accept W, 169, CommandLineData.Content.Source_File_List, "Direct updates OK here" &
               --#        W, 169, CommandLineData.Content.Valid, "Direct updates OK here";
               if Next_Symbol.Typ = S_Switch_Character then
                  Read_Argument_Option
                    (Listing_File_Name => File_Name,
                     Listing           => Do_List,
                     OK                => OK,
                     Command_String    => Command_String,
                     Next_Symbol       => Next_Symbol);
                  CommandLineData.Content.Source_File_List (CommandLineData.Content.Number_Source).Listing_File_Name := File_Name;
                  CommandLineData.Content.Source_File_List (CommandLineData.Content.Number_Source).Listing           := Do_List;
                  CommandLineData.Content.Valid                                                                      := OK;
                  Possible_Error (E => ES_ListingFile);
               else
                  CommandLineData.Content.Source_File_List (CommandLineData.Content.Number_Source).Listing := True;

                  CommandLineData.Content.Source_File_List (CommandLineData.Content.Number_Source).Listing_File_Name :=
                    FileSystem.Just_File
                    (Fn  => CommandLineData.Content.Source_File_List (CommandLineData.Content.Number_Source).Source_File_Name,
                     Ext => False);
               end if;

               if CommandLineData.Content.Valid
                 and then CommandLineData.Content.Source_File_List (CommandLineData.Content.Number_Source).Listing then

                  File_Name := CommandLineData.Content.Source_File_List (CommandLineData.Content.Number_Source).Listing_File_Name;

                  FileSystem.Check_Listing_Extension
                    (Source_Name => CommandLineData.Content.Source_File_List (CommandLineData.Content.Number_Source).Source_File_Name,
                     Fn          => File_Name,
                     Ext         => CommandLineData.Content.Listing_Extension);

                  CommandLineData.Content.Source_File_List (CommandLineData.Content.Number_Source).Listing_File_Name := File_Name;
               end if;
               --# end accept;
            end Parse_Argument_Option;

         begin
            --# accept W, 169, CommandLineData.Content.Source_File_List, "Direct updates OK here" &
            --#        W, 169, CommandLineData.Content.Valid, "Direct updates OK here" &
            --#        W, 169, CommandLineData.Content.Number_Source, "Direct updates OK here";
            if Next_Symbol.Typ = S_String then
               CommandLineData.Content.Number_Source := CommandLineData.Content.Number_Source + 1;

               File_Name := Next_Symbol.The_String;

               if E_Strings.Get_Element (E_Str => File_Name,
                                         Pos   => 1) = '@' then
                  FileSystem.Check_Extension
                    (Fn  => File_Name,
                     Ext => E_Strings.Copy_String (Str => CommandLineData.Meta_File_Extension));
                  CommandLineData.Content.Source_File_List (CommandLineData.Content.Number_Source).Source_File_Name := File_Name;
                  CommandLineData.Content.Source_File_List (CommandLineData.Content.Number_Source).Listing          := False;
                  Get_Next_Symbol (Command_String => Command_String,
                                   Next_Symbol    => Next_Symbol);
               else
                  FileSystem.Check_Extension (Fn  => File_Name,
                                              Ext => CommandLineData.Content.Source_Extension);
                  CommandLineData.Content.Source_File_List (CommandLineData.Content.Number_Source).Source_File_Name := File_Name;
                  Get_Next_Symbol (Command_String => Command_String,
                                   Next_Symbol    => Next_Symbol);
                  Parse_Argument_Option (Command_String => Command_String,
                                         Next_Symbol    => Next_Symbol);
               end if;
            else
               CommandLineData.Content.Valid := False;
               Possible_Error (E => ES_Source);
            end if;
            --# end accept;
         end Parse_File_Entry;

      begin
         --# accept W, 169, CommandLineData.Content.Valid, "Direct updates OK here" &
         --#        W, 169, CommandLineData.Content.Number_Source, "Direct updates OK here";
         Local_Next_Symbol                     := Next_Symbol;
         Local_Command_String                  := Command_String;
         CommandLineData.Content.Number_Source := 0;
         loop
            Parse_File_Entry (Command_String => Local_Command_String,
                              Next_Symbol    => Local_Next_Symbol);

            exit when Local_Next_Symbol.Typ = S_Empty or else not CommandLineData.Content.Valid;
            if CommandLineData.Content.Number_Source = ExaminerConstants.MaxFilesOnCommandLine then
               CommandLineData.Content.Valid := False;
               Output_Error (E => EW_Too_Many);
               exit;
            end if;

            if FileSystem.Use_Windows_Command_Line and then Local_Next_Symbol.Typ = S_Comma then
               Get_Next_Symbol (Command_String => Local_Command_String,
                                Next_Symbol    => Local_Next_Symbol);
            end if;

         end loop;
         --# end accept;
      end Parse_Arguments;

   begin
      Local_Command_String := Command_String;
      Get_Next_Symbol (Command_String => Local_Command_String,
                       Next_Symbol    => Next_Symbol);
      Parse_Command_Options (Command_String => Local_Command_String,
                             Next_Symbol    => Next_Symbol);
      if CommandLineData.Content.Valid then
         Parse_Arguments (Command_String => Local_Command_String,
                          Next_Symbol    => Next_Symbol);
      end if;
   end Parse_Command_Line;

   ----------------------------------------------------------------------
   -- Does a quick "look ahead" through all the command-line
   -- switches to check for the presence of "-noswitch", "/noswitch"
   -- or any unambiguous abbreviation thereof.
   --
   -- Uses Ada.Command_Line directly, so is hidden from SPARK.
   ----------------------------------------------------------------------
   function Ignore_Default_Switch_File return Boolean
   --# global in SPARK_IO.File_Sys;
   is
      --# hide Ignore_Default_Switch_File;
      Result    : Boolean;
      Arg_Count : constant Natural := Ada.Command_Line.Argument_Count;
   begin
      Result := False;
      for I in Positive range 1 .. Arg_Count loop
         declare
            Arg : constant String := Ada.Command_Line.Argument (I);
         begin
            if Arg'Length >= 5 then
               declare
                  Prefix       : constant Character := Arg (1);
                  Switch       : constant String    := String (Arg (2 .. Arg'Last));
                  Prefix_Legal : Boolean;
               begin
                  Prefix_Legal := (Prefix = '-');

                  if Prefix_Legal
                    and then (Switch = "noswitch"
                                or else Switch = "noswitc"
                                or else Switch = "noswit"
                                or else Switch = "noswi"
                                or else Switch = "nosw") then

                     Result := True;
                     exit;
                  end if;
               end;
            end if;
         end;
      end loop;
      return Result;
   end Ignore_Default_Switch_File;

   procedure Process is
      Command_String : Command_Strings;

      procedure Wff_Command_Line
      --# global in out CommandLineData.Content;
      --#        in out SPARK_IO.File_Sys;
      --# derives CommandLineData.Content,
      --#         SPARK_IO.File_Sys       from CommandLineData.Content,
      --#                                      SPARK_IO.File_Sys;
      is

         procedure Wff_Non_Overlapping
         --# global in out CommandLineData.Content;
         --#        in out SPARK_IO.File_Sys;
         --# derives CommandLineData.Content,
         --#         SPARK_IO.File_Sys       from *,
         --#                                      CommandLineData.Content;
         is

            function Exists_In
              (F          : E_Strings.T;
               L          : CommandLineData.Source_File_Lists;
               Start_Pos  : CommandLineData.Source_File_Positions;
               Finish_Pos : CommandLineData.Source_File_Positions)
              return       Boolean
            is
               Result : Boolean;
            begin
               Result := False;
               for Ix in CommandLineData.Source_File_Positions range Start_Pos .. Finish_Pos loop
                  Result := FileSystem.Same_File (F1 => F,
                                                  F2 => L (Ix).Source_File_Name);
                  exit when Result;
                  if L (Ix).Listing then
                     Result := FileSystem.Same_File (F1 => F,
                                                     F2 => L (Ix).Listing_File_Name);
                  end if;
                  exit when Result;
               end loop;
               return Result;
            end Exists_In;

            procedure Index_Non_Overlapping
            --# global in out CommandLineData.Content;
            --#        in out SPARK_IO.File_Sys;
            --# derives CommandLineData.Content,
            --#         SPARK_IO.File_Sys       from *,
            --#                                      CommandLineData.Content;
            is
            begin
               --# accept W, 169, CommandLineData.Content.Valid, "Direct updates OK here";
               if CommandLineData.Content.Index then
                  CommandLineData.Content.Valid :=
                    not FileSystem.Same_File
                    (F1 => CommandLineData.Content.Index_File_Name,
                     F2 => CommandLineData.Content.Report_File_Name)
                    and then not (CommandLineData.Content.Warning
                                    and then FileSystem.Same_File
                                    (F1 => CommandLineData.Content.Index_File_Name,
                                     F2 => CommandLineData.Content.Warning_File_Name))
                    and then not Exists_In
                    (F          => CommandLineData.Content.Index_File_Name,
                     L          => CommandLineData.Content.Source_File_List,
                     Start_Pos  => 1,
                     Finish_Pos => CommandLineData.Content.Number_Source);
                  Possible_Error2 (E => EW_Overlap,
                                   F => CommandLineData.Content.Index_File_Name);
               end if;
               --# end accept;
            end Index_Non_Overlapping;

            procedure Warning_Non_Overlapping
            --# global in out CommandLineData.Content;
            --#        in out SPARK_IO.File_Sys;
            --# derives CommandLineData.Content,
            --#         SPARK_IO.File_Sys       from *,
            --#                                      CommandLineData.Content;
            is
            begin
               --# accept W, 169, CommandLineData.Content.Valid, "Direct updates OK here";
               if CommandLineData.Content.Warning then
                  CommandLineData.Content.Valid :=
                    not FileSystem.Same_File
                    (F1 => CommandLineData.Content.Warning_File_Name,
                     F2 => CommandLineData.Content.Report_File_Name)
                    and then not Exists_In
                    (F          => CommandLineData.Content.Warning_File_Name,
                     L          => CommandLineData.Content.Source_File_List,
                     Start_Pos  => 1,
                     Finish_Pos => CommandLineData.Content.Number_Source);
                  Possible_Error2 (E => EW_Overlap,
                                   F => CommandLineData.Content.Warning_File_Name);
               end if;
               --# end accept;
            end Warning_Non_Overlapping;

            procedure Report_Non_Overlapping
            --# global in out CommandLineData.Content;
            --#        in out SPARK_IO.File_Sys;
            --# derives CommandLineData.Content,
            --#         SPARK_IO.File_Sys       from *,
            --#                                      CommandLineData.Content;
            is
            begin
               --# accept W, 169, CommandLineData.Content.Valid, "Direct updates OK here";
               if CommandLineData.Content.Report then
                  CommandLineData.Content.Valid :=
                    not Exists_In
                    (F          => CommandLineData.Content.Report_File_Name,
                     L          => CommandLineData.Content.Source_File_List,
                     Start_Pos  => 1,
                     Finish_Pos => CommandLineData.Content.Number_Source);
                  Possible_Error2 (E => EW_Overlap,
                                   F => CommandLineData.Content.Report_File_Name);
               end if;
               --# end accept;
            end Report_Non_Overlapping;

            procedure Source_File_List_Non_Overlapping
            --# global in out CommandLineData.Content;
            --#        in out SPARK_IO.File_Sys;
            --# derives CommandLineData.Content,
            --#         SPARK_IO.File_Sys       from *,
            --#                                      CommandLineData.Content;
            is
            begin
               --# accept W, 169, CommandLineData.Content.Valid, "Direct updates OK here";
               for Ix in CommandLineData.Source_File_Positions range 1 .. (CommandLineData.Content.Number_Source - 1) loop
                  CommandLineData.Content.Valid :=
                    not Exists_In
                    (F          => CommandLineData.Content.Source_File_List (Ix).Source_File_Name,
                     L          => CommandLineData.Content.Source_File_List,
                     Start_Pos  => Ix + 1,
                     Finish_Pos => CommandLineData.Content.Number_Source);
                  Possible_Error2 (E => EW_Overlap,
                                   F => CommandLineData.Content.Source_File_List (Ix).Source_File_Name);
                  exit when not CommandLineData.Content.Valid;
                  if CommandLineData.Content.Source_File_List (Ix).Listing then
                     CommandLineData.Content.Valid :=
                       not FileSystem.Same_File
                       (F1 => CommandLineData.Content.Source_File_List (Ix).Source_File_Name,
                        F2 => CommandLineData.Content.Source_File_List (Ix).Listing_File_Name)
                       and then not Exists_In
                       (F          => CommandLineData.Content.Source_File_List (Ix).Source_File_Name,
                        L          => CommandLineData.Content.Source_File_List,
                        Start_Pos  => Ix + 1,
                        Finish_Pos => CommandLineData.Content.Number_Source);
                     Possible_Error2 (E => EW_Overlap,
                                      F => CommandLineData.Content.Source_File_List (Ix).Source_File_Name);
                  end if;
                  exit when not CommandLineData.Content.Valid;
               end loop;
               if CommandLineData.Content.Valid and then CommandLineData.Content.Number_Source /= 0 then
                  CommandLineData.Content.Valid :=
                    not FileSystem.Same_File
                    (F1 => CommandLineData.Content.Source_File_List (CommandLineData.Content.Number_Source).Source_File_Name,
                     F2 => CommandLineData.Content.Source_File_List (CommandLineData.Content.Number_Source).Listing_File_Name);
                  Possible_Error2
                    (E => EW_Overlap,
                     F => CommandLineData.Content.Source_File_List (CommandLineData.Content.Number_Source).Source_File_Name);
               end if;
               --# end accept;
            end Source_File_List_Non_Overlapping;

         begin
            Index_Non_Overlapping;

            if CommandLineData.Content.Valid then
               Warning_Non_Overlapping;
            end if;

            if CommandLineData.Content.Valid then
               Report_Non_Overlapping;
            end if;

            if CommandLineData.Content.Valid then
               Source_File_List_Non_Overlapping;
            end if;
         end Wff_Non_Overlapping;

         function Strip_Any_At (S : E_Strings.T) return E_Strings.T is
            Result : E_Strings.T;
         begin
            if E_Strings.Get_Element (E_Str => S,
                                      Pos   => 1) = '@' then
               Result := E_Strings.Section (E_Str     => S,
                                            Start_Pos => 2,
                                            Length    => E_Strings.Get_Length (E_Str => S) - 1);
            else
               Result := S;
            end if;
            return Result;
         end Strip_Any_At;

         function Adjust_Filename (S : E_Strings.T) return E_Strings.T
         --# global in CommandLineData.Content;
         is
            R : E_Strings.T;
         begin
            if CommandLineData.Content.Plain_Output then
               R := FileSystem.Just_File (Fn  => S,
                                          Ext => True);
            else
               R := S;
            end if;
            return R;
         end Adjust_Filename;

         procedure Check_Output_Directory_Exists
         --# global in out CommandLineData.Content;
         --#        in out SPARK_IO.File_Sys;
         --# derives CommandLineData.Content,
         --#         SPARK_IO.File_Sys       from CommandLineData.Content,
         --#                                      SPARK_IO.File_Sys;
         is
         begin
            --# accept W, 169, CommandLineData.Content.Valid, "Direct updates OK here" &
            --#        W, 169, CommandLineData.Content, "Direct updates OK here";
            if CommandLineData.Content.Valid and then CommandLineData.Content.Output_Directory then

               if FileSystem.Is_Directory (F => CommandLineData.Content.Output_Directory_Name) then
                  -- Make sure it ends with an EndOfPath separator, so it can be used
                  -- later in a call to FileSystem.InterpretRelative
                  FileSystem.Append_End_Of_Path_If_Needed (D => CommandLineData.Content.Output_Directory_Name);
               else
                  CommandLineData.Content.Valid := False;
                  Possible_Error2
                    (E => ES_OutputDirNotFound,
                     F => Adjust_Filename (S => CommandLineData.Content.Output_Directory_Name));
               end if;

            end if;
            --# end accept;
         end Check_Output_Directory_Exists;

         procedure Check_Language_Profile
         --# global in out CommandLineData.Content;
         --#        in out SPARK_IO.File_Sys;
         --# derives CommandLineData.Content,
         --#         SPARK_IO.File_Sys       from *,
         --#                                      CommandLineData.Content;
         is
         begin
            --# accept W, 169, CommandLineData.Content.Valid, "Direct updates OK here";

            if CommandLineData.Content.Language_Profile = CommandLineData.SPARK83 then
               -- Ravenscar is not permitted in SPARK83 mode
               if CommandLineData.Content.Concurrency_Profile = CommandLineData.Ravenscar then
                  CommandLineData.Content.Valid := False;
                  Possible_Error (E => ES_NoRavenscarInSPARK83);
               end if;
               -- -sparklib is not permitted in SPARK83 mode
               if CommandLineData.Content.SPARK_Lib then
                  CommandLineData.Content.Valid := False;
                  Possible_Error (E => ES_NoSPARKLibInSPARK83);
               end if;
               -- -flow=auto is not permitted in SPARK83 mode
               if CommandLineData.Content.Flow_Option = CommandLineData.Auto_Flow then
                  CommandLineData.Content.Valid := False;
                  Possible_Error (E => ES_NoAutoFlowInSPARK83);
               end if;
            end if;
            --# end accept;
         end Check_Language_Profile;

      begin
         --# accept W, 169, CommandLineData.Content.Valid, "Direct updates OK here";
         -- Check index file readable
         if CommandLineData.Content.Valid and then CommandLineData.Content.Index then
            CommandLineData.Content.Valid := FileSystem.Is_Readable_File (F => CommandLineData.Content.Index_File_Name);
            Possible_Error2 (E => EW_Index,
                             F => Adjust_Filename (S => CommandLineData.Content.Index_File_Name));
         end if;

         --# assert True;

         -- Check warning control file readable
         if CommandLineData.Content.Valid and then CommandLineData.Content.Warning then
            CommandLineData.Content.Valid := FileSystem.Is_Readable_File (F => CommandLineData.Content.Warning_File_Name);
            Possible_Error2 (E => EW_Warning,
                             F => Adjust_Filename (S => CommandLineData.Content.Warning_File_Name));
         end if;

         --# assert True;

         -- Check target data file readable
         if CommandLineData.Content.Valid and then CommandLineData.Content.Target_Data then
            CommandLineData.Content.Valid := FileSystem.Is_Readable_File (F => CommandLineData.Content.Target_Data_File);
            Possible_Error2 (E => EW_Target,
                             F => Adjust_Filename (S => CommandLineData.Content.Target_Data_File));
         end if;

         --# assert True;

         -- Check config file readable
         if CommandLineData.Content.Valid and then CommandLineData.Content.Target_Config then
            CommandLineData.Content.Valid := FileSystem.Is_Readable_File (F => CommandLineData.Content.Target_Config_File);
            Possible_Error2 (E => EW_Config,
                             F => Adjust_Filename (S => CommandLineData.Content.Target_Config_File));
         end if;

         --# assert True;

         -- Check source files readable
         if CommandLineData.Content.Valid then
            for Ix in CommandLineData.Source_File_Positions range 1 .. CommandLineData.Content.Number_Source loop

               CommandLineData.Content.Valid :=
                 FileSystem.Is_Readable_File
                 (F => Strip_Any_At (S => CommandLineData.Content.Source_File_List (Ix).Source_File_Name));

               Possible_Error2
                 (E => EW_Source,
                  F => Adjust_Filename (S => CommandLineData.Content.Source_File_List (Ix).Source_File_Name));
               exit when not CommandLineData.Content.Valid;
            end loop;
         end if;

         --# assert True;

         --  The -makefile option can only be specified in certain
         --  circumstances.
         if CommandLineData.Content.Valid and then CommandLineData.Content.Makefile_Mode then
            CommandLineData.Content.Valid := CommandLineData.Content.Echo and CommandLineData.Content.Brief;

            Possible_Error (ES_Makefile);
         end if;

         --# assert True;

         Check_Output_Directory_Exists;

         Check_Language_Profile;

         if CommandLineData.Content.Valid then
            Wff_Non_Overlapping;
         end if;
         --# end accept;
      end Wff_Command_Line;

      procedure Read_Command_Line (Command_String : out Command_Strings)
      --# global in out CommandLineData.Content;
      --#        in out SPARK_IO.File_Sys;
      --# derives CommandLineData.Content,
      --#         SPARK_IO.File_Sys       from *,
      --#                                      SPARK_IO.File_Sys &
      --#         Command_String          from SPARK_IO.File_Sys;
      is
         Cmd_Line_Found         : Boolean;
         Default_Switches_Found : Boolean;
         Cmd_Line               : E_Strings.T;
         Tmp                    : E_Strings.T;
      begin
         --# accept W, 169, CommandLineData.Content.Default_Switch_File, "Direct updates OK here" &
         --#        W, 169, CommandLineData.Content.Help_Requested, "Direct updates OK here" &
         --#        W, 169, CommandLineData.Content.Plain_Output, "Direct updates OK here";

         Cmd_Line := E_Strings.Empty_String;

         if Ignore_Default_Switch_File then
            CommandLineData.Content.Default_Switch_File := False;
         else
            Read_Default_Switches (Default_Switches_Found => Default_Switches_Found,
                                   Cmd_Line               => Cmd_Line);
            if Default_Switches_Found then
               CommandLineData.Content.Default_Switch_File := True;
            end if;
         end if;

         -- Read commandline and append to the `switch line' (if any)
         FileSystem.Read_Cmd_Line (Cmd_Line_Found => Cmd_Line_Found,
                                   Cmd_Line       => Tmp);
         E_Strings.Append_Examiner_String (E_Str1 => Cmd_Line,
                                           E_Str2 => Tmp);
         Command_String := Command_Strings'(Current_Position => 1,
                                            Contents         => Cmd_Line);

         if not Cmd_Line_Found then
            -- Nothing on command-line so abandon processing and
            -- indicate that the user needs Help!
            CommandLineData.Content.Help_Requested := True;

            -- Override setting of PlainOutput so Help information
            -- always appears with Examiner version number and date.
            CommandLineData.Content.Plain_Output := False;
         end if;
         --# end accept;
      end Read_Command_Line;

   begin -- Process

      Read_Command_Line (Command_String => Command_String);

      -- If there's no command line at all, then we assume Help
      -- is needed, so don't bother to parse the remainder or default switches.
      if not CommandLineData.Content.Help_Requested then
         Parse_Command_Line (Command_String => Command_String);

         if CommandLineData.Content.Valid then
            Wff_Command_Line;
         end if;

      end if;
   end Process;

   procedure Process_Defaults_From_Switch_File is
      Command_String : Command_Strings;

      procedure Read_Switch_File (Command_String : out Command_Strings)
      --# global in out CommandLineData.Content;
      --#        in out SPARK_IO.File_Sys;
      --# derives CommandLineData.Content,
      --#         SPARK_IO.File_Sys       from *,
      --#                                      SPARK_IO.File_Sys &
      --#         Command_String          from SPARK_IO.File_Sys;
      is
         Default_Switches_Found : Boolean;
         Switch_Line            : E_Strings.T;

         Command_String_Content : E_Strings.T;
      begin
         Command_String_Content := E_Strings.Empty_String;

         Read_Default_Switches (Default_Switches_Found => Default_Switches_Found,
                                Cmd_Line               => Switch_Line);

         if Default_Switches_Found then
            --# accept W, 169, CommandLineData.Content.Default_Switch_File, "Direct updates OK here";
            CommandLineData.Content.Default_Switch_File := True;
            --# end accept;
            Command_String_Content := Switch_Line;
         end if;
         Command_String := Command_Strings'(1, Command_String_Content);
      end Read_Switch_File;

      procedure Parse_Switch_File (Command_String : in Command_Strings)
      --# global in out CommandLineData.Content;
      --#        in out SPARK_IO.File_Sys;
      --# derives CommandLineData.Content,
      --#         SPARK_IO.File_Sys       from *,
      --#                                      CommandLineData.Content,
      --#                                      Command_String;
      is
         Next_Symbol          : Symbols;
         Local_Command_String : Command_Strings;
      begin
         Local_Command_String := Command_String;
         Get_Next_Symbol (Command_String => Local_Command_String,
                          Next_Symbol    => Next_Symbol);
         --# accept F, 10, Next_Symbol, "Next_Symbol not used here" &
         --#        F, 10, Local_Command_String, "Local_Command_String not used here";
         Parse_Command_Options (Command_String => Local_Command_String,
                                Next_Symbol    => Next_Symbol);
      end Parse_Switch_File;

   begin -- Process_Defaults_From_Switch_File

      if Ignore_Default_Switch_File then
         null;
      else
         Read_Switch_File (Command_String => Command_String);
         Parse_Switch_File (Command_String => Command_String);
      end if;
   end Process_Defaults_From_Switch_File;

end CommandLineHandler;