+2011-08-01 Robert Dewar <dewar@adacore.com>
+
+ * sem_util.ads, sem_util.adb, sem_ch6.adb (Last_Source_Statement):
+ Replaces Last_Source_Node_In_Sequence.
+ * err_vars.ads (Error_Msg_Lang): 16 is OK, don't need 4K
+ * errout.adb (Set_Error_Msg_Lang): Takes arg with no parens, but stores
+ parens and blank in string (this was inconsistently implemented).
+ * errout.ads
+ (Set_Error_Msg_Lang): Takes arg with no parens, but stores parens and
+ blank in string (this was inconsistently implemented).
+ * gnat1drv.adb
+ (Set_Global_Switches): Set formal mode switches appropriately
+ * opt.ads, opt.adb: Formal mode is now global switches, more consistent
+ * par-prag.adb
+ (Analyze_Pragma, case SPARK_95): Set opt switches appropriately and
+ call Set_Error_Msg_Lang to set "spark" as language name.
+ * par.adb: Remove unnecessary call to set formal language for errout
+ * sem_prag.adb (P_Pragma, case SPARK_95): Set opt switches
+ appropriately and call Set_Error_Msg_Lang to set "spark" as language
+ name.
+ * sem_ch4.adb (Analyze_Concatenation_Operand): remove procedure and
+ calls to it, moved after resolution so that types are known
+ * sem_res.adb (Resolve_Op_Concat): issue an error in formal mode if
+ result of concatenation is not of type String
+ (Resolve_Op_Concat_Arg): issue an error in formal mode if an operand of
+ concatenation is not properly restricted
+ * gnat_rm.texi: Add doc on pragma Spark_95.
+ * gcc-interface/Makefile.in: Remove obsolete target pairs for
+ Interfaces.C.* on VMS. Remove s-parame-vms-restrict.ads.
+ * gcc-interface/Make-lang.in: Update dependencies.
+
2011-08-01 Javier Miranda <miranda@adacore.com>
* sem_disp.adb (Override_Dispatching_Operation): Enforce strictness of
-- Used if current message contains a ~ insertion character to indicate
-- insertion of the string Error_Msg_String (1 .. Error_Msg_Strlen).
- Error_Msg_Lang : String (1 .. 4096);
+ Error_Msg_Lang : String (1 .. 16);
Error_Msg_Langlen : Natural;
-- Used if current message contains a ~~ insertion character to indicate
-- insertion of the string Error_Msg_Lang (1 .. Error_Msg_Langlen).
procedure Set_Error_Msg_Lang (To : String) is
begin
- Error_Msg_Langlen := To'Length;
- Error_Msg_Lang (1 .. Error_Msg_Langlen) := To;
+ Error_Msg_Lang (1) := '(';
+ Error_Msg_Lang (2 .. To'Length + 1) := To;
+ Error_Msg_Lang (To'Length + 2) := ')';
+ Error_Msg_Lang (To'Length + 3) := ' ';
+ Error_Msg_Langlen := To'Length + 3;
end Set_Error_Msg_Lang;
-----------------------
-- on each element of the list, see above).
procedure Set_Error_Msg_Lang (To : String);
- -- Set Error_Msg_Lang and Error_Msg_Langlen used for insertion character ~~
- -- so that Error_Msg_Lang (1 .. Error_Msg_Langlen) = To.
+ -- Set Error_Msg_Lang/Error_Msg_Langlen used for insertion character ~~.
+ -- The argument is just the language name, e.g. "spark". The stored string
+ -- is of the form "(langname) ".
procedure Set_Ignore_Errors (To : Boolean);
-- Following a call to this procedure with To=True, all error calls are
ada/urealp.ads
ada/opt.o : ada/ada.ads ada/a-except.ads ada/a-unccon.ads ada/a-uncdea.ads \
- ada/gnatvsn.ads ada/hostparm.ads ada/opt.ads ada/opt.adb ada/system.ads \
- ada/s-exctab.ads ada/s-os_lib.ads ada/s-parame.ads ada/s-secsta.ads \
- ada/s-soflin.ads ada/s-stache.ads ada/s-stalib.ads ada/s-stoele.ads \
- ada/s-stoele.adb ada/s-string.ads ada/s-traent.ads ada/s-unstyp.ads \
- ada/s-wchcon.ads ada/tree_io.ads ada/types.ads ada/unchconv.ads \
- ada/unchdeal.ads
+ ada/debug.ads ada/gnatvsn.ads ada/hostparm.ads ada/opt.ads ada/opt.adb \
+ ada/system.ads ada/s-exctab.ads ada/s-os_lib.ads ada/s-parame.ads \
+ ada/s-secsta.ads ada/s-soflin.ads ada/s-stache.ads ada/s-stalib.ads \
+ ada/s-stoele.ads ada/s-stoele.adb ada/s-string.ads ada/s-traent.ads \
+ ada/s-unstyp.ads ada/s-wchcon.ads ada/tree_io.ads ada/types.ads \
+ ada/unchconv.ads ada/unchdeal.ads
ada/osint-b.o : ada/ada.ads ada/a-except.ads ada/a-unccon.ads \
ada/a-uncdea.ads ada/alloc.ads ada/debug.ads ada/hostparm.ads \
endif
ifeq ($(strip $(filter-out alpha64 ia64 dec hp vms% openvms% alphavms%,$(targ))),)
- ifeq ($(strip $(filter-out ia64 hp vms% openvms%,$(targ))),)
- LIBGNAT_TARGET_PAIRS_AUX1 = \
- g-enblsp.adb<g-enblsp-vms-ia64.adb \
- g-trasym.adb<g-trasym-vms-ia64.adb \
- s-asthan.adb<s-asthan-vms-ia64.adb \
- s-auxdec.adb<s-auxdec-vms-ia64.adb \
- s-osinte.adb<s-osinte-vms-ia64.adb \
- s-osinte.ads<s-osinte-vms-ia64.ads \
- s-vaflop.adb<s-vaflop-vms-ia64.adb \
- system.ads<system-vms-ia64.ads
-
- LIBGNAT_TARGET_PAIRS_AUX2 = \
- s-parame.ads<s-parame-vms-ia64.ads \
- $(ATOMICS_TARGET_PAIRS)
- else
- ifeq ($(strip $(filter-out alpha64 dec vms% openvms% alphavms%,$(targ))),)
- LIBGNAT_TARGET_PAIRS_AUX1 = \
- g-enblsp.adb<g-enblsp-vms-alpha.adb \
- g-trasym.adb<g-trasym-vms-alpha.adb \
- s-asthan.adb<s-asthan-vms-alpha.adb \
- s-auxdec.adb<s-auxdec-vms-alpha.adb \
- s-osinte.adb<s-osinte-vms.adb \
- s-osinte.ads<s-osinte-vms.ads \
- s-traent.adb<s-traent-vms.adb \
- s-traent.ads<s-traent-vms.ads \
- s-vaflop.adb<s-vaflop-vms-alpha.adb \
- system.ads<system-vms_64.ads
-
- ifeq ($(strip $(filter-out express EXPRESS,$(THREAD_KIND))),)
- LIBGNAT_TARGET_PAIRS_AUX2 = \
- s-parame.ads<s-parame-vms-restrict.ads
- else
- LIBGNAT_TARGET_PAIRS_AUX2 = \
- s-parame.ads<s-parame-vms-alpha.ads \
- $(ATOMICS_TARGET_PAIRS)
- endif
- endif
- endif
-
LIBGNAT_TARGET_PAIRS = \
a-caldel.adb<a-caldel-vms.adb \
a-calend.adb<a-calend-vms.adb \
g-socthi.ads<g-socthi-vms.ads \
g-socthi.adb<g-socthi-vms.adb \
g-stsifd.adb<g-stsifd-sockets.adb \
- i-c.ads<i-c-vms_64.ads \
- i-cstrin.ads<i-cstrin-vms_64.ads \
- i-cstrin.adb<i-cstrin-vms_64.adb \
- i-cpoint.ads<i-cpoint-vms_64.ads \
- i-cpoint.adb<i-cpoint-vms_64.adb \
i-cstrea.adb<i-cstrea-vms.adb \
memtrack.adb<memtrack-vms_64.adb \
s-auxdec.ads<s-auxdec-vms_64.ads \
s-taspri.ads<s-taspri-vms.ads \
s-tpopsp.adb<s-tpopsp-posix-foreign.adb \
s-tpopde.adb<s-tpopde-vms.adb \
- s-tpopde.ads<s-tpopde-vms.ads \
- $(LIBGNAT_TARGET_PAIRS_AUX1) \
- $(LIBGNAT_TARGET_PAIRS_AUX2)
+ s-tpopde.ads<s-tpopde-vms.ads
ifeq ($(strip $(filter-out ia64 hp vms% openvms%,$(targ))),)
+ LIBGNAT_TARGET_PAIRS += \
+ g-enblsp.adb<g-enblsp-vms-ia64.adb \
+ g-trasym.adb<g-trasym-vms-ia64.adb \
+ s-asthan.adb<s-asthan-vms-ia64.adb \
+ s-auxdec.adb<s-auxdec-vms-ia64.adb \
+ s-osinte.adb<s-osinte-vms-ia64.adb \
+ s-osinte.ads<s-osinte-vms-ia64.ads \
+ s-vaflop.adb<s-vaflop-vms-ia64.adb \
+ system.ads<system-vms-ia64.ads \
+ s-parame.ads<s-parame-vms-ia64.ads \
+ $(ATOMICS_TARGET_PAIRS)
+
TOOLS_TARGET_PAIRS= \
mlib-tgt-specific.adb<mlib-tgt-specific-vms-ia64.adb \
symbols.adb<symbols-vms.adb \
symbols-processing.adb<symbols-processing-vms-ia64.adb
else
+ ifeq ($(strip $(filter-out alpha64 dec vms% openvms% alphavms%,$(targ))),)
+ LIBGNAT_TARGET_PAIRS += \
+ g-enblsp.adb<g-enblsp-vms-alpha.adb \
+ g-trasym.adb<g-trasym-vms-alpha.adb \
+ s-asthan.adb<s-asthan-vms-alpha.adb \
+ s-auxdec.adb<s-auxdec-vms-alpha.adb \
+ s-osinte.adb<s-osinte-vms.adb \
+ s-osinte.ads<s-osinte-vms.ads \
+ s-traent.adb<s-traent-vms.adb \
+ s-traent.ads<s-traent-vms.ads \
+ s-vaflop.adb<s-vaflop-vms-alpha.adb \
+ system.ads<system-vms_64.ads \
+ s-parame.ads<s-parame-vms-alpha.ads \
+ $(ATOMICS_TARGET_PAIRS)
+
TOOLS_TARGET_PAIRS= \
mlib-tgt-specific.adb<mlib-tgt-specific-vms-alpha.adb \
symbols.adb<symbols-vms.adb \
symbols-processing.adb<symbols-processing-vms-alpha.adb
+ endif
endif
adamsg.o: adamsg.msg
else
Back_End_Handles_Limited_Types := False;
end if;
+
+ -- Set switches for formal verification modes
+
+ if Debug_Flag_Dot_DD then
+ SPARK_Mode := True;
+ end if;
+
+ if Debug_Flag_Dot_EE then
+ ALFA_Through_SPARK_Mode := True;
+ end if;
+
+ if Debug_Flag_Dot_FF then
+ ALFA_Through_Why_Mode := True;
+ end if;
+
+ ALFA_Mode := ALFA_Through_SPARK_Mode or ALFA_Through_Why_Mode;
+
+ if ALFA_Mode then
+ Set_Error_Msg_Lang ("alfa");
+ Formal_Verification_Mode := True;
+ elsif SPARK_Mode then
+ Set_Error_Msg_Lang ("spark");
+ Formal_Verification_Mode := True;
+ end if;
end Adjust_Global_Switches;
--------------------
* Pragma Source_File_Name::
* Pragma Source_File_Name_Project::
* Pragma Source_Reference::
+* Pragma SPARK_95::
* Pragma Static_Elaboration_Desired::
* Pragma Stream_Convert::
* Pragma Style_Checks::
* Pragma Source_File_Name::
* Pragma Source_File_Name_Project::
* Pragma Source_Reference::
+* Pragma SPARK_95::
* Pragma Static_Elaboration_Desired::
* Pragma Stream_Convert::
* Pragma Style_Checks::
string expression other than a string literal. This is because its value
is needed for error messages issued by all phases of the compiler.
+@node Pragma SPARK_95
+@unnumberedsec Pragma SPARK_95
+@findex SPARK_95
+@noindent
+Syntax:
+@smallexample @c ada
+pragma SPARK_95;
+@end smallexample
+
+@noindent
+A configuration pragma that establishes SPARK 95 mode for the unit to which
+it applies, regardless of the mode set by the command line switches.
+In this mode, the compiler rejects constructs outside the SPARK 95 subset of
+Ada, which provides a useful initial filter for those projects developed in
+SPARK. Syntax and semantic error messages related to SPARK restrictions have
+the form:
+
+@code{(spark) error message}.
+
+This is not a replacement for the semantic checks performed by the
+SPARK Examiner tool, as the compiler only deals currently with code,
+not at all with SPARK annotations, so it may well be the case that code which
+passes the compiler in SPARK 95 mode is rejected by the SPARK Examiner,
+e.g. due to the different visibility rules of the Examiner based on
+@code{inherit} SPARK annotations.
+
@node Pragma Static_Elaboration_Desired
@unnumberedsec Pragma Static_Elaboration_Desired
@findex Static_Elaboration_Desired
-- --
------------------------------------------------------------------------------
-with Debug;
with Gnatvsn; use Gnatvsn;
with System; use System;
with Tree_IO; use Tree_IO;
SU : constant := Storage_Unit;
-- Shorthand for System.Storage_Unit
- ---------------
- -- ALFA_Mode --
- ---------------
-
- function ALFA_Mode return Boolean is
- begin
- return ALFA_Through_SPARK_Mode or else ALFA_Through_Why_Mode;
- end ALFA_Mode;
-
- -----------------------------
- -- ALFA_Through_SPARK_Mode --
- -----------------------------
-
- function ALFA_Through_SPARK_Mode return Boolean is
- begin
- return Debug.Debug_Flag_Dot_EE;
- end ALFA_Through_SPARK_Mode;
-
- ---------------------------
- -- ALFA_Through_Why_Mode --
- ---------------------------
-
- function ALFA_Through_Why_Mode return Boolean is
- begin
- return Debug.Debug_Flag_Dot_FF;
- end ALFA_Through_Why_Mode;
-
- ---------------------
- -- Formal_Language --
- ---------------------
-
- function Formal_Language return String is
- begin
- pragma Assert (Formal_Verification_Mode);
- if ALFA_Mode then
- return "alfa";
- elsif SPARK_Mode then
- return "spark";
- else
- pragma Assert (False);
- return ""; -- unreachable
- end if;
- end Formal_Language;
-
- ------------------------------
- -- Formal_Verification_Mode --
- ------------------------------
-
- function Formal_Verification_Mode return Boolean is
- begin
- return ALFA_Mode or else SPARK_Mode;
- end Formal_Verification_Mode;
-
----------------------------------
-- Register_Opt_Config_Switches --
----------------------------------
Short_Descriptors := Short_Descriptors_Config;
end Set_Opt_Config_Switches;
- ----------------
- -- SPARK_Mode --
- ----------------
-
- function SPARK_Mode return Boolean is
- begin
- -- When dropping the debug flag in favor of a compiler option,
- -- the option should implicitly set the SPARK_Version, so that this test
- -- becomes simply SPARK_Version > SPARK_None.
-
- return Debug.Debug_Flag_Dot_DD or else SPARK_Version > SPARK_None;
- end SPARK_Mode;
-
---------------
-- Tree_Read --
---------------
-- These modes are currently defined through debug flags
- function Formal_Language return String;
- -- Returns "alfa" in ALFA_Mode and "spark" in SPARK_Mode
+ Formal_Verification_Mode : Boolean := False;
+ -- Set True if ALFA_Mode or SPARK_Mode
- function Formal_Verification_Mode return Boolean;
- -- Shorthand for ALFA_Mode or else SPARK_Mode
+ ALFA_Mode : Boolean := False;
+ -- Set True if ALFA_Through_SPARK_Mode or else ALFA_Through_Why_Mode
- function ALFA_Mode return Boolean;
- -- Shorthand for ALFA_Through_SPARK_Mode or else ALFA_Through_Why_Mode
-
- function ALFA_Through_SPARK_Mode return Boolean;
+ ALFA_Through_SPARK_Mode : Boolean := False;
-- Specific compiling mode targeting formal verification through
-- the generation of SPARK code for those parts of the input code that
- -- belong to the ALFA subset of Ada. It is set by the flag -gnatd.E.
+ -- belong to the ALFA subset of Ada. Set by debug flag -gnatd.E.
- function ALFA_Through_Why_Mode return Boolean;
+ ALFA_Through_Why_Mode : Boolean := False;
-- Specific compiling mode targeting formal verification through
-- the generation of Why code for those parts of the input code that
- -- belong to the ALFA subset of Ada. It is set by the flag -gnatd.F.
+ -- belong to the ALFA subset of Ada. Set by debuf flag -gnatd.F.
- function SPARK_Mode return Boolean;
- -- Accept the SPARK subset of Ada only. It is set by the flag -gnatd.D.
+ SPARK_Mode : Boolean := False;
+ -- Reject constructs not allowed by SPARK. Set by flag -gnatd.D or
+ -- by pragma SPARK_95.
private
-- SPARK_95 --
--------------
- -- This pragma must be processed at parse time, since we want to set
- -- the SPARK version properly at parse time to recognize the appropriate
+ -- This pragma must be processed at parse time, since we want to set the
+ -- SPARK version properly at parse time to recognize the appropriate
-- SPARK version syntax.
when Pragma_SPARK_95 =>
SPARK_Version := SPARK_95;
- Set_Error_Msg_Lang ("(" & Formal_Language & ") ");
+ SPARK_Mode := True;
+ Set_Error_Msg_Lang ("spark");
+ Formal_Verification_Mode := True;
-------------------------
-- Style_Checks (GNAT) --
begin
Compiler_State := Parsing;
- if Formal_Verification_Mode then
- Set_Error_Msg_Lang ("(" & Formal_Language & ") ");
- end if;
-
-- Deal with configuration pragmas case first
if Configuration_Pragmas then
-- Local Subprograms --
-----------------------
- procedure Analyze_Concatenation_Operand (N : Node_Id);
- -- Checks that concatenation operands are properly restricted in SPARK or
- -- ALFA: each operand must be either a string literal, a static character
- -- expression, or another concatenation.
-
procedure Analyze_Concatenation_Rest (N : Node_Id);
-- Does the "rest" of the work of Analyze_Concatenation, after the left
-- operand has been analyzed. See Analyze_Concatenation for details.
-- First analyze L ...
Analyze_Expression (L);
- Analyze_Concatenation_Operand (L);
-- ... then walk NN back up until we reach N (where we started), calling
-- Analyze_Concatenation_Rest along the way.
exit when NN = N;
NN := Parent (NN);
end loop;
-
- if Formal_Verification_Mode
- and then Etype (N) /= Standard_String
- then
- Error_Msg_F ("|~~result of concatenation should have type String", N);
- end if;
end Analyze_Concatenation;
- -----------------------------------
- -- Analyze_Concatenation_Operand --
- -----------------------------------
-
- -- Concatenation is restricted in SPARK or ALFA: each operand must be
- -- either a string literal, a static character expression, or another
- -- concatenation. N cannot be a concatenation here as Analyze_Concatenation
- -- and Analyze_Concatenation_Rest call Analyze_Concatenation_Operand
- -- separately on each final operand, past concatenation operations.
-
- procedure Analyze_Concatenation_Operand (N : Node_Id) is
- begin
- if Formal_Verification_Mode then
- if Is_Character_Type (Etype (N)) then
- if not Is_Static_Expression (N) then
- Error_Msg_F ("|~~character operand for concatenation should be "
- & "static", N);
- end if;
- elsif Is_String_Type (Etype (N)) then
- if Nkind (N) /= N_String_Literal then
- Error_Msg_F ("|~~string operand for concatenation should be "
- & "a literal", N);
- end if;
-
- -- Do not issue error on an operand that is neither a character nor
- -- a string, as the error is issued in Analyze_Concatenation_Rest.
-
- end if;
- end if;
- end Analyze_Concatenation_Operand;
-
--------------------------------
-- Analyze_Concatenation_Rest --
--------------------------------
begin
Analyze_Expression (R);
- Analyze_Concatenation_Operand (R);
-- If the entity is present, the node appears in an instance, and
-- denotes a predefined concatenation operation. The resulting type is
if Formal_Verification_Mode then
declare
- Stat : constant Node_Id :=
- Last_Source_Node_In_Sequence (Statements (HSS));
+ Stat : constant Node_Id := Last_Source_Statement (HSS);
begin
if Present (Stat)
and then not Nkind_In (Stat,
Check_Arg_Count (0);
Check_Valid_Configuration_Pragma;
SPARK_Version := SPARK_95;
- Set_Error_Msg_Lang ("(" & Formal_Language & ") ");
+ SPARK_Mode := True;
+ Formal_Verification_Mode := True;
+ Set_Error_Msg_Lang ("spark");
--------------------------------
-- Static_Elaboration_Desired --
exit when NN = N;
NN := Parent (NN);
end loop;
+
+ if Formal_Verification_Mode
+ and then Base_Type (Etype (N)) /= Standard_String
+ then
+ Error_Msg_F ("|~~result of concatenation should have type String", N);
+ end if;
end Resolve_Op_Concat;
---------------------------
Resolve (Arg, Btyp);
end if;
+ -- Concatenation is restricted in SPARK or ALFA: each operand must be
+ -- either a string literal, a static character expression, or another
+ -- concatenation. Arg cannot be a concatenation here as callers of
+ -- Resolve_Op_Concat_Arg call it separately on each final operand, past
+ -- concatenation operations.
+
+ if Formal_Verification_Mode then
+ if Is_Character_Type (Etype (Arg)) then
+ if not Is_Static_Expression (Arg) then
+ Error_Msg_F ("|~~character operand for concatenation should be "
+ & "static", N);
+ end if;
+
+ elsif Is_String_Type (Etype (Arg)) then
+ if Nkind (Arg) /= N_String_Literal then
+ Error_Msg_F ("|~~string operand for concatenation should be "
+ & "a literal", N);
+ end if;
+
+ -- Do not issue error on an operand that is neither a character nor
+ -- a string, as the error is issued in Resolve_Op_Concat.
+
+ else
+ null;
+ end if;
+ end if;
+
Check_Unset_Reference (Arg);
end Resolve_Op_Concat_Arg;
end case;
end Known_To_Be_Assigned;
- ----------------------------------
- -- Last_Source_Node_In_Sequence --
- ----------------------------------
+ ---------------------------
+ -- Last_Source_Statement --
+ ---------------------------
- function Last_Source_Node_In_Sequence (List : List_Id) return Node_Id is
+ function Last_Source_Statement (HSS : Node_Id) return Node_Id is
N : Node_Id;
begin
- N := Last (List);
+ N := Last (Statements (HSS));
while Present (N) loop
exit when Comes_From_Source (N);
- N := Prev (N);
+ Prev (N);
end loop;
return N;
- end Last_Source_Node_In_Sequence;
+ end Last_Source_Statement;
-------------------
-- May_Be_Lvalue --
-- direction. Cases which may possibly be assignments but are not known to
-- be may return True from May_Be_Lvalue, but False from this function.
- function Last_Source_Node_In_Sequence (List : List_Id) return Node_Id;
- -- Returns the last node in List for which Comes_From_Source returns True,
- -- if any, or Empty otherwise.
+ function Last_Source_Statement (HSS : Node_Id) return Node_Id;
+ -- HSS is a handled statement sequence. This function returns the last
+ -- statement in Statements (HSS) that has Comes_From_Source set. If no
+ -- such statement exists, Empty is returned.
function Make_Simple_Return_Statement
(Sloc : Source_Ptr;
OSDN Git Service
