+2011-08-04 Eric Botcazou <ebotcazou@adacore.com>
+
+ * bindgen.adb: Add comments.
+
+2011-08-04 Yannick Moy <moy@adacore.com>
+
+ * einfo.adb, einfo.ads: Free Flag254 and make Formal_Proof_On a
+ synthesized flag.
+ * sem_prag.adb (Analyze_Pragma): record the pragma Annotate
+ (Formal_Proof, On/Off) in the Rep_Item list of the current subprogram.
+
+2011-08-04 Robert Dewar <dewar@adacore.com>
+
+ * exp_ch7.adb, exp_ch6.adb, sem_ch3.adb, layout.adb, sem_ch5.adb,
+ osint-c.ads, sem_util.ads, gnat1drv.adb, targparm.ads, sem_ch6.adb,
+ sem_ch13.adb, s-pooloc.adb: Minor reformatting.
+
2011-08-04 Thomas Quinot <quinot@adacore.com>
* s-pooloc.ads, s-pooglo.ads: Minor reformatting
WBI ("");
end if;
+ -- The B.1 (39) implementation advice says that the adainit/adafinal
+ -- routines should be idempotent. Generate a flag to ensure that.
+
WBI (" Is_Elaborated : Boolean := False;");
WBI ("");
WBI ("");
end if;
+ -- The B.1 (39) implementation advice says that the adainit/adafinal
+ -- routines should be idempotent. Generate a flag to ensure that.
+
WBI ("static char is_elaborated = 0;");
WBI ("");
-- Body_Is_In_ALFA Flag251
-- Is_Processed_Transient Flag252
-- Is_Postcondition_Proc Flag253
- -- Formal_Proof_On Flag254
+ -- (unused) Flag254
-----------------------
-- Local subprograms --
return Node6 (Id);
end First_Rep_Item;
- function Formal_Proof_On (Id : E) return B is
- begin
- pragma Assert (Is_Subprogram (Id) or else Is_Generic_Subprogram (Id));
- return Flag254 (Id);
- end Formal_Proof_On;
-
function Freeze_Node (Id : E) return N is
begin
return Node7 (Id);
Set_Uint10 (Id, UI_From_Int (F'Pos (V)));
end Set_Float_Rep;
- procedure Set_Formal_Proof_On (Id : E; V : B := True) is
- begin
- pragma Assert (Is_Subprogram (Id) or else Is_Generic_Subprogram (Id));
- Set_Flag254 (Id, V);
- end Set_Formal_Proof_On;
-
procedure Set_Freeze_Node (Id : E; V : N) is
begin
Set_Node7 (Id, V);
end if;
end First_Formal_With_Extras;
+ ---------------------
+ -- Formal_Proof_On --
+ ---------------------
+
+ function Formal_Proof_On (Id : E) return B is
+ N : Node_Id;
+ Arg1 : Node_Id;
+ Arg2 : Node_Id;
+
+ begin
+ pragma Assert (Is_Subprogram (Id) or else Is_Generic_Subprogram (Id));
+
+ N := First_Rep_Item (Id);
+ while Present (N) loop
+ if Nkind (N) = N_Pragma
+ and then Get_Pragma_Id (Pragma_Name (N)) = Pragma_Annotate
+ and then Present (Pragma_Argument_Associations (N))
+ and then List_Length (Pragma_Argument_Associations (N)) = 2
+ then
+ Arg1 := First (Pragma_Argument_Associations (N));
+ Arg2 := Next (Arg1);
+
+ if Chars (Get_Pragma_Arg (Arg1)) = Name_Formal_Proof
+ and then Chars (Get_Pragma_Arg (Arg2)) = Name_On
+ then
+ return True;
+ end if;
+ end if;
+
+ Next_Rep_Item (N);
+ end loop;
+
+ return False;
+ end Formal_Proof_On;
+
-------------------------------------
-- Get_Attribute_Definition_Clause --
-------------------------------------
W ("Entry_Accepted", Flag152 (Id));
W ("Can_Use_Internal_Rep", Flag229 (Id));
W ("Finalize_Storage_Only", Flag158 (Id));
- W ("Formal_Proof_On", Flag254 (Id));
W ("From_With_Type", Flag159 (Id));
W ("Has_Aliased_Components", Flag135 (Id));
W ("Has_Alignment_Clause", Flag46 (Id));
-- Float_Rep_Kind. Together with the Digits_Value uniquely defines
-- the floating-point representation to be used.
--- Formal_Proof_On (Flag254)
--- Present in subprogram and generic subprogram entities. Set on for
--- subprograms whose body contains an Annotate pragma which forces formal
--- proof on this body.
+-- Formal_Proof_On (synthesized)
+-- Applies to subprogram and generic subprogram entities. Returns True if
+-- the Rep_Item chain for the subprogram has a pragma Annotate which
+-- forces formal proof on the subprogram's body.
-- Freeze_Node (Node7)
-- Present in all entities. If there is an associated freeze node for
-- Delay_Cleanups (Flag114)
-- Delay_Subprogram_Descriptors (Flag50)
-- Discard_Names (Flag88)
- -- Formal_Proof_On (Flag254)
-- Has_Completion (Flag26)
-- Has_Controlling_Result (Flag98)
-- Has_Invariants (Flag232)
-- Is_Primitive (Flag218)
-- Is_Thunk (Flag225)
-- Default_Expressions_Processed (Flag108)
- -- Formal_Proof_On (Flag254)
-- Aren't there more flags and fields? seems like this list should be
-- more similar to the E_Function list, which is much longer ???
-- Delay_Cleanups (Flag114)
-- Delay_Subprogram_Descriptors (Flag50)
-- Discard_Names (Flag88)
- -- Formal_Proof_On (Flag254)
-- Has_Completion (Flag26)
-- Has_Invariants (Flag232)
-- Has_Master_Entity (Flag21)
function First_Private_Entity (Id : E) return E;
function First_Rep_Item (Id : E) return N;
function Float_Rep (Id : E) return F;
- function Formal_Proof_On (Id : E) return B;
function Freeze_Node (Id : E) return N;
function From_With_Type (Id : E) return B;
function Full_View (Id : E) return E;
function First_Component_Or_Discriminant (Id : E) return E;
function First_Formal (Id : E) return E;
function First_Formal_With_Extras (Id : E) return E;
+ function Formal_Proof_On (Id : E) return B;
function Has_Attach_Handler (Id : E) return B;
function Has_Entries (Id : E) return B;
function Has_Foreign_Convention (Id : E) return B;
procedure Set_First_Private_Entity (Id : E; V : E);
procedure Set_First_Rep_Item (Id : E; V : N);
procedure Set_Float_Rep (Id : E; V : F);
- procedure Set_Formal_Proof_On (Id : E; V : B := True);
procedure Set_Freeze_Node (Id : E; V : N);
procedure Set_From_With_Type (Id : E; V : B := True);
procedure Set_Full_View (Id : E; V : E);
pragma Inline (First_Optional_Parameter);
pragma Inline (First_Private_Entity);
pragma Inline (First_Rep_Item);
- pragma Inline (Formal_Proof_On);
pragma Inline (Freeze_Node);
pragma Inline (From_With_Type);
pragma Inline (Full_View);
pragma Inline (Set_First_Optional_Parameter);
pragma Inline (Set_First_Private_Entity);
pragma Inline (Set_First_Rep_Item);
- pragma Inline (Set_Formal_Proof_On);
pragma Inline (Set_Freeze_Node);
pragma Inline (Set_From_With_Type);
pragma Inline (Set_Full_View);
null;
-- Do not generate the call to Make_Set_Finalize_Address_Ptr for
- -- CodePeer compilations becase Finalize_Address is never built.
+ -- CodePeer compilations because Finalize_Address is never built.
elsif not CodePeer_Mode then
Insert_Action (Allocator,
-- order to detect this scenario, save the state of entry into the
-- finalization code.
+ -- No need to do this for VM case, since VM version of Ada.Exceptions
+ -- does not include routine Raise_From_Controlled_Operation which is the
+ -- the sole user of flag Abort.
+
if Abort_Allowed
and then VM_Target = No_VM
then
Attribute_Name => Name_Identity)));
end;
- -- No abort or .NET/JVM. The VM version of Ada.Exceptions does not
- -- include routine Raise_From_Controlled_Operation which is the sole
- -- user of flag Abort.
+ -- No abort or .NET/JVM
else
A_Expr := New_Reference_To (Standard_False, Loc);
Utyp := Underlying_Type (Root_Type (Base_Type (Typ)));
Ref := Unchecked_Convert_To (Utyp, Ref);
+ -- The following is to prevent problems with UC see 1.156 RH ???
+
Set_Assignment_OK (Ref);
- -- To prevent problems with UC see 1.156 RH ???
end if;
-- If the underlying_type is a subtype, then we are dealing with the
Write_ALI (Object => (Back_End_Mode = Generate_Object));
if not Compilation_Errors then
+
-- In case of ada backends, we need to make sure that the generated
- -- object file has a timestamp greater than the ALI file.
- -- We do this to make gnatmake happy when checking the ALI and obj
- -- timestamps, where it expects the object file being written after
- -- the ali file.
+ -- object file has a timestamp greater than the ALI file. We do this
+ -- to make gnatmake happy when checking the ALI and obj timestamps,
+ -- where it expects the object file being written after the ali file.
+
-- Gnatmake's assumption is true for gcc platforms where the gcc
-- wrapper needs to call the assembler after calling gnat1, but is
-- not true for ada backends, where the object files are created
-- directly by gnat1 (so are created before the ali file).
+
Back_End.Gen_Or_Update_Object_File;
end if;
end;
end if;
- -- Now set the dynamic size (the Value_Size is always the same
- -- as the Object_Size for arrays whose length is dynamic).
+ -- Now set the dynamic size (the Value_Size is always the same as the
+ -- Object_Size for arrays whose length is dynamic).
-- ??? If Size.Status = Dynamic, Vtyp will not have been set.
-- The added initialization sets it to Empty now, but is this
Lo : Node_Id;
Hi : Node_Id;
Res : Boolean := False;
+
begin
-- Loop to process array indexes
Hi := Type_High_Bound (Ityp);
if (Nkind (Lo) = N_Identifier
- and then Ekind (Entity (Lo)) = E_Discriminant)
- or else (Nkind (Hi) = N_Identifier
- and then Ekind (Entity (Hi)) = E_Discriminant)
+ and then Ekind (Entity (Lo)) = E_Discriminant)
+ or else
+ (Nkind (Hi) = N_Identifier
+ and then Ekind (Entity (Hi)) = E_Discriminant)
then
Res := True;
end if;
-- above for a discussion of how library information files are stored.
procedure Set_Library_Info_Name;
- -- Sets a default ALI file name from the main compiler source name.
- -- This is used by Create_Output_Library_Info, and by the version of
- -- Read_Library_Info that takes a default file name. The name is in
- -- Name_Buffer (with length in Name_Len) on return from the call.
+ -- Sets a default ALI file name from the main compiler source name. Used by
+ -- Create_Output_Library_Info, and by the version of Read_Library_Info that
+ -- takes a default file name. The name is in Name_Buffer (with length in
+ -- Name_Len) on return from the call.
procedure Create_Output_Library_Info;
-- Creates the output library information file for the source file which
if Prev (Allocated).all = Null_Address then
Pool.First := Next (Allocated).all;
+ -- Comment needed
+
if Pool.First /= Null_Address then
Prev (Pool.First).all := Null_Address;
end if;
Error_Msg_Uint_1 := SSU;
Error_Msg_F
("\and is not a multiple of Storage_Unit (^) "
- & "('R'M 13.4.1(10))",
+ & "(RM 13.4.1(10))",
First_Bit (CC));
else
Error_Msg_Uint_1 := Fbit;
Error_Msg_F
("\and first bit (^) is non-zero "
- & "('R'M 13.4.1(10))",
+ & "(RM 13.4.1(10))",
First_Bit (CC));
end if;
end if;
elsif No (Real_Range_Specification (Def)) then
Error_Msg_Uint_1 := Max_Digs_Val;
Error_Msg_N ("types with more than ^ digits need range spec "
- & "('R'M 3.5.7(6))", Digs);
+ & "(RM 3.5.7(6))", Digs);
end if;
end;
end if;
-- elements of a container using the OF syntax.
if Is_In_ALFA (Etype (Id))
- and then (No (Iterator_Specification (N))
- or else not Of_Present (Iterator_Specification (N)))
+ and then
+ (No (Iterator_Specification (N))
+ or else not Of_Present (Iterator_Specification (N)))
then
Set_Is_In_ALFA (Id);
end if;
Obj_Decl, Typ);
Error_Msg_N
("\an equality operator cannot be declared after this "
- & "point ('R'M 4.5.2 (9.8)) (Ada 2012))?", Obj_Decl);
+ & "point (RM 4.5.2 (9.8)) (Ada 2012))?", Obj_Decl);
exit;
end if;
-- external tool and a tool-specific function. These arguments are
-- not analyzed.
- when Pragma_Annotate => Annotate : begin
+ -- The following is a special form used in conjunction with the
+ -- ALFA subset of Ada:
+
+ -- pragma Annotate (Formal_Proof, MODE);
+ -- MODE ::= On | Off
+
+ -- This pragma either forces (mode On) or disables (mode Off)
+ -- formal verification of the subprogram in which it is added. When
+ -- formal verification is forced, all violations of the the ALFA
+ -- subset of Ada present in the subprogram are reported as errors
+ -- to the user.
+
+ when Pragma_Annotate => Annotate : declare
+ Arg : Node_Id;
+ Exp : Node_Id;
+
+ begin
GNAT_Pragma;
Check_At_Least_N_Arguments (1);
Check_Arg_Is_Identifier (Arg1);
Check_No_Identifiers;
Store_Note (N);
- declare
- Arg : Node_Id;
- Exp : Node_Id;
+ -- Special processing for Formal_Proof case
- begin
- if Chars (Get_Pragma_Arg (Arg1)) = Name_Formal_Proof then
- if No (Arg2) then
- Error_Pragma_Arg
- ("missing second argument for pragma%", Arg1);
- end if;
+ if Chars (Get_Pragma_Arg (Arg1)) = Name_Formal_Proof then
+ if No (Arg2) then
+ Error_Pragma_Arg
+ ("missing second argument for pragma%", Arg1);
+ end if;
- Check_Arg_Is_Identifier (Arg2);
- Check_Arg_Count (2);
+ Check_Arg_Count (2);
+ Check_Arg_Is_One_Of (Arg2, Name_On, Name_Off);
- if Chars (Get_Pragma_Arg (Arg2)) /= Name_On
- and then Chars (Get_Pragma_Arg (Arg2)) /= Name_Off
+ declare
+ Cur_Subp : constant Entity_Id := Current_Subprogram;
+
+ begin
+ if Present (Cur_Subp)
+ and then (Is_Subprogram (Cur_Subp)
+ or else Is_Generic_Subprogram (Cur_Subp))
then
- Error_Pragma_Arg
- ("wrong second argument for pragma%", Arg2);
- end if;
+ -- Notify user if some ALFA violation occurred before
+ -- this point in Cur_Subp. These violations are not
+ -- precisly located, but this is better than ignoring
+ -- these violations.
+
+ if Chars (Get_Pragma_Arg (Arg2)) = Name_On
+ and then (not Is_In_ALFA (Cur_Subp)
+ or else not Body_Is_In_ALFA (Cur_Subp))
+ then
+ Error_Pragma
+ ("pragma% is placed after violation"
+ & " of 'A'L'F'A");
+ end if;
- if Chars (Get_Pragma_Arg (Arg2)) = Name_On then
- declare
- Cur_Subp : constant Entity_Id := Current_Subprogram;
+ -- We treat this as a Rep_Item to record it on the rep
+ -- item chain for easy location later on.
- begin
- if Present (Cur_Subp)
- and then (Is_Subprogram (Cur_Subp)
- or else Is_Generic_Subprogram (Cur_Subp))
- then
- -- Notify user if some ALFA violation occurred
- -- before this point in Cur_Subp. These violations
- -- are not precisly located, but this is better
- -- than ignoring them.
+ Record_Rep_Item (Cur_Subp, N);
- if not Is_In_ALFA (Cur_Subp)
- or else not Body_Is_In_ALFA (Cur_Subp)
- then
- Error_Pragma
- ("pragma% is placed after violation"
- & " of 'A'L'F'A");
- end if;
+ else
+ Error_Pragma ("wrong placement for pragma%");
+ end if;
+ end;
- Set_Formal_Proof_On (Cur_Subp);
+ -- Second parameter is optional, it is never analyzed
- else
- Error_Pragma ("wrong placement for pragma%");
- end if;
- end;
- end if;
- end if;
+ elsif No (Arg2) then
+ null;
- -- Second unanalyzed parameter is optional
+ -- Here if we have a second parameter
- if No (Arg2) then
- null;
- else
- Arg := Next (Arg2);
- while Present (Arg) loop
- Exp := Get_Pragma_Arg (Arg);
- Analyze (Exp);
+ else
+ -- Second parameter must be identifier
- if Is_Entity_Name (Exp) then
- null;
+ Check_Arg_Is_Identifier (Arg2);
- -- For string literals, we assume Standard_String as the
- -- type, unless the string contains wide or wide_wide
- -- characters.
+ -- Process remaining parameters if any
- elsif Nkind (Exp) = N_String_Literal then
- if Has_Wide_Wide_Character (Exp) then
- Resolve (Exp, Standard_Wide_Wide_String);
- elsif Has_Wide_Character (Exp) then
- Resolve (Exp, Standard_Wide_String);
- else
- Resolve (Exp, Standard_String);
- end if;
+ Arg := Next (Arg2);
+ while Present (Arg) loop
+ Exp := Get_Pragma_Arg (Arg);
+ Analyze (Exp);
- elsif Is_Overloaded (Exp) then
- Error_Pragma_Arg
- ("ambiguous argument for pragma%", Exp);
+ if Is_Entity_Name (Exp) then
+ null;
+
+ -- For string literals, we assume Standard_String as the
+ -- type, unless the string contains wide or wide_wide
+ -- characters.
+ elsif Nkind (Exp) = N_String_Literal then
+ if Has_Wide_Wide_Character (Exp) then
+ Resolve (Exp, Standard_Wide_Wide_String);
+ elsif Has_Wide_Character (Exp) then
+ Resolve (Exp, Standard_Wide_String);
else
- Resolve (Exp);
+ Resolve (Exp, Standard_String);
end if;
- Next (Arg);
- end loop;
- end if;
- end;
+ elsif Is_Overloaded (Exp) then
+ Error_Pragma_Arg
+ ("ambiguous argument for pragma%", Exp);
+
+ else
+ Resolve (Exp);
+ end if;
+
+ Next (Arg);
+ end loop;
+ end if;
end Annotate;
------------
-- specification, and calls to the subprogram, from being in ALFA.
-- If the subprogram being marked as not in ALFA is annotated with
- -- Formal_Proof being On, then an error is issued with message Msg on node
- -- N.
+ -- Formal_Proof On, then an error is issued with message Msg on node N.
function Defining_Entity (N : Node_Id) return Entity_Id;
-- Given a declaration N, returns the associated defining entity. If the
-- This package obtains parameters from the target runtime version of System,
-- to indicate parameters relevant to the target environment.
--- Is it right for this to be modified GPL???
-
-- Conceptually, these parameters could be obtained using rtsfind, but
-- we do not do this for four reasons:
projects / gcc.git / commitdiff