+2013-10-17 Yannick Moy <moy@adacore.com>
+
+ * sem_ch8.adb (Find_Direct_Name): Keep track of assignments for
+ renamings in SPARK mode.
+
+2013-10-17 Yannick Moy <moy@adacore.com>
+
+ * exp_spark.adb (Expand_SPARK): Remove special case for NOT IN
+ operation.
+ * sinfo.ads: Add special comment section to describe SPARK mode
+ effect on tree.
+ * exp_spark.ads: Remove comments, moved to sinfo.ads.
+
+2013-10-17 Yannick Moy <moy@adacore.com>
+
+ * exp_ch3.adb (Expand_Freeze_Class_Wide_Type,
+ Expand_Freeze_Class_Wide_Type, Expand_Freeze_Class_Wide_Type):
+ Remove useless special cases.
+ * exp_ch4.adb (Expand_Allocator_Expression, Expand_N_Allocator,
+ Expand_N_Op_Expon): Remove useless special cases.
+ * exp_ch6.adb (Is_Build_In_Place_Function_Call): Disable build-in-place
+ in SPARK mode by testing Full_Expander_Active instead of
+ Expander_Active.
+ (Make_Build_In_Place_Call_In_Allocator): Remove useless special case.
+ * exp_util.adb (Build_Allocate_Deallocate_Proc): Remove
+ useless special case.
+ * sem_eval.adb (Compile_Time_Known_Value): Remove special handling of
+ deferred constant.
+
+2013-10-17 Yannick Moy <moy@adacore.com>
+
+ * gnat_ugn.texi: Document -gnateT and target file format.
+
+2013-10-17 Vincent Celier <celier@adacore.com>
+
+ * prep.adb (Check_Command_Line_Symbol_Definition): Is_A_String is
+ always False, even when the value starts and ends with double quotes.
+
2013-10-17 Tristan Gingold <gingold@adacore.com>
* a-exexpr-gcc.adb: Synchronize declarations of other/all others.
elsif CodePeer_Mode then
return;
-
- -- Do not create TSS routine Finalize_Address when compiling in SPARK
- -- mode because it is not necessary and results in useless expansion.
-
- elsif SPARK_Mode then
- return;
end if;
-- Create the body of TSS primitive Finalize_Address. This automatically
-- be done before the bodies of all predefined primitives are
-- created. If Def_Id is limited, Stream_Input and Stream_Read
-- may produce build-in-place allocations and for those the
- -- expander needs Finalize_Address. Do not create the body of
- -- Finalize_Address in SPARK mode since it is not needed.
-
- if not SPARK_Mode then
- Make_Finalize_Address_Body (Def_Id);
- end if;
+ -- expander needs Finalize_Address.
+ Make_Finalize_Address_Body (Def_Id);
Predef_List := Predefined_Primitive_Bodies (Def_Id, Renamed_Eq);
Append_Freeze_Actions (Def_Id, Predef_List);
end if;
-- * .NET/JVM - these targets do not support address arithmetic
-- and unchecked conversion, key elements of Finalize_Address.
- -- * SPARK mode - the call is useless and results in unwanted
- -- expansion.
-
-- * CodePeer mode - TSS primitive Finalize_Address is not
-- created in this mode.
if VM_Target = No_VM
- and then not SPARK_Mode
and then not CodePeer_Mode
and then Present (Finalization_Master (PtrT))
and then Present (Temp_Decl)
end if;
-- The finalization master must be inserted and analyzed as part of
- -- the current semantic unit. This form of expansion is not carried
- -- out in SPARK mode because it is useless. Note that the master is
- -- updated when analysis changes current units.
+ -- the current semantic unit. Note that the master is updated when
+ -- analysis changes current units.
- if not SPARK_Mode then
- if Present (Rel_Typ) then
- Set_Finalization_Master (PtrT, Finalization_Master (Rel_Typ));
- else
- Set_Finalization_Master (PtrT, Current_Anonymous_Master);
- end if;
+ if Present (Rel_Typ) then
+ Set_Finalization_Master (PtrT, Finalization_Master (Rel_Typ));
+ else
+ Set_Finalization_Master (PtrT, Current_Anonymous_Master);
end if;
end if;
-- Set_Finalize_Address
-- (<PtrT>FM, <T>FD'Unrestricted_Access);
- -- Do not generate this call in the following cases:
- --
- -- * SPARK mode - the call is useless and results in
- -- unwanted expansion.
- --
- -- * CodePeer mode - TSS primitive Finalize_Address is
- -- not created in this mode.
+ -- Do not generate this call in CodePeer mode, as TSS
+ -- primitive Finalize_Address is not created in this
+ -- mode.
- elsif not (SPARK_Mode or CodePeer_Mode) then
+ elsif not CodePeer_Mode then
Insert_Action (N,
Make_Set_Finalize_Address_Call
(Loc => Loc,
begin
Binary_Op_Validity_Checks (N);
- -- CodePeer and GNATprove want to see the unexpanded N_Op_Expon node
+ -- CodePeer wants to see the unexpanded N_Op_Expon node
- if CodePeer_Mode or SPARK_Mode then
+ if CodePeer_Mode then
return;
end if;
-- disabled (such as with -gnatc) since those would trip over the raise
-- of Program_Error below.
- if not Expander_Active then
+ -- In SPARK mode, build-in-place calls are not expanded, so that we
+ -- may end up with a call that is neither resolved to an entity, nor
+ -- an indirect call.
+
+ if not Full_Expander_Active then
return False;
end if;
return False;
else
- -- In SPARK mode, build-in-place calls are not expanded, so that we
- -- may end up with a call that is neither resolved to an entity, nor
- -- an indirect call.
-
- if SPARK_Mode then
- return False;
-
- elsif Is_Entity_Name (Name (Exp_Node)) then
+ if Is_Entity_Name (Name (Exp_Node)) then
Function_Id := Entity (Name (Exp_Node));
-- In the case of an explicitly dereferenced call, use the subprogram
then
null;
- -- Do not generate the call to Set_Finalize_Address in SPARK mode
- -- because it is not necessary and results in unwanted expansion.
- -- This expansion is also not carried out in CodePeer mode because
- -- Finalize_Address is never built.
+ -- Do not generate the call to Set_Finalize_Address in CodePeer mode
+ -- because Finalize_Address is never built.
- elsif not SPARK_Mode
- and then not CodePeer_Mode
- then
+ elsif not CodePeer_Mode then
Insert_Action (Allocator,
Make_Set_Finalize_Address_Call (Loc,
Typ => Etype (Function_Id),
with Atree; use Atree;
with Einfo; use Einfo;
-with Exp_Ch4; use Exp_Ch4;
with Exp_Dbug; use Exp_Dbug;
with Exp_Util; use Exp_Util;
with Sem_Aux; use Sem_Aux;
N_Identifier =>
Expand_Potential_Renaming (N);
- -- A NOT IN B gets transformed to NOT (A IN B). This is the same
- -- expansion used in the normal case, so shared the code.
-
- when N_Not_In =>
- Expand_N_Not_In (N);
-
when N_Object_Renaming_Declaration =>
Expand_SPARK_N_Object_Renaming_Declaration (N);
-- Expand_SPARK is called directly by Expander.Expand.
--- SPARK expansion has three main objectives:
-
--- 1. Perform limited expansion to explicit some Ada rules and constructs
--- (translate 'Old and 'Result, replace renamings by renamed, insert
--- conversions, expand actuals in calls to introduce temporaries, expand
--- generics instantiations)
-
--- 2. Facilitate treatment for the formal verification back-end (fully
--- qualify names, expand set membership, compute data dependences)
-
--- 3. Avoid the introduction of low-level code that is difficult to analyze
--- formally, as typically done in the full expansion for high-level
--- constructs (tasking, dispatching)
-
--- To fulfill objective 1, Expand_SPARK selectively expands some constructs.
-
--- To fulfill objective 2, the tree after SPARK expansion should be fully
--- analyzed semantically. In particular, all expression must have their proper
--- type, and semantic links should be set between tree nodes (partial to full
--- view, etc.) Some kinds of nodes should be either absent, or can be ignored
--- by the formal verification backend:
-
--- N_Object_Renaming_Declaration: can be ignored safely
--- N_Expression_Function: absent (rewitten)
--- N_Expression_With_Actions: absent (not generated)
-
--- SPARK cross-references are generated from the regular cross-references
--- (used for browsing and code understanding) and additional references
--- collected during semantic analysis, in particular on all
--- dereferences. These SPARK cross-references are output in a separate section
--- of ALI files, as described in spark_xrefs.adb. They are the basis for the
--- computation of data dependences in the formal verification backend. This
--- implies that all cross-references should be generated in this mode, even
--- those that would not make sense from a user point-of-view, and that
--- cross-references that do not lead to data dependences for subprograms can
--- be safely ignored.
-
--- To support the formal verification of units parameterized by data, the
--- value of deferred constants should not be considered as a compile-time
--- constant at program locations where the full view is not visible.
-
--- To fulfill objective 3, Expand_SPARK does not expand features that are not
--- formally analyzed (tasking), or for which formal analysis relies on the
--- source level representation (dispatching, aspects, pragmas). However, these
--- should be semantically analyzed, which sometimes requires the insertion of
--- semantic pre-analysis, for example for subprogram contracts and pragma
--- check/assert.
-
with Types; use Types;
package Exp_SPARK is
-- Start of processing for Build_Allocate_Deallocate_Proc
begin
- -- Do not perform this expansion in SPARK mode because it is not
- -- necessary.
-
- if SPARK_Mode then
- return;
- end if;
-
-- Obtain the attributes of the allocation / deallocation
if Nkind (N) = N_Free_Statement then
@cindex @option{-gnateS} (@command{gcc})
Synonym of @option{-fdump-scos}, kept for backards compatibility.
-@item ^-gnatet^/TARGET_DEPENDENT_INFO^
-@cindex @option{-gnatet} (@command{gcc})
-Generate target dependent information.
+@item ^-gnatet^/TARGET_DEPENDENT_INFO^=@var{path}
+@cindex @option{-gnatet=file} (@command{gcc})
+Generate target dependent information. The format of the output file is
+described in the section about switch @option{-gnateT}.
+
+@item ^-gnateT^/TARGET_DEPENDENT_INFO^=@var{path}
+@cindex @option{-gnateT} (@command{gcc})
+Read target dependent information, such as endianness or sizes and alignments
+of base type. If this switch is passed, the default target dependent
+information of the compiler is replaced by the one read from the input file.
+This is used by tools other than the compiler, e.g. to do
+semantic analysis of programs that will run on some other target than
+the machine on which the tool is run.
+
+The following target dependent values should be defined,
+where @code{Nat} denotes a natural integer value, @code{Pos} denotes a
+positive integer value, and fields marked with a question mark are
+boolean fields, where a value of 0 is False, and a value of 1 is True:
+
+@smallexample
+Bits_BE : Nat; -- Bits stored big-endian?
+Bits_Per_Unit : Pos; -- Bits in a storage unit
+Bits_Per_Word : Pos; -- Bits in a word
+Bytes_BE : Nat; -- Bytes stored big-endian?
+Char_Size : Pos; -- Standard.Character'Size
+Double_Float_Alignment : Nat; -- Alignment of double float
+Double_Scalar_Alignment : Nat; -- Alignment of double length scalar
+Double_Size : Pos; -- Standard.Long_Float'Size
+Float_Size : Pos; -- Standard.Float'Size
+Float_Words_BE : Nat; -- Float words stored big-endian?
+Int_Size : Pos; -- Standard.Integer'Size
+Long_Double_Size : Pos; -- Standard.Long_Long_Float'Size
+Long_Long_Size : Pos; -- Standard.Long_Long_Integer'Size
+Long_Size : Pos; -- Standard.Long_Integer'Size
+Maximum_Alignment : Pos; -- Maximum permitted alignment
+Max_Unaligned_Field : Pos; -- Maximum size for unaligned bit field
+Pointer_Size : Pos; -- System.Address'Size
+Short_Size : Pos; -- Standard.Short_Integer'Size
+Strict_Alignment : Nat; -- Strict alignment?
+System_Allocator_Alignment : Nat; -- Alignment for malloc calls
+Wchar_T_Size : Pos; -- Interfaces.C.wchar_t'Size
+Words_BE : Nat; -- Words stored big-endian?
+@end smallexample
+
+The format of the input file is as follows. First come the values of
+the variables defined above, with one line per value:
+
+@smallexample
+name value
+@end smallexample
+
+where @code{name} is the name of the parameter, spelled out in full,
+and cased as in the above list, and @code{value} is an unsigned decimal
+integer. Two or more blanks separates the name from the value.
+
+All the variables must be present, in alphabetical order (i.e. the
+same order as the list above).
+
+Then there is a blank line to separate the two parts of the file. Then
+come the lines showing the floating-point types to be registered, with
+one line per registered mode:
+
+@smallexample
+name digs float_rep size alignment
+@end smallexample
+
+where @code{name} is the string name of the type (which can have
+single spaces embedded in the name (e.g. long double), @code{digs} is
+the number of digits for the floating-point type, @code{float_rep} is
+the float representation (I/V/A for IEEE-754-Binary, Vax_Native,
+AAMP), @code{size} is the size in bits, @code{alignment} is the
+alignment in bits. The name is followed by at least two blanks, fields
+are separated by at least one blank, and a LF character immediately
+follows the alignment field.
+
+Here is an example of target parametrization file:
+
+@smallexample
+Bits_BE 0
+Bits_Per_Unit 8
+Bits_Per_Word 64
+Bytes_BE 0
+Char_Size 8
+Double_Float_Alignment 0
+Double_Scalar_Alignment 0
+Double_Size 64
+Float_Size 32
+Float_Words_BE 0
+Int_Size 64
+Long_Double_Size 128
+Long_Long_Size 64
+Long_Size 64
+Maximum_Alignment 16
+Max_Unaligned_Field 64
+Pointer_Size 64
+Short_Size 16
+Strict_Alignment 0
+System_Allocator_Alignment 16
+Wchar_T_Size 32
+Words_BE 0
+
+float 15 I 64 64
+double 15 I 64 64
+long double 18 I 80 128
+TF 33 I 128 128
+@end smallexample
@item -gnateu
@cindex @option{-gnateu} (@command{gcc})
-- Check the syntax of the value
- if Definition (Index + 1) = '"'
- and then Definition (Definition'Last) = '"'
+ if Definition (Index + 1) /= '"'
+ or else Definition (Definition'Last) /= '"'
then
- Result.Is_A_String := True;
-
- else
- Result.Is_A_String := False;
-
for J in Index + 1 .. Definition'Last loop
case Definition (J) is
when '_' | '.' | '0' .. '9' | 'a' .. 'z' | 'A' .. 'Z' =>
-- And put the value in the result
+ Result.Is_A_String := False;
+ -- Even if the value is a string, we still set Is_A_String to False,
+ -- to avoid adding additional quotes in the preprocessed sources when
+ -- replacing $<symbol>.
+
Start_String;
Store_String_Chars (Definition (Index + 1 .. Definition'Last));
Result.Value := End_String;
-- Entity is unambiguous, indicate that it is referenced here
-- For a renaming of an object, always generate simple reference,
- -- we don't try to keep track of assignments in this case.
+ -- we don't try to keep track of assignments in this case, except
+ -- in SPARK mode where renamings are traversed for generating
+ -- local effects of subprograms.
- if Is_Object (E) and then Present (Renamed_Object (E)) then
+ if Is_Object (E)
+ and then Present (Renamed_Object (E))
+ and then not SPARK_Mode
+ then
Generate_Reference (E, N);
-- If the renamed entity is a private protected component,
if Ekind (E) = E_Enumeration_Literal then
return True;
- -- In SPARK mode, the value of deferred constants should be
- -- ignored outside the scope of their full view. This allows
- -- parameterized formal verification, in which a deferred constant
- -- value if not known from client units.
-
- elsif Ekind (E) = E_Constant
- and then not (SPARK_Mode
- and then Present (Full_View (E))
- and then not In_Open_Scopes (Scope (E)))
- then
+ elsif Ekind (E) = E_Constant then
V := Constant_Value (E);
return Present (V) and then Compile_Time_Known_Value (V);
end if;
-- simply ignore these nodes, since they are not relevant to the task
-- of back annotating representation information.
+ ----------------
+ -- SPARK Mode --
+ ----------------
+
+ -- When a file is compiled in SPARK mode (-gnatd.F), a very light expansion
+ -- is performed and the analysis must generate a tree in a form that meets
+ -- additional requirements.
+
+ -- The SPARK expansion does two transformations of the tree, that cannot be
+ -- postponed after the frontend semantic analysis:
+
+ -- 1. Replace renamings by renamed (object/subprogram). This requires
+ -- introducing temporaries at the point of the renaming, which must be
+ -- properly analyzed.
+
+ -- 2. Fully qualify entity names. This is needed to generate suitable
+ -- local effects/call-graphs in ALI files, with the completely
+ -- qualified names (in particular the suffix to distinguish homonyms).
+
+ -- The tree after SPARK expansion should be fully analyzed semantically,
+ -- which sometimes requires the insertion of semantic pre-analysis, for
+ -- example for subprogram contracts and pragma check/assert. In particular,
+ -- all expression must have their proper type, and semantic links should be
+ -- set between tree nodes (partial to full view, etc.) Some kinds of nodes
+ -- should be either absent, or can be ignored by the formal verification
+ -- backend:
+
+ -- N_Object_Renaming_Declaration: can be ignored safely
+ -- N_Expression_Function: absent (rewitten)
+ -- N_Expression_With_Actions: absent (not generated)
+
+ -- SPARK cross-references are generated from the regular cross-references
+ -- (used for browsing and code understanding) and additional references
+ -- collected during semantic analysis, in particular on all dereferences.
+ -- These SPARK cross-references are output in a separate section of ALI
+ -- files, as described in spark_xrefs.adb. They are the basis for the
+ -- computation of data dependences in the formal verification backend.
+ -- This implies that all cross-references should be generated in this mode,
+ -- even those that would not make sense from a user point-of-view, and that
+ -- cross-references that do not lead to data dependences for subprograms
+ -- can be safely ignored.
+
------------------------
-- Common Flag Fields --
------------------------
projects / platform / upstream / gcc.git / commitdiff