+2021-12-02 Eric Botcazou <ebotcazou@adacore.com>
+
+ * gcc-interface/Make-lang.in (ADA_GENERATED_FILES): Add warning.
+
+2021-12-02 Marc Poulhiès <poulhies@adacore.com>
+
+ * gcc-interface/a-assert.ads, gcc-interface/a-assert.adb: Remove.
+
+2021-12-02 Eric Botcazou <ebotcazou@adacore.com>
+
+ * gcc-interface/decl.c (gnat_to_gnu_entity): Do not back-annotate a
+ maximum size for the Esize of limited record and concurrent types.
+
+2021-12-02 Eric Botcazou <ebotcazou@adacore.com>
+
+ * gcc-interface/gigi.h (aggregate_type_contains_array_p): Delete.
+ (type_has_variable_size): Declare.
+ * gcc-interface/decl.c (adjust_packed): Return 0 only if the field
+ type is an array with variable size.
+ * gcc-interface/utils.c (aggregate_type_contains_array_p): Make
+ static and remove SELF_REFERENTIAL parameter.
+ (type_has_variable_size): Make public.
+ (create_field_decl): Adjust call to aggregate_type_contains_array_p.
+
+2021-12-02 Justin Squirek <squirek@adacore.com>
+
+ * gcc-interface/decl.c (gnat_to_gnu_entity): Skip normal
+ processing for Itypes that are E_Class_Wide_Subtype with
+ Equivalent_Type set.
+
+2021-12-02 Eric Botcazou <ebotcazou@adacore.com>
+
+ * gcc-interface/trans.c (Call_to_gnu): Rename GNAT_NAME variable
+ into GNAT_SUBPROG to avoid later shadowing.
+
+2021-12-02 Yannick Moy <moy@adacore.com>
+
+ * libgnat/s-arit32.adb: Add ghost instances and lemmas.
+ (Scaled_Divide32): Add ghost code to prove. Minor code
+ modification to return early in error when divisor is zero.
+ * libgnat/s-arit32.ads: Add ghost instances and utilities.
+ (Scaled_Divide32): Add contract.
+
+2021-12-02 Eric Botcazou <ebotcazou@adacore.com>
+
+ * sprint.adb (Source_Dump): Set both Print_Generated_Code and
+ Debug_Generated_Code to False at the end.
+
+2021-12-02 Marc Poulhiès <poulhies@adacore.com>
+
+ * sem_aggr.adb (Resolve_Array_Aggregate): Filter out nodes not
+ coming from source before emitting the warning.
+
+2021-12-02 Yannick Moy <moy@adacore.com>
+
+ * libgnat/s-aridou.adb (Log_Single_Size, Big_0): New ghost
+ constants.
+ (Lemma_Mult_Non_Negative, Lemma_Mult_Non_Positive,
+ Lemma_Not_In_Range_Big2xx64): New lemmas on big integers.
+ (Double_Divide): Remove justifications. Amend for that local
+ lemma Prove_Overflow_Case.
+ (Scaled_Divide): Remove justifications. Insert for that local
+ lemmas Prove_Negative_Dividend, Prove_Positive_Dividend and
+ Prove_Q_Too_Big, and amend local lemma Prove_Overflow. To prove
+ the loop invariant on (Shift mod 2 = 0), introduce local ghost
+ variable Iter to count loop iterations, and relate its value to
+ the value of Shift through Log_Single_Size, with the help of
+ local lemma Prove_Power. Deal with proof regression by adding
+ new local lemma Prove_First_Iteration and local ghost variable
+ D123.
+ * libgnat/s-arit64.ads (Multiply_With_Ovflo_Check64): Remove
+ unnecessary Pure_Function on function as package is Pure.
+
+2021-12-02 Yannick Moy <moy@adacore.com>
+
+ * libgnat/s-widthi.adb: Add pragma Annotate.
+
+2021-12-02 Yannick Moy <moy@adacore.com>
+
+ * libgnat/s-widint.ads: Mark in SPARK.
+ * libgnat/s-widlli.ads: Likewise.
+ * libgnat/s-widllli.ads: Likewise.
+ * libgnat/s-widlllu.ads: Likewise.
+ * libgnat/s-widllu.ads: Disable ghost/contract.
+ * libgnat/s-widthi.adb: Replicate and adapt the proof from
+ s-widthu.adb.
+ * libgnat/s-widthi.ads: Add minimal postcondition.
+ * libgnat/s-widthu.adb: Fix comments in the modular case.
+ * libgnat/s-widthu.ads: Add minimal postcondition.
+ * libgnat/s-widuns.ads: Disable ghost/contract.
+
+2021-12-02 Piotr Trojanek <trojanek@adacore.com>
+
+ * rtsfind.ads (RE_Id, RE_Unit_Table): Add RE_Suspension_Object.
+ * sem_util.adb (Is_Descendant_Of_Suspension_Object): Use Is_RTE.
+ (Is_Suspension_Object): Remove body.
+ * sem_util.ads (Is_Suspension_Object): Remove spec.
+ * snames.ads-tmpl (Name_Suspension_Object): Remove, now
+ unreferenced.
+
+2021-12-02 Piotr Trojanek <trojanek@adacore.com>
+
+ * exp_util.adb (Append_Freeze_Action): Tune whitespace to make
+ the code look similar to Append_Freeze_Actions, which takes a
+ List_Id.
+ * sem_ch6.adb (Analyze_Return_Type): Cleanup with
+ Append_Freeze_Action.
+ * exp_ch3.adb (Build_Access_Subprogram_Wrapper_Body): Likewise.
+ * sem_ch3.adb (Build_Access_Subprogram_Wrapper): Likewise.
+ * contracts.adb (Add_Indirect_Call_Wrapper): Remove extra call
+ to Ensure_Freeze_Node.
+ (Add_Call_Helper): Likewise.
+ * freeze.adb (Check_Inherited_Conditions): Likewise.
+ (Attribute_Renaming): Likewise.
+ * sem_ch8.adb: Likewise.
+
+2021-12-02 Piotr Trojanek <trojanek@adacore.com>
+
+ * doc/gnat_rm/standard_and_implementation_defined_restrictions.rst
+ (No_Dispatching_Calls): Fix whitespace in example code.
+ * gnat_rm.texi: Regenerate.
+ * exp_ch13.adb (Expand_N_Freeze_Entity): Replace low-level
+ membership test with a high-level wrapper.
+ * exp_ch3.adb (Expand_Freeze_Record_Type): Remove unnecessary
+ initialization of list of wrapper declarations and unnecessary
+ guard for list of their bodies (if no bodies are created then
+ Append_Freeze_Actions is a no-op).
+
+2021-12-02 Marc Poulhiès <poulhies@adacore.com>
+
+ * exp_imgv.adb (Append_Table_To): Add new parameter to
+ Make_Aggregate call.
+ * gen_il-fields.ads (Opt_Field_Enum):
+ Add Is_Parenthesis_Aggregate and Is_Enum_Array_Aggregate.
+ * gen_il-gen-gen_nodes.adb (Union): Add Is_Enum_Array_Aggregate
+ and Is_Parenthesis_Aggregate field to N_Aggregate.
+ * libgnarl/s-interr.adb (User_Handler, User_Entry, Blocked)
+ (Ignored, Last_Unblocker, Server_ID): Likewise.
+ * libgnarl/s-intman.ads (Keep_Unmasked, Reserve): Likewise.
+ * libgnarl/s-intman__posix.adb (Exception_Interrupts)
+ (Initialize): Likewise.
+ * libgnarl/s-mudido__affinity.adb (Create): Likewise.
+ * libgnarl/s-osinte__linux.ads (Unmasked, Reserved): Likewise.
+ * libgnarl/s-taprop__linux.adb (Create_Task, Set_Task_Affinity)
+ * libgnarl/s-tasdeb.adb (Trace_On): Likewise.
+ * libgnarl/s-tasdeb.ads (Known_Tasks): Likewise.
+ * libgnarl/s-tasinf__linux.ads (Any_CPU, No_CPU): Likewise.
+ * libgnarl/s-taskin.adb (Initialize_ATCB): Likewise.
+ * libgnarl/s-taskin.ads (Ada_Task_Control_Block): Likewise.
+ * libgnarl/s-tasren.adb (Default_Treatment)
+ (New_State): Likewise.
+ * libgnarl/s-tassta.adb (Trace_Unhandled_Exception_In_Task):
+ Likewise.
+ * libgnarl/s-tataat.adb (Index_Array): Likewise.
+ * libgnarl/s-tpobop.adb (New_State): Likewise.
+ * libgnat/a-calend.adb (Cumulative_Days_Before_Month)
+ (Leap_Second_Times): Likewise.
+ * libgnat/a-calend.ads (Days_In_Month): Likewise.
+ * libgnat/a-cfinve.adb (Insert): Likewise.
+ * libgnat/a-chahan.adb (Char_Map): Likewise.
+ * libgnat/a-chtgbo.adb (Clear): Likewise.
+ * libgnat/a-cobove.adb ("&", Insert, To_Vector): Likewise.
+ * libgnat/a-cofove.adb (Insert, To_Vector): Likewise.
+ * libgnat/a-cohata.ads (Hash_Table_Type): Likewise.
+ * libgnat/a-coinve.adb (Merge, Insert, Insert_Space): Likewise.
+ * libgnat/a-convec.adb (Insert, To_Vector): Likewise.
+ * libgnat/a-coprnu.ads (Primes): Likewise.
+ * libgnat/a-direct.adb (Empty_String): Use regular "" instead
+ of aggregate.
+ (Start_Search_Internal, Name_Case_Equivalence, Search)
+ (Start_Search, Start_Search_Internal): Use bracket for
+ aggregate.
+ * libgnat/a-direct.ads (Start_Search,Search): Likewise.
+ * libgnat/a-direio.adb (Zeroes): Likewise.
+ * libgnat/a-nbnbre.adb (Leading_Padding, Trailing_Padding)
+ (Numerator_Image): Likewise.
+ * libgnat/a-ngrear.adb (Jacobi): Likewise.
+ * libgnat/a-stbubo.adb (Get_UTF_8): Likewise.
+ * libgnat/a-stbufo.adb (Put): Likewise.
+ * libgnat/a-stbuun.adb (Get_UTF_8): Likewise.
+ * libgnat/a-stbuut.adb (Put_7bit, Put_Character)
+ (Put_Wide_Character, Put_Wide_Wide_Character): Likewise.
+ * libgnat/a-stmaco.ads (Control_Set,Graphic_Set,Letter_Set)
+ (Lower_Set, Upper_Set, Basic_Set, Decimal_Digit_Set)
+ (Hexadecimal_Digit_Set, Alphanumeric_Set, Special_Set)
+ (ISO_646_Set): Likewise.
+ * libgnat/a-strbou.ads (Insert, Tail, "*", Replicate)
+ (Null_Bounded_String): Likewise.
+ * libgnat/a-strfix.ads (Head, Tail): Likewise.
+ * libgnat/a-strmap.adb (To_Domain, Lemma_Is_Sorted): Likewise.
+ * libgnat/a-strmap.ads (Null_Set): Likewise.
+ * libgnat/a-strsup.adb (Super_Head, Super_Replicate)
+ (Super_Tail): Likewise.
+ * libgnat/a-strsup.ads (Super_Head, Super_Tail, Times)
+ (Super_Replicate): Likewise.
+ * libgnat/a-sttebu.adb (Put_UTF8, Wide_Put_UTF_16): Likewise.
+ * libgnat/a-stuten.ads (BOM_16): Likewise.
+ * libgnat/a-stwibo.ads (Null_Bounded_Wide_String): Likewise.
+ * libgnat/a-stwima.ads (Null_Range): Likewise.
+ * libgnat/a-stwisu.adb (Super_Head, Super_Replicate)
+ (Super_Tail): Likewise.
+ * libgnat/a-stzbou.ads
+ (Null_Bounded_Wide_Wide_String): Likewise.
+ * libgnat/a-stzmap.ads (Null_Range): Likewise.
+ * libgnat/a-stzsup.adb (Super_Head, Super_Replicate)
+ (Super_Tail, Super_Trim): Likewise.
+ * libgnat/a-swmwco.ads (Control_Ranges, Graphic_Ranges)
+ (Letter_Ranges, Lower_Ranges, Upeer_Ranges, Basic_Ranges)
+ (Decimal_Digit_Ranges, Hexadecimal_Digit_Ranges)
+ (Alphanumeric_Ranges, Special_Graphic_Ranges, ISO_646_Ranges)
+ (Character_Ranges, Lower_Case_Mapping, Upper_Case_Mapping)
+ (Basic_Mapping): Likewise.
+ * libgnat/a-szmzco.ads (Control_Ranges, Graphic_Ranges)
+ (Letter_Ranges, Lower_Ranges, Upeer_Ranges, Basic_Ranges)
+ (Decimal_Digit_Ranges, Hexadecimal_Digit_Ranges)
+ (Alphanumeric_Ranges, Special_Graphic_Ranges, ISO_646_Ranges)
+ (Character_Ranges, Lower_Case_Mapping, Upper_Case_Mapping)
+ (Basic_Mapping): Likewise.
+ * libgnat/a-teioed.adb (Format_Number): Likewise.
+ * libgnat/a-wtedit.adb (Format_Number): Likewise.
+ * libgnat/a-ztedit.adb (Format_Number): Likewise.
+ * libgnat/g-arrspl.adb (Separators): Likewise.
+ * libgnat/g-catiio.adb (Month_Name_To_Number): Likewise.
+ * libgnat/g-cgideb.adb (NL, Title): Likewise.
+ * libgnat/g-comlin.adb (Internal_Initialize_Option_Scan)
+ (Display_Section_Help): Likewise.
+ * libgnat/g-comlin.ads (Opt_Parser_Data): Likewise.
+ * libgnat/g-debpoo.adb (Set_Dead_Beef, Dump): Likewise.
+ * libgnat/g-expect.adb (Expect, Has_Process, Send): Likewise.
+ * libgnat/g-forstr.adb ("+", Get_Formatted): Likewise.
+ * libgnat/g-memdum.adb (Dump): Likewise.
+ * libgnat/g-rannum.adb (Image): Likewise.
+ * libgnat/g-sechas.adb (Final, HMAC_Initial_Context): Likewise.
+ * libgnat/g-sehamd.ads (Initial_State): Likewise.
+ * libgnat/g-sehash.ads (Initial_State): Likewise.
+ * libgnat/g-sercom.ads (Data_Rate_Value): Likewise.
+ * libgnat/g-sercom__linux.adb (C_Data_Rate, C_Bits, C_Stop_Bits)
+ (C_Parity): Likewise.
+ * libgnat/g-shsh32.ads (K, Transform): Likewise.
+ * libgnat/g-shsh64.ads (K, Transform): Likewise.
+ * libgnat/g-socket.adb (Levels, Modes, Shutmodes, Requests)
+ (Options, Flags, Get_Name_Info, Image): Likewise.
+ * libgnat/g-socket.ads (Inet_Addr_Bytes_Length, Inet_Addr_Type)
+ (IPv4_To_IPv6_Prefix, Any_Inet_Addr, Any_Inet6_Addr)
+ (No_Inet_Addr, Broadcast_Inet_Addr, Loopback_Inet_Addr)
+ (Loopback_Inet6_Addr, Unspecified_Group_Inet_Addr)
+ (All_Hosts_Group_Inet_Addr, All_Routers_Group_Inet_Addr)
+ (Unspecified_Group_Inet6_Addr, All_Hosts_Group_Inet6_Addr)
+ (All_Routers_Group_Inet6_Addr): Likewise.
+ * libgnat/g-socpol.adb (To_C, Status, Get_Events): Likewise.
+ * libgnat/g-socpol.ads (Input_Event, Output_Event, Both_Event)
+ (Error_Event): Likewise.
+ * libgnat/g-sothco.ads (Families, Lengths, Sockaddr): Likewise.
+ * libgnat/g-spipat.adb (OK_For_Simple_Arbno): Likewise.
+ * libgnat/i-cobol.ads (Ada_To_COBOL, COBOL_To_Ada): Likewise.
+ * libgnat/i-pacdec.adb (Packed_Byte): Likewise.
+ * libgnat/i-pacdec.ads (Packed_Size): Likewise.
+ * libgnat/s-bitops.adb (Masks): Likewise.
+ * libgnat/s-crc32.adb (Table): Likewise.
+ * libgnat/s-gearop.adb (Unit_Matrix, Unit_Vector): Likewise.
+ * libgnat/s-genbig.adb (Out_data, Zero_Data, Big_Exp, Big_Mul)
+ (To_Bignum, To_String, Image, Leading_Padding): Likewise.
+ * libgnat/s-htable.adb (Reset): Likewise.
+ * libgnat/s-imgcha.adb (C0, C1): Likewise.
+ * libgnat/s-powflt.ads (Powten): Likewise.
+ * libgnat/s-powlfl.ads (Powten): Likewise.
+ * libgnat/s-powllf.ads (Powten): Likewise.
+ * libgnat/s-rannum.adb (Matrix_A, Random_Float_Template, Image):
+ Likewise.
+ * libgnat/s-rannum.ads (Generator): Likewise.
+ * libgnat/s-regexp.adb (Compile,Create_Primary_Table)
+ (Create_Primary_Table_Glob, Create_Secondary_Table, Compile):
+ Likewise.
+ * libgnat/s-regpat.adb (Bit_Conversion, Set, Dump_Until)
+ (Dump_Current, Dump_Error, Try, Reset_Class): Likewise.
+ * libgnat/s-regpat.ads (Pattern_Matcher, Never_Match): Likewise.
+ * libgnat/s-scaval__128.adb (Initialize): Likewise.
+ * libgnat/s-statxd.adb (Fields, W_F, W_LF)
+ (W_LLF, W_SF): Likewise.
+ * libgnat/s-stausa.adb (Initialize, Initialize_Analyzer)
+ (Output_Results): Likewise.
+ * libgnat/s-strops.adb (Str_Concat_SC): Likewise.
+ * libgnat/s-valrea.adb (Maxexp32, Maxexp64, Maxexp80): Likewise.
+ * libgnat/s-wchcon.ads (WC_Encoding_Letters)
+ (WC_Longest_Sequences): Likewise.
+ * par-ch4.adb (P_Aggregate_Or_Paren_Expr): Set
+ Is_Parenthesis_Aggregate when creating a N_Aggregate using
+ parenthesis.
+ * scng.adb (Scan): Lower version needed for bracket syntax from
+ Extensions to Ada2022.
+ * sem_aggr.adb (Resolve_Aggregate): Raise error for container
+ aggregate using parenthesis instead of bracket.
+ (Resolve_Array_Aggregate): Raise warning for aggregate using
+ parenthesis in Ada2022 with obsolescent warning enabled and not
+ in GNAT mode.
+ * sem_util.ads (Check_Ambiguous_Aggregate): Typo fix in comment.
+
+2021-12-02 Piotr Trojanek <trojanek@adacore.com>
+
+ * libgnarl/a-taside.ads (Activation_Is_Complete): Add pragma
+ Inline.
+
+2021-12-02 Eric Botcazou <ebotcazou@adacore.com>
+
+ * sem_ch12.adb (Freeze_Package_Instance): Consistently consider
+ the freeze node of the parent and use large inequality for
+ Slocs.
+ (Freeze_Subprogram_Instance): Likewise.
+ (Insert_Freeze_Node_For_Instance): For an instance in a package
+ spec with no source body that immediately follows, consider the
+ body of the package for the placement of the freeze node and go
+ to the outer level if there is no such body.
+
+2021-12-02 Piotr Trojanek <trojanek@adacore.com>
+
+ * exp_ch13.ads (Expand_N_Freeze_Entity): Add note about a SPARK
+ twin.
+ * exp_ch3.ads (Freeze_Type): Likewise.
+ * exp_spark.adb (Expand_SPARK_N_Freeze_Entity): Mimic what is
+ done in Freeze_Entity.
+ (SPARK_Freeze_Type): Mimic what is done in Freeze_Type; add call
+ to Make_Predefined_Primitive_Eq_Spec.
+
+2021-12-02 Piotr Trojanek <trojanek@adacore.com>
+
+ * exp_ch3.adb (Make_Predefined_Primitive_Specs): Move code for
+ spec of dispatching equality.
+ (Predefined_Primitive_Bodies): Move code for body if dispatching
+ equality.
+ (Make_Predefined_Primitive_Eq_Spec): Separated code for spec of
+ dispatching equality.
+ (Predefined_Primitive_Eq_Body): Separated code for body of
+ dispatching equality.
+ * exp_ch3.ads: Update.
+
+2021-12-02 Piotr Trojanek <trojanek@adacore.com>
+
+ * libgnat/s-valuti.ads (Scan_Natural_Ghost): Split body from
+ spec and put it into private part, so that GNATprove can pick it
+ both when analysing the unit and its clients.
+
+2021-12-02 Piotr Trojanek <trojanek@adacore.com>
+
+ * exp_aggr.adb, exp_ch6.adb, par-ch4.adb, sem_ch13.adb: Remove
+ extra space after ":=" symbol.
+ * gen_il-gen.adb: Likewise; add missing headerbox.
+
+2021-12-02 Richard Kenner <kenner@adacore.com>
+
+ * rtsfind.adb (Maybe_Add_With): Ensure that the added "with" is
+ never marked as ignored ghost code.
+
+2021-12-02 Piotr Trojanek <trojanek@adacore.com>
+
+ * freeze.adb (Freeze_Entity): Replace First_Entity/Next_Entity
+ with First_Component/Next_Component; remove condition with Ekind
+ equal to E_Component.
+ * sem_ch13.adb (Check_Record_Representation_Clause): Likewise
+ for component-or-discriminant.
+ * sem_util.adb (Is_Fully_Initialized_Type): Likewise; rename Ent
+ to a more specific Comp.
+ * sem_warn.adb (Check_References): Likewise.
+
+2021-12-02 Piotr Trojanek <trojanek@adacore.com>
+
+ * sem_warn.adb (Warn_On_Unassigned_Out_Parameter): Move inner
+ loop at the beginning of subprogram, so it is executed only
+ once; fix order in the "add an ad hoc" phrase.
+
+2021-12-02 Piotr Trojanek <trojanek@adacore.com>
+
+ * sem_warn.adb (Check_References): Remove redundant condition.
+
+2021-12-02 Doug Rupp <rupp@adacore.com>
+
+ * vxworks7-cert-rtp-link__ppcXX.spec: New file.
+ * Makefile.rtl: Use it.
+
+2021-12-02 Yannick Moy <moy@adacore.com>
+
+ * libgnat/i-c.adb: Add ghost code.
+ (C_Length_Ghost): New ghost functions to query the C length of a
+ string.
+ (To_Ada): Insert constant Count_Cst where needed to comply with
+ SPARK. Homogeneize code between variants for char, wchar_t,
+ char16_t and char32_t. Use char16_nul and char32_nul
+ systematically instead of their value. Fix the type of index To
+ to be Integer instead of Positive, to avoid a possible range
+ check failure on an empty Target. Insert an exit statement to
+ avoid a possible overflow failure when the last index in Target
+ is Natural'Last (possibly on a small string as well).
+ * libgnat/i-c.ads: Add contracts.
+ (C_Length_Ghost): New ghost functions to query the C length of a
+ string.
+ * libgnat/s-os_lib.adb: Remove pragma Compiler_Unit_Warning
+ causing a spurious error during compilation of GNAT, as this
+ pragma is not needed anymore now that we bootstrap (stage1) with
+ the base compiler runtime.
+
+2021-12-02 Piotr Trojanek <trojanek@adacore.com>
+
+ * libgnarl/a-taside.ads (Activation_Is_Complete): Add
+ precondition.
+
+2021-12-02 Piotr Trojanek <trojanek@adacore.com>
+
+ * sem_ch3.adb (Check_Derived_Type): Rename local variables; fix
+ style in comment.
+
+2021-12-02 Yannick Moy <moy@adacore.com>
+
+ * libgnat/s-valboo.adb (First_Non_Space_Ghost): Move to
+ utilities.
+ (Value_Boolean): Prefix call to First_Non_Space_Ghost.
+ * libgnat/s-valboo.ads (First_Non_Space_Ghost): Move to
+ utilities.
+ (Is_Boolean_Image_Ghost, Value_Boolean): Prefix call to
+ First_Non_Space_Ghost.
+ * libgnat/s-valuer.adb (Scan_Raw_Real): Adapt to change of
+ function Scan_Exponent to procedure.
+ * libgnat/s-valueu.adb (Scan_Raw_Unsigned): Adapt to change of
+ function Scan_Exponent to procedure.
+ * libgnat/s-valuti.adb (First_Non_Space_Ghost): Function moved
+ here.
+ (Last_Number_Ghost): New ghost query function.
+ (Scan_Exponent): Change function with side-effects into
+ procedure, to mark in SPARK. Prove procedure wrt contract.
+ Change type of local P to avoid possible range check failure (it
+ is not known whether this can be activated by callers).
+ (Scan_Plus_Sign, Scan_Sign): Change type of local P to avoid
+ possible range check failure. Add loop invariants and assertions
+ for proof.
+ (Scan_Trailing_Blanks): Add loop invariant.
+ (Scan_Underscore): Remove SPARK_Mode Off.
+ * libgnat/s-valuti.ads (First_Non_Space_Ghost): Function moved
+ here.
+ (Last_Number_Ghost, Only_Number_Ghost, Is_Natural_Format_Ghost,
+ Scan_Natural_Ghost): New ghost query functions.
+ (Scan_Plus_Sign, Scan_Sign, Scan_Exponent, Scan_Trailing_Blanks,
+ Scan_Underscore): Add functional contracts.
+
+2021-12-02 Yannick Moy <moy@adacore.com>
+
+ * libgnat/s-imgboo.adb: Mark in SPARK.
+ * libgnat/s-imgboo.ads: Mark in SPARK. Change from Pure to
+ Preelaborate unit in order to be able to depend on
+ System.Val_Bool.
+ (Image_Boolean): Functionally specify the result of the
+ procedure by calling System.Val_Bool.Value_Boolean on the
+ result.
+ * libgnat/s-valboo.adb: Mark in SPARK.
+ (First_Non_Space_Ghost): New ghost function.
+ (Value_Boolean): Change type of L and F to avoid possible range
+ check failure on empty Str.
+ * libgnat/s-valboo.ads: Mark in SPARK. Duplicate with-clause
+ from body in the spec to be able to call
+ System.Val_Util.Only_Space_Ghost in the contract.
+ (First_Non_Space_Ghost): New ghost function computing the first
+ non-space character in a string.
+ (Is_Boolean_Image_Ghost): New ghost function computing whether a
+ string is the image of a boolean value.
+ (Value_Boolean): Add in precondition the conditions to avoid
+ raising Constraint_Error. This precondition is never executed,
+ and only used in proof, thanks to the use of pragma
+ Assertion_Policy. Given that precondition, the postcondition can
+ simply check the first non-space character to decide whether
+ True or False is read.
+ * libgnat/s-valuti.adb: Mark in SPARK, but use SPARK_Mode Off on
+ all subprograms not yet proved.
+ (Bad_Value): Annotate expected exception.
+ (Normalize_String): Rewrite to avoid possible overflow when
+ incrementing F in the first loop. Add loop invariants.
+ * libgnat/s-valuti.ads: Mark in SPARK.
+ (Bad_Value): Add Depends contract to avoid warning on unused S.
+ (Only_Space_Ghost): New ghost function to query if string has
+ only space in the specified range.
+ (Normalize_String): Add functional contract.
+ (Scan_Exponent): Mark spec as not in SPARK as this function has
+ side-effects.
+
+2021-12-02 Pascal Obry <obry@adacore.com>
+
+ * libgnat/g-socket.ads (Max_Name_Length): Initialize with
+ NI_MAXHOST.
+
+2021-12-02 Pascal Obry <obry@adacore.com>
+
+ * libgnat/g-socket.ads: Minor style fix.
+
2021-12-01 Eric Botcazou <ebotcazou@adacore.com>
* einfo.ads (E_Decimal_Fixed_Point_Subtype): Fix pasto.
projects / thirdparty / gcc.git / blobdiff