in the compiler sources for details in files @file{scos.ads} and
@file{scos.adb}.
+@item -fdump-xref
+@cindex @option{-fdump-xref} (@command{gcc})
+Generates cross reference information in GLI files for C and C++ sources.
+The GLI files have the same syntax as the ALI files for Ada, and can be used
+for source navigation in IDEs and on the command line using e.g. gnatxref
+and the @option{--ext=gli} switch.
+
@item -flto@r{[}=n@r{]}
@cindex @option{-flto} (@command{gcc})
Enables Link Time Optimization. This switch must be used in conjunction
@item --ext=@var{extension}
@cindex @option{--ext} (@command{gnatxref})
Specify an alternate ali file extension. The default is @code{ali} and other
-extensions (e.g. @code{sli} for SPARK library files) may be specified via this
-switch. Note that if this switch overrides the default, which means that only
-the new extension will be considered.
+extensions (e.g. @code{gli} for C/C++ sources when using @option{-fdump-xref})
+may be specified via this switch. Note that if this switch overrides the
+default, which means that only the new extension will be considered.
@item --RTS=@var{rts-path}
@cindex @option{--RTS} (@command{gnatxref})
@item --ext=@var{extension}
@cindex @option{--ext} (@command{gnatfind})
Specify an alternate ali file extension. The default is @code{ali} and other
-extensions (e.g. @code{sli} for SPARK library files) may be specified via this
-switch. Note that if this switch overrides the default, which means that only
-the new extension will be considered.
+extensions (e.g. @code{gli} for C/C++ sources when using @option{-fdump-xref})
+may be specified via this switch. Note that if this switch overrides the
+default, which means that only the new extension will be considered.
@item --RTS=@var{rts-path}
@cindex @option{--RTS} (@command{gnatfind})
-- pragma Abstract_State (ABSTRACT_STATE_LIST)
-- ABSTRACT_STATE_LIST ::=
- -- null
- -- | STATE_NAME_WITH_OPTIONS
+ -- null
+ -- | STATE_NAME_WITH_OPTIONS
-- | (STATE_NAME_WITH_OPTIONS {, STATE_NAME_WITH_OPTIONS} )
-- STATE_NAME_WITH_OPTIONS ::=
- -- STATE_NAME
+ -- STATE_NAME
-- | (STATE_NAME with OPTION_LIST)
-- OPTION_LIST ::= OPTION {, OPTION}
-- | External [=> EXTERNAL_PROPERTY_LIST]
-- EXTERNAL_PROPERTY_LIST ::=
- -- EXTERNAL_PROPERTY
+ -- EXTERNAL_PROPERTY
-- | (EXTERNAL_PROPERTY {, EXTERNAL_PROPERTY} )
-- EXTERNAL_PROPERTY ::=
-- | Async_Writers [=> boolean_EXPRESSION]
-- | Effective_Reads [=> boolean_EXPRESSION]
-- | Effective_Writes [=> boolean_EXPRESSION]
+ -- others => boolean_EXPRESSION
-- STATE_NAME ::= defining_identifier
ER_Seen : Boolean := False;
EW_Seen : Boolean := False;
External_Seen : Boolean := False;
+ Others_Seen : Boolean := False;
Part_Of_Seen : Boolean := False;
-- Flags used to store the static value of all external states'
Expr_Val : Boolean;
begin
- -- The external property must be one of the predefined four
- -- reader/writer choices.
-
- if Nkind (Prop) /= N_Identifier
- or else not Nam_In (Chars (Prop), Name_Async_Readers,
- Name_Async_Writers,
- Name_Effective_Reads,
- Name_Effective_Writes)
+ -- Check the placement of "others" (if available)
+
+ if Nkind (Prop) = N_Others_Choice then
+ if Others_Seen then
+ Error_Msg_N
+ ("only one others choice allowed in option External",
+ Prop);
+ else
+ Others_Seen := True;
+ end if;
+
+ elsif Others_Seen then
+ Error_Msg_N
+ ("others must be the last property in option External",
+ Prop);
+
+ -- The only remaining legal options are the four predefined
+ -- external properties.
+
+ elsif Nkind (Prop) = N_Identifier
+ and then Nam_In (Chars (Prop), Name_Async_Readers,
+ Name_Async_Writers,
+ Name_Effective_Reads,
+ Name_Effective_Writes)
then
+ null;
+
+ -- Otherwise the construct is not a valid property
+
+ else
Error_Msg_N ("invalid external state property", Prop);
return;
end if;
Expr_Val := True;
end if;
- if Chars (Prop) = Name_Async_Readers then
- Check_Duplicate_Option (Prop, AR_Seen);
- AR_Val := Expr_Val;
+ -- Named properties
- elsif Chars (Prop) = Name_Async_Writers then
- Check_Duplicate_Option (Prop, AW_Seen);
- AW_Val := Expr_Val;
+ if Nkind (Prop) = N_Identifier then
+ if Chars (Prop) = Name_Async_Readers then
+ Check_Duplicate_Option (Prop, AR_Seen);
+ AR_Val := Expr_Val;
- elsif Chars (Prop) = Name_Effective_Reads then
- Check_Duplicate_Option (Prop, ER_Seen);
- ER_Val := Expr_Val;
+ elsif Chars (Prop) = Name_Async_Writers then
+ Check_Duplicate_Option (Prop, AW_Seen);
+ AW_Val := Expr_Val;
+
+ elsif Chars (Prop) = Name_Effective_Reads then
+ Check_Duplicate_Option (Prop, ER_Seen);
+ ER_Val := Expr_Val;
+
+ else
+ Check_Duplicate_Option (Prop, EW_Seen);
+ EW_Val := Expr_Val;
+ end if;
+
+ -- The handling of property "others" must take into account
+ -- all other named properties that have been encountered so
+ -- far. Only those that have not been seen are affected by
+ -- "others".
else
- Check_Duplicate_Option (Prop, EW_Seen);
- EW_Val := Expr_Val;
+ if not AR_Seen then
+ AR_Val := Expr_Val;
+ end if;
+
+ if not AW_Seen then
+ AW_Val := Expr_Val;
+ end if;
+
+ if not ER_Seen then
+ ER_Val := Expr_Val;
+ end if;
+
+ if not EW_Seen then
+ EW_Val := Expr_Val;
+ end if;
end if;
end Analyze_External_Property;