aboutsummaryrefslogtreecommitdiff
path: root/gcc/ada/libgnat
AgeCommit message (Collapse)AuthorFilesLines
2022-09-02[Ada] Fix proof of runtime unit System.Exp_ModClaire Dross1-0/+10
Regain the proof of System.Exp_Mod after changes in provers and Why3. gcc/ada/ * libgnat/s-expmod.adb (Lemma_Add_Mod): Add new lemma to factor out a complex sub-proof. (Exp_Modular): Add assertion to help proof.
2022-09-02[Ada] Fix proof of runtime unit System.Wid_*Claire Dross1-1/+15
Regain the proof of System.Wid_* after changes in provers and Why3. gcc/ada/ * libgnat/s-widthu.adb (Lemma_Euclidean): Lemma to prove the relation between the quotient/remainder of a division.
2022-09-02[Ada] Recover proof of Scaled_Divide in System.Arith_64Yannick Moy2-122/+211
Proof of Scaled_Divide was impacted by changes in provers and Why3. Recover it partially, leaving some unproved basic inferences to be further investigated. gcc/ada/ * libgnat/s-aridou.adb: Add or rework ghost code. * libgnat/s-aridou.ads: Add Big_Positive subtype.
2022-09-02[Ada] Fix proof of runtime unit System.Value* and System.Image*Claire Dross24-1547/+1853
Refactor specification of the Value* and Image* units and fix proofs. gcc/ada/ * libgnat/a-nbnbig.ads: Add Always_Return annotation. * libgnat/s-vaispe.ads: New ghost unit for the specification of System.Value_I. Restore proofs. * libgnat/s-vauspe.ads: New ghost unit for the specification of System.Value_U. Restore proofs. * libgnat/s-valuei.adb: The specification only subprograms are moved to System.Value_I_Spec. Restore proofs. * libgnat/s-valueu.adb: The specification only subprograms are moved to System.Value_U_Spec. Restore proofs. * libgnat/s-valuti.ads (Uns_Params): Generic unit used to bundle together the specification functions of System.Value_U_Spec. (Int_Params): Generic unit used to bundle together the specification functions of System.Value_I_Spec. * libgnat/s-imagef.adb: It is now possible to instantiate the appropriate specification units instead of creating imported ghost subprograms. * libgnat/s-imagei.adb: Update to refactoring of specifications and fix proofs. * libgnat/s-imageu.adb: Likewise. * libgnat/s-imgint.ads: Ghost parameters are grouped together in a package now. * libgnat/s-imglli.ads: Likewise. * libgnat/s-imgllu.ads: Likewise. * libgnat/s-imgllli.ads: Likewise. * libgnat/s-imglllu.ads: Likewise. * libgnat/s-imguns.ads: Likewise. * libgnat/s-vallli.ads: Likewise. * libgnat/s-valllli.ads: Likewise. * libgnat/s-imagei.ads: Likewise. * libgnat/s-imageu.ads: Likewise. * libgnat/s-vaispe.adb: Likewise. * libgnat/s-valint.ads: Likewise. * libgnat/s-valuei.ads: Likewise. * libgnat/s-valueu.ads: Likewise. * libgnat/s-vauspe.adb: Likewise.
2022-07-13[Ada] Fix proof of runtime unit System.Arith_64Yannick Moy1-4/+92
After changes in provers and Why3, changes are needed to recover automatic proof of System.Arith_64. This is the first part of it. gcc/ada/ * libgnat/s-aridou.adb (Lemma_Mult_Div, Lemma_Powers): New lemmas. (Prove_Sign_Quotient): New local lemma. (Prove_Signs): Expand definition of Big_R and Big_Q in the postcondition. Add intermediate assertions. (Double_Divide): Call new lemma. (Lemma_Div_Eq): Provide body for proving lemma. (Lemma_Powers_Of_2, Lemma_Shift_Without_Drop, Prove_Dividend_Scaling, Prove_Multiplication, Prove_Z_Low): Call lemmas, add intermediate assertions.
2022-07-13[Ada] Fix automatic proof on System.Arith_32Yannick Moy1-1/+2
gcc/ada/ * libgnat/s-arit32.adb (Scaled_Divide32): Add an assertion, move the call of Prove_Sign_R around.
2022-07-13[Ada] Fix CodePeer warnings in GNAT sourcesJustin Squirek2-115/+15
This patch fixes various redundant constructs or uninitialized variables identified by CodePeer in the GNAT frontend and runtime sources. gcc/ada/ * exp_ch6.adb (Expand_N_Extended_Return_Statement): Add default initialization for Stmts. * sem_ch12.adb (Analyze_Associations): Add default initialization for Match. * libgnat/a-ztenau.adb (Scan_Enum_Lit): Remove duplicated boolean test. * libgnat/g-spipat.adb (XMatch): Combine duplicated cases.
2022-07-12[Ada] Fix 0-sized secondary stack allocationsMarc Poulhiès1-1/+6
The Has_Enough_Free_Memory was not correctly reporting a completely full chunk in the case of a 0-sized allocation. gcc/ada/ * libgnat/s-secsta.adb (Has_Enough_Free_Memory): Check for full chunk before computing the available size.
2022-07-12[Ada] Suppress warning in g-socthi__vxworks.adbBob Duff1-1/+3
Follow-on to previous change, which missed the vxworks version of this package. gcc/ada/ * libgnat/g-socthi__vxworks.adb (C_Connect): Suppress new warning.
2022-07-12[Ada] Vxworks7* - Makefile.rtl rtp vs rtp-smp cleanup - remove unused filesDoug Rupp2-327/+0
Only smp runtimes are built for vxworks7*, even though the -smp suffix is removed during install. This change removes unused system packages for rtp runtimes. gcc/ada/ * libgnat/system-vxworks7-ppc-rtp.ads: Remove * libgnat/system-vxworks7-x86-rtp.ads: Likewise.
2022-07-12[Ada] Remove out-of-range warning in unreachable codeBob Duff1-1/+3
This patch removes a warning in examples like this: if cond then return; -- or other jump end if; X := ...; -- where the value is out of range where cond is known at compile time. It could, for example, be a generic formal parameter that is known to be True in some instances. As a side effect, this patch adds new warnings about unreachable code. gcc/ada/ * gnatls.adb (Output_License_Information): Remove pragma No_Return; call sites deal with Exit_Program. * libgnat/g-socthi.adb (C_Connect): Suppress warning about unreachable code. * sem_ch5.adb (Check_Unreachable_Code): Special-case if statements with static conditions. If we remove unreachable code (including the return statement) from a function, add "raise Program_Error", so we won't warn about missing returns. Remove Original_Node in test for N_Raise_Statement; it's not needed. Remove test for CodePeer_Mode; if Operating_Mode = Generate_Code, then CodePeer_Mode can't be True. Misc cleanup. Do not reuse Nxt variable for unrelated purpose (the usage in the Kill_Dead_Code loop is entirely local to the loop). * sem_ch6.adb: Add check for Is_Transfer. Misc cleanup. * sem_prag.adb: Minor. * sem_res.adb: Minor. * sem_util.adb: Minor cleanup. (Is_Trivial_Boolean): Move to nonnested place, so it can be called from elsewhere. (Is_Static_Constant_Boolean): New function. * sem_util.ads (Is_Trivial_Boolean): Export. (Is_Static_Constant_Boolean): New function.
2022-07-12[Ada] Add one more leading underscore to couple of exported symbolsEric Botcazou1-2/+2
For the sake of consistency with other runtime units. gcc/ada/ * libgnat/s-stchop.ads: Use a double underscore prefix for symbols.
2022-07-12[Ada] Annotate libraries with returning annotationJoffrey Huguet37-258/+442
This patch annotates SPARK-annotated libraries with returning annotations (Always_Return, Might_Not_Return) to remove the warnings raised by GNATprove about missing annotations. gcc/ada/ * libgnarl/a-reatim.ads, libgnat/a-cfdlli.ads, libgnat/a-cfhama.ads, libgnat/a-cfhase.ads, libgnat/a-cfinse.ads, libgnat/a-cfinve.ads, libgnat/a-cforma.ads, libgnat/a-cforse.ads, libgnat/a-chahan.ads, libgnat/a-cofove.ads, libgnat/a-cofuma.ads, libgnat/a-cofuse.ads, libgnat/a-cofuve.ads, libgnat/a-nbnbin.ads, libgnat/a-nbnbre.ads, libgnat/a-ngelfu.ads, libgnat/a-nlelfu.ads, libgnat/a-nllefu.ads, libgnat/a-nselfu.ads, libgnat/a-nuelfu.ads, libgnat/a-strbou.ads, libgnat/a-strfix.ads, libgnat/a-strmap.ads, libgnat/a-strunb.ads, libgnat/a-strunb__shared.ads, libgnat/a-strsea.ads, libgnat/a-textio.ads, libgnat/a-tideio.ads, libgnat/a-tienio.ads, libgnat/a-tifiio.ads, libgnat/a-tiflio.ads, libgnat/a-tiinio.ads, libgnat/a-timoio.ads, libgnat/i-c.ads, libgnat/interfac.ads, libgnat/interfac__2020.ads, libgnat/s-atacco.ads, libgnat/s-stoele.ads: Annotate packages and subprograms with returning annotations.
2022-07-12[Ada] Fix buffer overrun for small string concatenation at -O0Eric Botcazou16-228/+19
The concatenation routines may read too much data on the source side when the destination buffer is larger than the final result. This change makes sure that this does not happen any more and also removes obsolete stuff. gcc/ada/ * rtsfind.ads (RE_Id): Remove RE_Str_Concat_Bounds_N values. (RE_Unit_Table): Remove RE_Str_Concat_Bounds_N entries. * libgnat/s-conca2.ads (Str_Concat_2): Adjust head comment. (Str_Concat_Bounds_2): Delete. * libgnat/s-conca2.adb (Str_Concat_2): Use the length of the last input to size the last assignment. (Str_Concat_Bounds_2): Delete. * libgnat/s-conca3.ads (Str_Concat_3): Adjust head comment. (Str_Concat_Bounds_3): Delete. * libgnat/s-conca3.adb (Str_Concat_3): Use the length of the last input to size the last assignment. (Str_Concat_Bounds_3): Delete. * libgnat/s-conca4.ads (Str_Concat_4): Adjust head comment. (Str_Concat_Bounds_4): Delete. * libgnat/s-conca4.adb (Str_Concat_4): Use the length of the last input to size the last assignment. (Str_Concat_Bounds_4): Delete. * libgnat/s-conca5.ads (Str_Concat_5): Adjust head comment. (Str_Concat_Bounds_5): Delete. * libgnat/s-conca5.adb (Str_Concat_5): Use the length of the last input to size the last assignment. (Str_Concat_Bounds_5): Delete. * libgnat/s-conca6.ads (Str_Concat_6): Adjust head comment. (Str_Concat_Bounds_6): Delete. * libgnat/s-conca6.adb (Str_Concat_6): Use the length of the last input to size the last assignment. (Str_Concat_Bounds_6): Delete. * libgnat/s-conca7.ads (Str_Concat_7): Adjust head comment. (Str_Concat_Bounds_7): Delete. * libgnat/s-conca7.adb (Str_Concat_7): Use the length of the last input to size the last assignment. (Str_Concat_Bounds_7): Delete. * libgnat/s-conca8.ads (Str_Concat_8): Adjust head comment. (Str_Concat_Bounds_8): Delete. * libgnat/s-conca8.adb (Str_Concat_8): Use the length of the last input to size the last assignment. (Str_Concat_Bounds_8): Delete. * libgnat/s-conca9.ads (Str_Concat_9): Adjust head comment. (Str_Concat_Bounds_9): Delete. * libgnat/s-conca9.adb (Str_Concat_9): Use the length of the last input to size the last assignment. (Str_Concat_Bounds_9): Delete.
2022-07-12[Ada] Avoid namespace pollution for Next and PreviousBob Duff21-84/+72
This patch renames Next and Previous in a-convec.ads and other containers to be _Next and _Previous, to avoid namespace pollution. The compiler now uses the leading-underscore names to look them up. The scanner is changed to allow this. gcc/ada/ * exp_ch5.adb (Expand_Iterator_Loop_Over_Array): Use _Next and _Previous in the optimized expansion of "for ... of". No longer need to check parameter profiles for these, because the leading-underscore names are unique. * libgnat/a-convec.ads (_Next, _Previous): Renamings of Next and Previous, to avoid namespace pollution. * libgnat/a-cbdlli.ads, libgnat/a-cbhama.ads, libgnat/a-cbhase.ads, libgnat/a-cbmutr.ads, libgnat/a-cborma.ads, libgnat/a-cborse.ads, libgnat/a-cdlili.ads, libgnat/a-cidlli.ads, libgnat/a-cihama.ads, libgnat/a-cihase.ads, libgnat/a-cimutr.ads, libgnat/a-ciorma.ads, libgnat/a-ciorse.ads, libgnat/a-cobove.ads, libgnat/a-cohama.ads, libgnat/a-cohase.ads, libgnat/a-coinve.ads, libgnat/a-comutr.ads, libgnat/a-coorma.ads, libgnat/a-coorse.ads: Likewise. Also, remove duplicated comments -- refer to one comment about _Next, _Previous, Pseudo_Reference in libgnat/a-convec.ads. DRY. * scng.adb (Scan): Allow leading underscores in identifiers in the run-time library. * snames.ads-tmpl (Name_uNext, Name_uPrevious): New names with leading underscores.
2022-07-12[Ada] Add new unbounded and indefinite formal doubly linked listJulien Bortolussi2-0/+3724
Before this patch, the only formal doubly linked lists were bounded and definite. This means that it is necessary to provide their maximum length or capacity at instantiation and that they can only be used with definite element types. The formal lists added by this patch are unbounded and indefinite. Their length grows dynamically until Count_Type'Last. This makes them easier to use but requires the use of dynamic allocation and controlled types. gcc/ada/ * libgnat/a-cfidll.adb, libgnat/a-cfidll.ads: Implementation files of the formal unbounded indefinite list. * Makefile.rtl, impunit.adb: Take into account the add of the new files.
2022-07-06[Ada] Indexing error when calling GNAT.Regpat.MatchJustin Squirek2-20/+42
This patch corrects an error in the compiler whereby a buffer sizing error fails to get raised when compiling a regex expression with an insufficiently sized Pattern_Matcher as the documentation indicated. This, in turn, could lead to indexing errors when attempting to call Match with the malformed regex program buffer. gcc/ada/ * libgnat/s-regpat.adb, libgnat/s-regpat.ads (Compile): Add a new defaulted parameter Error_When_Too_Small to trigger an error, if specified true, when Matcher is too small to hold the compiled regex program.
2022-07-06[Ada] Support ghost generic formal parametersYannick Moy3-23/+46
This adds support in GNAT for ghost generic formal parameters, as included in SPARK RM 6.9. gcc/ada/ * ghost.adb (Check_Ghost_Context): Delay checking for generic associations. (Check_Ghost_Context_In_Generic_Association): Perform ghost checking in analyzed generic associations. (Check_Ghost_Formal_Procedure_Or_Package): Check SPARK RM 6.9(13-14) for formal procedures and packages. (Check_Ghost_Formal_Variable): Check SPARK RM 6.9(13-14) for variables. * ghost.ads: Declarations for the above. * sem_ch12.adb (Analyze_Associations): Apply delayed checking for generic associations. (Analyze_Formal_Object_Declaration): Same. (Analyze_Formal_Subprogram_Declaration): Same. (Instantiate_Formal_Package): Same. (Instantiate_Formal_Subprogram): Same. (Instantiate_Object): Same. Copy ghost aspect to newly declared object for actual for IN formal object. Use new function Get_Enclosing_Deep_Object to retrieve root object. (Instantiate_Type): Copy ghost aspect to declared subtype for actual for formal type. * sem_prag.adb (Analyze_Pragma): Recognize new allowed declarations. * sem_util.adb (Copy_Ghost_Aspect): Copy the ghost aspect between nodes. (Get_Enclosing_Deep_Object): New function to return enclosing deep object (or root for reachable part). * sem_util.ads (Copy_Ghost_Aspect): Same. (Get_Enclosing_Deep_Object): Same. * libgnat/s-imageu.ads: Declare formal subprograms as ghost. * libgnat/s-valuei.ads: Same. * libgnat/s-valuti.ads: Same.
2022-07-06[Ada] Handle secondary stack memory allocations alignmentMarc Poulhiès2-31/+68
To accomodate cases where objects allocated on the secondary stack needed a more constrained alignement than Standard'Maximum_Alignement, the alignment for all allocations in the full runtime were forced on to be aligned on Standard'Maximum_Alignement*2. This changes removes this workaround and correctly handles the over-alignment in all runtimes. This change modifies the SS_Allocate procedure to accept a new Alignment parameter and to dynamically realign the pointer returned by the memory allocation (Allocate_* functions or dedicated stack allocations for zfp/cert). It also simplifies the 0-sized allocations by not allocating any memory if pointer is already correctly aligned (already the case in cert and zfp runtimes). gcc/ada/ * libgnat/s-secsta.ads (SS_Allocate): Add new Alignment parameter. (Memory_Alignment): Remove. * libgnat/s-secsta.adb (Align_Addr): New. (SS_Allocate): Add new Alignment parameter. Realign pointer if needed. Don't allocate anything for 0-sized allocations. * gcc-interface/utils2.cc (build_call_alloc_dealloc_proc): Add allocated object's alignment as last parameter to allocation invocation.
2022-07-06[Ada] Cleanup use of local scalars in GNAT.Socket.Get_Address_InfoPiotr Trojanek1-4/+4
A cleanup opportunity spotted while working on improved detection of uninitialised local scalar objects. gcc/ada/ * libgnat/g-socket.adb (Get_Address_Info): Reduce scope of the Found variable; avoid repeated assignment inside the loop.
2022-07-06[Ada] Remove old vxworks from Makefile.rtl - e500 port.Doug Rupp3-489/+0
The powerpc e500 port has been LTS'd gcc/ada/ * libgnat/system-vxworks7-e500-kernel.ads: Remove. * libgnat/system-vxworks7-e500-rtp-smp.ads: Likewise. * libgnat/system-vxworks7-e500-rtp.ads: Likewise.
2022-07-05[Ada] Annotate GNAT.Sockets with No_Return aspectsPiotr Trojanek2-3/+5
Opportunity for extra annotations spotted while fixing detection of unreachable code that follows calls to procedures annotated with No_Return. gcc/ada/ * libgnat/g-socket.adb (Raise_Host_Error): Add No_Return aspect. (Raise_GAI_Error): Likewise. * libgnat/g-socket.ads (Raise_Socket_Error): Likewise.
2022-07-05[Ada] Remove unnecessary dead code after calls to nonreturning proceduresPiotr Trojanek2-8/+0
A new warning about unreachable code that follows calls to procedures with No_Return would flag some dead defensive code. Comments next to this code suggest that it was added to please some ancient version of the compiler, but recent releases of GNAT do not require such a code. gcc/ada/ * gnatls.adb (Corresponding_Sdep_Entry): Remove dead return statement in defensive path; there is another return statement for a normal execution of this routine, so rule Ada RM 6.5(5), which requires function to have at least one return statement is still satisfied. (Gnatls): Remove dead, call to nonreturning Exit_Program after Output_License_Information which itself does not return. * libgnat/a-exstat.adb (Bad_EO): Remove raise statement that was meant to please some ancient version of GNAT. * libgnat/g-awk.adb (Raise_With_Info): Likewise. * sem_attr.adb (Check_Reference): Remove dead return statement; rule Ada RM 6.5(5), which requires function to have at least one return statement is still satisfied. (Analyze_Attribute): Remove dead exit statement. (Check_Reference): Same as above. * sem_ch12.adb (Instantiate_Formal_Package): Remove dead raise statement; it was inconsistent with other calls to Abandon_Instantiation, which are not followed by a raise statement. * sem_prag.adb (Process_Convention): Remove dead defensive assignment. (Interrupt_State): Remove dead defensive exit statement. (Do_SPARK_Mode): Likewise. * sfn_scan.adb (Scan_String): Remove dead defensive assignment.
2022-07-05[Ada] Combine system.ads files - vxworks6 constants.Doug Rupp3-6/+6
Systemitize Word_Size and Memory_Size declarations rather than hard code with numerical values or OS specific Long_Integer size. gcc/ada/ * libgnat/system-vxworks-ppc-kernel.ads (Word_Size): Compute based on Standard'Word_Size. (Memory_Size): Compute based on Word_Size. * libgnat/system-vxworks-ppc-rtp-smp.ads: Likewise. * libgnat/system-vxworks-ppc-rtp.ads: Likewise.
2022-07-05[Ada] Remove old vxworks6 from Makefile.rtlDoug Rupp9-1468/+0
Pre vxworks7 code excepting legacy vxworks6 code is removed from Makefile.rtl and unused files are deleted. gcc/ada/ * Makefile.rtl (*vxworks*): Remove most pre-vxworks7 code. * vxworks-arm-link.spec: Remove. * vxworks-e500-link.spec: Likewise. * vxworks-smp-arm-link.spec: Likewise. * vxworks-smp-e500-link.spec: Likewise. * vxworks-smp-x86-link.spec: Likewise. * libgnat/system-vxworks-arm-rtp-smp.ads: Likewise. * libgnat/system-vxworks-arm-rtp.ads: Likewise. * libgnat/system-vxworks-arm.ads: Likewise. * libgnat/system-vxworks-e500-kernel.ads: Likewise. * libgnat/system-vxworks-e500-rtp-smp.ads: Likewise. * libgnat/system-vxworks-e500-rtp.ads: Likewise. * libgnat/system-vxworks-x86-kernel.ads: Likewise. * libgnat/system-vxworks-x86-rtp-smp.ads: Likewise. * libgnat/system-vxworks-x86-rtp.ads: Likewise.
2022-07-04[Ada] Single character argument in call to Quote_Argument raises errorJustin Squirek1-1/+1
This patch corrects an issue in the compiler whereby calling Quote_Argument with an argument that is of size 1 may lead to a CONSTRAINT_ERROR raised at runtime due to an undersized buffer. gcc/ada/ * libgnat/s-os_lib.adb (Quote_Argument): Modify the result buffer size calculation to handle the case where Arg'Length is 1.
2022-07-04[Ada] Add Ada 2022 Key function to sets containersBob Duff6-0/+18
This patch adds the new Generic_Keys.Key function to the set children of Ada.Containers. gcc/ada/ * libgnat/a-cbhase.ads, libgnat/a-cborse.ads, libgnat/a-cihase.ads, libgnat/a-ciorse.ads, libgnat/a-cohase.ads, libgnat/a-coorse.ads (Key): New function that takes a Container parameter, implemented as an expression function, so it is self explanatory (doesn't need a comment).
2022-07-04[Ada] Add Ada 2022 features to sets containersBob Duff14-8/+482
This patch adds some Ada 2022 features to the set children of Ada.Containers. gcc/ada/ * libgnat/a-cbhase.adb, libgnat/a-cbhase.ads, libgnat/a-cborse.adb, libgnat/a-cborse.ads, libgnat/a-cihase.adb, libgnat/a-cihase.ads, libgnat/a-ciorse.adb, libgnat/a-ciorse.ads, libgnat/a-cohase.adb, libgnat/a-cohase.ads, libgnat/a-conhel.adb, libgnat/a-conhel.ads, libgnat/a-coorse.adb, libgnat/a-coorse.ads: Add Has_Element, Element, Query_Element, and Next subprograms that take a Set parameter. Add Tampering_With_Cursors_Prohibited function. These are all new in Ada 2022.
2022-07-04[Ada] Create new unbounded functional sequenceJulien Bortolussi2-0/+681
Add a new unbounded functional sequence. This sequence is indexed by Big_Positive and so is unbounded from the user and spark points view. Hower the actually implemented sequence are bounded by Count_Type'Last. gcc/ada/ * libgnat/a-cfinse.adb, libgnat/a-cfinse.ads: Implementation files of the sequence. * Makefile.rtl, impunit.adb: Take into account the add of the new files
2022-06-02[Ada] Rename GNATprove annotate pragma for termination to Always_ReturnClaire Dross3-5/+5
GNATprove changed the name of the pragma Annotate used to verify that a subprogram always returns normally. It is now called Always_Return instead of Terminating. gcc/ada/ * libgnat/s-aridou.adb: Use Always_Return instead of Terminating to annotate termination for GNATprove. * libgnat/s-arit32.adb: Idem. * libgnat/s-spcuop.ads: Idem.
2022-06-02[Ada] Make the functional Maps and Sets unboundedJulien Bortolussi11-49/+100
Before this patch, the Functional Sets ans Maps were bounded both from the user and the implementation points of view. To make them closer to mathematical Sets ans Maps, this patch removes the bounds from the contracts. Note that, in practice, they are still bounded by Count_Type'Last, even if the user is not aware of it anymore. This patch removed constraints on length of sets and maps from the preconditions of functions. The function Length and Num_Overlaps now return a Big_Natural. gcc/ada/ * libgnat/a-cofuse.ads, libgnat/a-cofuse.adb, libgnat/a-cofuma.ads, libgnat/a-cofuma.adb: Make Length and Num_Overlaps return Big_Natural. * libgnat/a-cforse.ads, libgnat/a-cforse.adb, libgnat/a-cforma.adb, libgnat/a-cfhase.ads, libgnat/a-cfhase.adb, libgnat/a-cfhama.adb, libgnat/a-cfdlli.adb: Adapt code to handle Big_Integers instead of Count_Type.
2022-06-02[Ada] vx7r2-arm/aarch64 - Support Atomic Primitives TrueDoug Rupp4-0/+4
This feature is an architecture feature, not an OS feature, so enable on vx7r2 for arm and aarch64 to coincide with what is done on similarly capable targets. gcc/ada/ * libgnat/system-vxworks7-arm.ads (Support_Atomic_Primitives): Set True. * libgnat/system-vxworks7-arm-rtp-smp.ads: Likewise. * libgnat/system-vxworks7-aarch64.ads: Likewise. * libgnat/system-vxworks7-aarch64-rtp-smp.ads: Likewise:
2022-06-02[Ada] Update documentation of GNAT.Dynamic_TablesJavier Miranda1-7/+4
Document that dynamic tables are defined aliased for backward compatibility. gcc/ada/ * libgnat/g-dyntab.ads (Table_Type): Update documentation.
2022-06-02[Ada] Fix preconditions of Interfaces.C.StringsJoffrey Huguet1-2/+8
Preconditions of Update procedures were always true when Offset was 0. The changes enable to protect from Update_Error when Offset is 0. gcc/ada/ * libgnat/i-cstrin.ads (Update): Update precondition.
2022-06-02[Ada] Complete contracts of Interfaces.C.Strings subprogramsJoffrey Huguet1-3/+8
This patch adds preconditions to Update procedures, to protect from Update_Error propagations. gcc/ada/ * libgnat/i-cstrin.ads (Update): Add precondition.
2022-06-02[Ada] Combine system.ads files - arm and aarch64 linuxDoug Rupp1-1/+1
Systemitize Word_Size and Memory_Size declarations rather than hard code with numerical values or OS specific Long_Integer size. gcc/ada/ * libgnat/system-linux-arm.ads (Memory_Size): Compute based on Word_Size.
2022-06-02[Ada] Combine system.ads file - vxworks7 rtp constantsDoug Rupp9-18/+18
Systemitize Word_Size and Memory_Size declarations rather than hard code with numerical values or OS specific Long_Integer size. gcc/ada/ * libgnat/system-vxworks7-aarch64-rtp-smp.ads (Word_Size): Compute based on Standard'Word_Size. (Memory_Size): Compute based on Word_Size. * libgnat/system-vxworks7-arm-rtp-smp.ads: Likewise. * libgnat/system-vxworks7-e500-rtp-smp.ads: Likewise. * libgnat/system-vxworks7-e500-rtp.ads: Likewise. * libgnat/system-vxworks7-ppc-rtp-smp.ads: Likewise. * libgnat/system-vxworks7-ppc-rtp.ads: Likewise. * libgnat/system-vxworks7-ppc64-rtp-smp.ads: Likewise. * libgnat/system-vxworks7-x86-rtp-smp.ads: Likewise. * libgnat/system-vxworks7-x86-rtp.ads: Likewise.
2022-06-02[Ada] Fix iteration on formal vectorsClaire Dross4-4/+4
We need to use Extended_Index for the Position parameter of the Element function in formal vectors so it is compatible with other primitives of the Iterable aspect. gcc/ada/ * libgnat/a-cfinve.ads (Element): Change the type of the Position parameter to Extended_Index. * libgnat/a-cfinve.adb (Element): Idem. * libgnat/a-cofove.ads (Element): Idem. * libgnat/a-cofove.adb (Element): Idem.
2022-06-02[Ada] Add contracts to System.Address_To_Access_ConversionsJoffrey Huguet1-2/+4
This patch adds SPARK annotations to subprograms from System.Address_To_Access_Conversions. To_Pointer is considered to have no global items, if the returned value has no aliases. To_Address is forbidden in SPARK because addresses are not handled. gcc/ada/ * libgnat/s-atacco.ads (To_Pointer): Add Global => null. (To_Address): Add SPARK_Mode => Off.
2022-06-02[Ada] Add contracts to Interfaces.C.StringsJoffrey Huguet2-16/+57
This patch adds Global contracts and preconditions to subprograms of Interfaces.C.Strings. Effects on allocated memory are modelled through an abstract state, C_Memory. The preconditions protect against Dereference_Error, but not Storage_Error (which is not handled by SPARK). This patch also disables the use of To_Chars_Ptr, which creates an alias between an ownership pointer and the abstract state, and the use of Free, in SPARK code. Thus, memory leaks will happen if the user creates the Chars_Ptr using New_Char_Array and New_String. gcc/ada/ * libgnat/i-cstrin.ads (To_Chars_Ptr): Add SPARK_Mode => Off. (Free): Likewise. (New_Char_Array): Add global contracts and Volatile attribute. (New_String): Likewise. (Value, Strlen, Update): Add global contracts and preconditions. * libgnat/i-cstrin.adb: Add SPARK_Mode => Off to the package body.
2022-06-01[Ada] Combine system.ads file - vxworks7 kernel constants.Doug Rupp7-14/+14
Systemitize Word_Size and Memory_Size declarations rather than hard code with numerical values or OS specific Long_Integer size. gcc/ada/ * libgnat/system-vxworks7-aarch64.ads (Word_Size): Compute based on Standard'Word_Size. (Memory_Size): Compute based on Word_Size. * libgnat/system-vxworks7-arm.ads: Likewise. * libgnat/system-vxworks7-e500-kernel.ads: Likewise. * libgnat/system-vxworks7-ppc-kernel.ads: Likewise. * libgnat/system-vxworks7-ppc64-kernel.ads: Likewise. * libgnat/system-vxworks7-x86-kernel.ads: Likewise. * libgnat/system-vxworks7-x86_64-kernel.ads: Likewise.
2022-06-01[Ada] Combine system.ads files - arm and aarch64 qnxDoug Rupp1-1/+1
Systemitize Word_Size and Memory_Size declarations rather than hard code with numerical values or OS specific Long_Integer size. gcc/ada/ * libgnat/system-qnx-arm.ads (Memory_Size): Compute based on Word_Size.
2022-06-01[Ada] Bug fix in "=" function of formal doubly linked listJulien Bortolussi1-2/+2
Correction of a typo regarding indexes. gcc/ada/ * libgnat/a-cfdlli.adb ("="): Make the function properly loop over the right list.
2022-06-01[Ada] Add reference counting in functional containersJulien Bortolussi2-52/+227
This patch adds reference counting to dynamically allocated pointers on arrays and elements used by the functional container. This is done by making both the arrays and the elements controlled. gcc/ada/ * libgnat/a-cofuba.ads, libgnat/a-cofuba.adb: Add reference counting.
2022-05-30[Ada] Remove contract duplication in formal doubly linked listsJulien Bortolussi1-9/+1
Remove a minor duplication in Post of a function of formal doubly linked lists. gcc/ada/ * libgnat/a-cfdlli.ads (Insert): Remove the duplication.
2022-05-30[Ada] Fix illegal Ada in s-dwalin.adbRomain Beguet1-0/+2
Both the `System.Mmap` and `System.Object_Reader` packages are defining entities named `Offset` and they are both `use`d at the top of s-dwalin.adb. Therefore, the references to `Offset` throughout this file are ambiguous, and GNAT is supposed to complain. Since it does not for the moment, we fix the ambiguity by declaring a subtype `Offset` at the top of the file simply renames `System.Object_Reader.Offset`. gcc/ada/ * libgnat/s-dwalin.adb: Add a subtype declaration to fix the ambiguity.
2022-05-30[Ada] Update proofs of double arithmetic unit after prover changesYannick Moy4-91/+576
Changes in GNATprove (translation to Why3 and provers) result in proofs being much less automatic, and requiring ghost code to detail intermediate steps. In some cases, it is better to use the new By mechanism to prove assertions in steps, as this avoids polluting the proof context for other proofs. For that reason, add units s-spark.ads and s-spcuop.ads/b to the runtime sources. gcc/ada/ * Makefile.rtl: Add new units. * libgnat/s-aridou.adb (Scaled_Divide): Add ghost code for provers. * libgnat/s-spcuop.adb: New unit for ghost cut operations. * libgnat/s-spcuop.ads: New unit for ghost cut operations. * libgnat/s-spark.ads: New unit.
2022-05-30[Ada] Fix typo in comment for functional setsPiotr Trojanek1-1/+1
Minor fix in a recently added comment. gcc/ada/ * libgnat/a-cofuse.ads (Empty_Set): Fix typo in comment.
2022-05-30[Ada] Adapt proof of runtime unit s-arit32Yannick Moy1-1/+1
After changes in GNATprove, adapt proof. Simply move an assertion up before it is first needed here. gcc/ada/ * libgnat/s-arit32.adb (Scaled_Divide32): Move assertion up.
2022-05-30[Ada] PR ada/105303 Fix use of Assertion_Policy in internal generics unitYannick Moy2-11/+77
The internal unit System.Generic_Array_Operations defines only generic subprograms. Thus, pragma Assertion_Policy inside the spec has no effect, as each instantiation is only subject to the assertion policy at the program point of the instantiation. Remove this confusing pragma, and add the pragma inside each generic body making use of additional assertions or ghost code, so that running time of instantiations is not impacted by assertions meant for formal verification. gcc/ada/ PR ada/105303 * libgnat/s-gearop.adb: Add pragma Assertion_Policy in generic bodies making use of additional assertions or ghost code. * libgnat/s-gearop.ads: Remove confusing Assertion_Policy.
generated by cgit v1.1 at 2024-07-21 04:22:39 +0000