aboutsummaryrefslogtreecommitdiff
path: root/gcc/ada/libgnat
AgeCommit message (Collapse)AuthorFilesLines
2024-01-22Update copyright years.Marc Poulhiès1475-1475/+1475
2024-01-09ada: Remove unused runtime entityEric Botcazou2-18/+0
The compiler has not generated direct attachments for a long time. gcc/ada/ * rtsfind.ads (RE_Id): Remove RE_Attach. (RE_Unit_Table): Likewise. * libgnat/s-finmas.ads (Attach): Delete. * libgnat/s-finmas.adb (Attach): Likewise.
2024-01-09ada: Add __atomic_store_n binding to System.Atomic_PrimitivesEric Botcazou2-0/+25
This is modeled on the existing binding for __atomic_load_n. gcc/ada/ * libgnat/s-atopri.ads (Atomic_Store): New generic procedure. (Atomic_Store_8): New instantiated procedure. (Atomic_Store_16): Likewise. (Atomic_Store_32): Likewise. (Atomic_Store_64): Likewise. * libgnat/s-atopri__32.ads (Atomic_Store): New generic procedure. (Atomic_Store_8): New instantiated procedure. (Atomic_Store_16): Likewise. (Atomic_Store_32): Likewise. * gcc-interface/decl.cc (gnat_to_gnu_subprog_type): Implement the support for __atomic_store_n and __sync_bool_compare_and_swap_n. * gcc-interface/gigi.h (list_second): New inline function.
2024-01-09ada: Fix precondition in Interfaces.C.StringsJoffrey Huguet1-4/+5
The precondition of both Update procedures in Interfaces.C.Strings were incorrect. This patch fixes this. gcc/ada/ * libgnat/i-cstrin.ads (Update): Fix precondition.
2024-01-09Fix outdated commentEric Botcazou1-5/+4
gcc/ada/ PR ada/78207 * libgnat/g-regexp.ads: Fix outdated comment.
2023-12-19ada: Remove GNATcheck violationsSheri Bernstein1-10/+8
Remove GNATcheck violations by refactoring code and also using pragma Annotate to exempt them. gcc/ada/ * libgnat/a-comlin.adb (Argument_Count): Rewrite code so there is only one return, to remove Improper_Returns violation. (Command_Name): Add pragma to exempt Improper_Returns violation.
2023-12-19ada: Optimize performance and remove dynamic frame requirement.Vasiliy Fofanov1-7/+10
gcc/ada/ * libgnat/i-cstrin.adb (Value): Optimize.
2023-12-19ada: Remove No_Dynamic_Priorities from Restricted_TaskingJohannes Kliemann1-1/+0
Some of our restricted runtimes support dynamic priorities. The binder needs to generate code for a restricted runtime even if the restriction No_Dynamic_Priorities is not in place. gcc/ada/ * libgnat/s-rident.ads: Remove No_Dynamic_Priorities from Restricted_Tasking.
2023-11-30ada: Remove GNATcheck violationsSheri Bernstein1-5/+19
Remove GNATcheck violations by refactoring code and also using pragma Annotate to exempt them. gcc/ada/ * libgnat/i-cstrin.adb (Free): Rewrite code so there is only one return, to remove Improper_Returns violation. (Position_Of_Nul): Add pragma to exempt Improper_Returns violation. (To_Chars_Ptr): Likewise. (Value): Likewise
2023-11-28ada: Remove dependency on System.Val_Bool in System.Img_BoolYannick Moy4-37/+40
In order to facilitate the certification of System.Img_Bool, remove its dependency on unit System.Val_Bool. Modify the definition of ghost function Is_Boolean_Image_Ghost to take the expected boolean value and move it to System.Val_Spec. gcc/ada/ * libgnat/s-imgboo.adb: Remove with_clause now in spec file. * libgnat/s-imgboo.ads: Remove dependency on System.Val_Bool. (Image_Boolean): Replace call to Value_Boolean by passing value V to updated ghost function Is_Boolean_Image_Ghost. * libgnat/s-valboo.ads (Is_Boolean_Image_Ghost): Move to other unit. (Value_Boolean.): Update precondition. * libgnat/s-valspe.ads (Is_Boolean_Image_Ghost): Move here. Add new parameter for expected boolean value.
2023-11-21ada: Fix string indexing within GNAT.Calendar.Time_IO.ValueJustin Squirek1-2/+2
The patch fixes an issue in the compiler whereby calls to GNAT.Calendar.Time_IO.Value where the actual for formal String Date with indexing starting at any value besides one would result in a spurious runtime exception. gcc/ada/ * libgnat/g-catiio.adb (Value): Modify conditionals to use 'Last instead of 'Length
2023-11-21ada: Runtime recompilation instructions improvements.Doug Rupp1-6/+7
Revise instructions to work on both cross and native targets hosted on Linux gcc/ada/ * libgnat/libada.gpr: Revise section 1
2023-11-21ada: Fix Ada.Text_IO.Delete with "encoding=8bits" formRonan Desplanques4-4/+14
Before this patch, on Windows, file with non-ASCII Latin1 names could be created with Ada.Text_IO.Create by passing "encoding=8bits" through the Form parameter and a Latin1-encoded string through the Name parameter, but calling Ada.Text_IO.Delete on them raised an illegitimate exception. This patch fixes this by making the wrappers of the unlink system function aware of the encoding value passed through the Form parameter. It also removes an unnecessary curly-brace block. gcc/ada/ * adaint.c (__gnat_unlink): Add new parameter and fix text conversion on Windows. Remove unnecessary curly braces. * adaint.h (__gnat_unlink): Add new parameter. * libgnat/i-cstrea.ads (unlink): Adapt to __gnat_unlink signature change. * libgnat/i-cstrea.adb (unlink): New Subprogram definition. * libgnat/s-crtl.ads (unlink): Adapt to __gnat_unlink signature change. * libgnat/s-fileio.adb (Delete): Pass encoding argument to unlink.
2023-11-21ada: Always use -gnatg in run-time GPR filesRonan Desplanques1-1/+1
This patch makes it so -gnatg is always passed to the compiler when rebuilding the run-time library with the dedicated GPR files. Before this patch, if a user rebuilt the run-time with -XADAFLAGS=XXX where XXX didn't include "-gnatg", the build would immediately fail. This case occurs when following the instructions in libada.gpr, which use '-XADAFLAGS="-gnatn"'. gcc/ada/ * libgnat/libgnat_common.gpr: Unconditionally pass -gnatg.
2023-11-09Fix PR ada/111813 (Inconsistent limit in Ada.Calendar.Formatting)Simon Wright1-3/+8
The description of the second Value function (returning Duration) (ARM 9.6.1(87) doesn't place any limitation on the Elapsed_Time parameter's value, beyond "Constraint_Error is raised if the string is not formatted as described for Image, or the function cannot interpret the given string as a Duration value". It would seem reasonable that Value and Image should be consistent, in that any string produced by Image should be accepted by Value. Since Image must produce a two-digit representation of the Hours, there's an implication that its Elapsed_Time parameter should be less than 100.0 hours (the ARM merely says that in that case the result is implementation-defined). The current implementation of Value raises Constraint_Error if the Elapsed_Time parameter is greater than or equal to 24 hours. This patch removes the restriction, so that the Elapsed_Time parameter must only be less than 100.0 hours. 2023-10-15 Simon Wright <simon@pushface.org> PR ada/111813 gcc/ada/ * libgnat/a-calfor.adb (Value (2)): Allow values of parameter Elapsed_Time greater than or equal to 24 hours, by doing the hour calculations in Natural rather than Hour_Number (0 .. 23). Calculate the result directly rather than by using Seconds_Of (whose Hour parameter is of type Hour_Number). If an exception occurs of type Constraint_Error, re-raise it rather than raising a new CE. gcc/testsuite/ * gnat.dg/calendar_format_value.adb: New test.
2023-11-07ada: Fix extra whitespace after END keywordsPiotr Trojanek2-2/+2
Style cleanup. gcc/ada/ * exp_pakd.adb, libgnarl/s-osinte__android.ads, libgnarl/s-osinte__linux.ads, libgnarl/s-osinte__qnx.ads, libgnarl/s-osinte__rtems.ads, libgnat/s-gearop.adb, libgnat/s-poosiz.adb, sem_util.adb: Fix style.
2023-10-19ada: Refactor code to remove GNATcheck violationSheri Bernstein1-35/+40
Rewrite for loop containing an exit (which violates GNATcheck rule Exits_From_Conditional_Loops), to use a while loop which contains the exit criteria in its condition. Also, move special case of first time through loop, to come before loop. gcc/ada/ * libgnat/s-imagef.adb (Set_Image_Fixed): Refactor loop.
2023-10-19ada: Add pragma Annotate for GNATcheck exemptionsSheri Bernstein1-0/+8
Exempt the GNATcheck rule "Unassigned_OUT_Parameters" with the rationale "the OUT parameter is assigned by component". gcc/ada/ * libgnat/s-imguti.adb (Set_Decimal_Digits): Add pragma to exempt Unassigned_OUT_Parameters. (Set_Floating_Invalid_Value): Likewise
2023-10-10ada: Tweak internal subprogram in Ada.DirectoriesRonan Desplanques1-21/+25
The purpose of this patch is to work around false-positive warnings emitted by GNAT SAS (also known as CodePeer). It does not change the behavior of the modified subprogram. gcc/ada/ * libgnat/a-direct.adb (Start_Search_Internal): Tweak subprogram body.
2023-10-10ada: Fix filesystem entry filteringRonan Desplanques1-14/+16
This patch fixes the behavior of Ada.Directories.Search when being requested to filter out regular files or directories. One of the configurations in which that behavior was incorrect was that when the caller requested only the regular and special files but not the directories, the directories would still be returned. gcc/ada/ * libgnat/a-direct.adb: Fix filesystem entry filtering.
2023-09-26ada: Fix conversions between addresses and integersDaniel King2-5/+6
On CHERI targets the size of System.Address and Integer_Address (or similar) are not the same. The operations in System.Storage_Elements should be used to convert between integers and addresses. gcc/ada/ * libgnat/a-tags.adb (To_Tag): Use System.Storage_Elements for integer to address conversion. * libgnat/s-putima.adb (Put_Image_Pointer): Likewise.
2023-09-26ada: Add CHERI variant of System.Stream_AttributesDaniel King1-0/+1019
Reading and writing System.Address to a stream on CHERI targets does not preserve the capability tag; it will always be invalid since a valid capability cannot be created out of thin air. Reading an Address from a stream would therefore never yield a capability that can be dereferenced. This patch introduces a CHERI variant of System.Stream_Attributes that raises Program_Error when attempting to read a System.Address from a stream. gcc/ada/ * libgnat/s-stratt__cheri.adb: New file
2023-09-26ada: Define CHERI exception typesDaniel King1-0/+16
These exception types map to the CHERI hardware exceptions that are triggered due to misuse of capabilities. gcc/ada/ * libgnat/i-cheri.ads (Capability_Bound_Error) (Capability_Permission_Error, Capability_Sealed_Error) (Capability_Tag_Error): New, define CHERI exception types.
2023-09-05ada: Remove TBC comment, no more neededLiaiss Merzougue1-1/+0
gcc/ada/ * libgnat/s-imguti.adb: Remove comment.
2023-09-05ada: Pass -msmp when linking for ppc-vx6 --RTS=rtp-smpAlexandre Oliva1-0/+1
gprbuild and gnatmake won't pass --RTS=rtp-smp to the compiler driver for linking. The flag was not used during linking: the .spec files named as linker options were all we passed for the linker to get the -L flags for lib_smp and lib. There was a problem, though: although /lib_smp/ and /lib/ were to be searched in this order, and the specs files did that correctly, the compiler would search /lib/ first regardless, because STARTFILE_PREFIX_SPEC said so, and specs files cannot override that. With this patch, we make sure the rtp-smp runtime causes -msmp to be added to the command line passed to the compiler driver for linking, and a corresponding patch for the ppc-vxworks configuration makes the GCC compiler driver use this flag to select /lib_smp/ rather than /lib/. gcc/ada/ * libgnat/system-vxworks-ppc-rtp-smp.ads: Add -msmp to Linker_Options pragma.
2023-09-05ada: Preserve capability validity in address arithmeticDaniel King11-65/+76
On CHERI targets where System.Address is a capability, arithmetic on addresses should avoid converting to integers and instead use the operations defined in System.Storage_Elements to perform the arithmetic directly on the System.Address object. This preserves the capability's validity throughout the calculation, ensuring that the resulting capability can be dereferenced. gcc/ada/ * libgnat/s-carsi8.adb: Use operations from System.Storage_Elements for address arithmetic. * libgnat/s-carun8.adb: Likewise * libgnat/s-casi128.adb: Likewise * libgnat/s-casi16.adb: Likewise * libgnat/s-casi32.adb: Likewise * libgnat/s-casi64.adb: Likewise * libgnat/s-caun128.adb: Likewise * libgnat/s-caun16.adb: Likewise * libgnat/s-caun32.adb: Likewise * libgnat/s-caun64.adb: Likewise * libgnat/s-geveop.adb: Likewise
2023-09-05ada: Remove GNATcheck violationsSheri Bernstein2-0/+14
Use pragma Annotate to exempt GNATcheck violations that are related to proof code. Specifically, exempt rules "Metrics_LSLOC" and "Metrics_Cyclomatic_Complexity" whose limits are exceeded due to proof code, and exempt rule "Discriminated_Records" for a variant record that is only used in proof code. gcc/ada/ * libgnat/s-aridou.adb: Add pragma to exempt Metrics_LSLOC. (Double_Divide): Add pragma to exempt Metrics_Cyclomatic_Complexity. (Scaled_Divide): Likewise. * libgnat/s-vauspe.ads (Uns_Option): Add pragma to exempt Discriminated_Records.
2023-09-05ada: Handle GNATcheck violationsSheri Bernstein2-0/+15
For the GNATcheck rule "Improper_Returns", either use pragma Annotate to exempt the violation with the rationale "early returns for performance", or refactor the code by replacing multiple returns by a single return statement with a conditional expression; this is more readable and maintainable, and also conformant with a Highly Recommended design principle of ISO 26262-6. For the GNATcheck rule "Discriminated_Records", use pragma Annotate to exempt the violation with the rationale "only variant records are disallowed". gcc/ada/ * libgnarl/a-reatim.adb (Time_Of): Add pragma to exempt Discriminated_Records. * libgnat/s-imguti.adb (Round, Set_Decimal_Digits): Likewise. * libgnat/s-multip.adb (Number_Of_CPUs): Likewise. * libgnarl/s-tpopsp__posix-foreign.adb (Self): Refactor multiple returns.
2023-09-05LoongArch: initial ada support on linuxYang Yujie1-0/+145
gcc/ada/ChangeLog: * Makefile.rtl: Add LoongArch support. * libgnarl/s-linux__loongarch.ads: New file. * libgnat/system-linux-loongarch.ads: New file. gcc/ChangeLog: * config/loongarch/loongarch.h (CC1_SPEC): Mark normalized options passed from driver to gnat1 as explicit for multilib.
2023-08-07ada: Refactor multiple returnsSheri Bernstein1-15/+15
Replace multiple returns by a single return statement with a conditional expression. This is more readable and maintainable, and also conformant with a Highly Recommended design principle of ISO 26262-6. gcc/ada/ * libgnat/s-parame__qnx.adb: Refactor multiple returns.
2023-08-07ada: Extend precondition of Interfaces.C.String.Value with LengthPiotr Trojanek1-4/+4
The existing precondition guarded against exception Dereference_Error, but not against Constraint_Error. The RM rule B.3.1(36/3) only mentions Constraint_Error for the Value function which returns char_array, but the one which returns String has the same restriction, because it is equivalent to calling the variant which returns char_array and then converted. gcc/ada/ * libgnat/i-cstrin.ads (Value): Extend preconditions; adapt comment for the package.
2023-08-03ada: Add pragma Annotate for GNATcheck exemptionsSheri Bernstein15-0/+66
Exempt the GNATcheck rule "Improper_Returns" with the rationale "early returns for performance". gcc/ada/ * libgnat/s-aridou.adb: Add pragma to exempt Improper_Returns. * libgnat/s-atopri.adb (Lock_Free_Try_Write): Likewise. * libgnat/s-bitops.adb (Bit_Eq): Likewise. * libgnat/s-carsi8.adb: Likewise. * libgnat/s-carun8.adb: Likewise. * libgnat/s-casi16.adb: Likewise. * libgnat/s-casi32.adb: Likewise. * libgnat/s-casi64.adb: Likewise. * libgnat/s-caun16.adb: Likewise. * libgnat/s-caun32.adb: Likewise. * libgnat/s-caun64.adb: Likewise. * libgnat/s-exponn.adb: Likewise. * libgnat/s-expont.adb: Likewise. * libgnat/s-valspe.adb: Likewise. * libgnat/s-vauspe.adb: Likewise.
2023-08-03ada: Rewrite Set_Image_*_Unsigned routines to remove recursion.Vasiliy Fofanov2-100/+55
This rewriting removes algorithm inefficiencies due to unnecessary recursion and copying. The new version has much smaller and statically known stack requirements and is additionally up to 2x faster. gcc/ada/ * libgnat/s-imageb.adb (Set_Image_Based_Unsigned): Rewritten. * libgnat/s-imagew.adb (Set_Image_Width_Unsigned): Likewise.
2023-08-03ada: Adjust again address arithmetics in System.Dwarf_LinesEric Botcazou1-2/+6
Using the operator of System.Storage_Elements has introduced a range check that may be tripped on, so this removes the intermediate conversion to the Storage_Count subtype that is responsible for it. gcc/ada/ * libgnat/s-dwalin.adb ("-"): New subtraction operator. (Enable_Cache): Use it to compute the offset. (Symbolic_Address): Likewise.
2023-07-28ada: Add support for binding to a specific network interface controller.Pascal Obry2-2/+29
gcc/ada/ * s-oscons-tmplt.c: Add support for SO_BINDTODEVICE constant. * libgnat/g-socket.ads (Set_Socket_Option): Handle SO_BINDTODEVICE option. (Get_Socket_Option): Handle SO_BINDTODEVICE option. * libgnat/g-socket.adb: Likewise. (Get_Socket_Option): Handle the case where IF_NAMESIZE is not defined and so equal to -1.
2023-07-28ada: Fix typo in comment of Ada.Exceptions.Save_OccurrencePiotr Trojanek1-1/+1
Minor typo in comment. gcc/ada/ * libgnat/a-except.ads (Save_Occurrence): Fix typo.
2023-07-18ada: Expose expected_throw attributeAlexandre Oliva2-0/+118
Mark exception-raising subprograms with expected_throw attribute. Document the use of the attribute in Control Flow Redundancy. Enable marking subprograms as expected_throw with Machine_Attribute pragmas. gcc/ada/ * libgnat/a-except.ads (Raise_Exception): Mark expected_throw. (Reraise_Occurrence): Likewise. (Raise_Exception_Always): Likewise. (Raise_From_Controlled_Operation): Likewise. (Reraise_Occurrence_Always): Likewise. (Reraise_Occurrence_No_Defer): Likewise. * libgnat/a-except.adb (Exception_Propagation.Propagate_Exception): Likewise. (Complete_And_Propagate_Occurrence): Likewise. (Raise_Exception_No_Defer): Likewise. (Raise_From_Signal_Handler): Likewise. (Raise_With_Msg): Likewise. (Raise_With_Location_And_Msg): Likewise. (Raise_Constraint_Error): Likewise. (Raise_Constraint_Error_Msg): Likewise. (Raise_Program_Error): Likewise. (Raise_Program_Error_Msg): Likewise. (Raise_Storage_Error): Likewise. (Raise_Storage_Error_Msg): Likewise. (Reraise, Rcheck_*): Likewise. * doc/gnat_rm/security_hardening_features.rst (Control Flow Hardening): Note the influence of expected_throw. * gnat_rm.texi: Regenerate. * gnat_ugn.texi: Regenerate. * gcc-interface/utils.cc (handle_expected_throw_attribute): New. (gnat_internal_attribute_table): Add expected_throw.
2023-07-18ada: Refactor s-pack* units to remove multiple returnsVasiliy Fofanov120-4248/+4071
The aim of this refactoring is to replace multiple returns from branches of case and if statements by a single return statement with a conditional expression. This is more readable and maintainable, and also conformant with a Highly Recommended design principle of ISO 26262-6. gcc/ada/ * libgnat/s-pack03.adb: Update copyright year; refactor return statements. * libgnat/s-pack05.adb: Likewise. * libgnat/s-pack06.adb: Likewise. * libgnat/s-pack07.adb: Likewise. * libgnat/s-pack09.adb: Likewise. * libgnat/s-pack10.adb: Likewise. * libgnat/s-pack100.adb: Likewise. * libgnat/s-pack101.adb: Likewise. * libgnat/s-pack102.adb: Likewise. * libgnat/s-pack103.adb: Likewise. * libgnat/s-pack104.adb: Likewise. * libgnat/s-pack105.adb: Likewise. * libgnat/s-pack106.adb: Likewise. * libgnat/s-pack107.adb: Likewise. * libgnat/s-pack108.adb: Likewise. * libgnat/s-pack109.adb: Likewise. * libgnat/s-pack11.adb: Likewise. * libgnat/s-pack110.adb: Likewise. * libgnat/s-pack111.adb: Likewise. * libgnat/s-pack112.adb: Likewise. * libgnat/s-pack113.adb: Likewise. * libgnat/s-pack114.adb: Likewise. * libgnat/s-pack115.adb: Likewise. * libgnat/s-pack116.adb: Likewise. * libgnat/s-pack117.adb: Likewise. * libgnat/s-pack118.adb: Likewise. * libgnat/s-pack119.adb: Likewise. * libgnat/s-pack12.adb: Likewise. * libgnat/s-pack120.adb: Likewise. * libgnat/s-pack121.adb: Likewise. * libgnat/s-pack122.adb: Likewise. * libgnat/s-pack123.adb: Likewise. * libgnat/s-pack124.adb: Likewise. * libgnat/s-pack125.adb: Likewise. * libgnat/s-pack126.adb: Likewise. * libgnat/s-pack127.adb: Likewise. * libgnat/s-pack13.adb: Likewise. * libgnat/s-pack14.adb: Likewise. * libgnat/s-pack15.adb: Likewise. * libgnat/s-pack17.adb: Likewise. * libgnat/s-pack18.adb: Likewise. * libgnat/s-pack19.adb: Likewise. * libgnat/s-pack20.adb: Likewise. * libgnat/s-pack21.adb: Likewise. * libgnat/s-pack22.adb: Likewise. * libgnat/s-pack23.adb: Likewise. * libgnat/s-pack24.adb: Likewise. * libgnat/s-pack25.adb: Likewise. * libgnat/s-pack26.adb: Likewise. * libgnat/s-pack27.adb: Likewise. * libgnat/s-pack28.adb: Likewise. * libgnat/s-pack29.adb: Likewise. * libgnat/s-pack30.adb: Likewise. * libgnat/s-pack31.adb: Likewise. * libgnat/s-pack33.adb: Likewise. * libgnat/s-pack34.adb: Likewise. * libgnat/s-pack35.adb: Likewise. * libgnat/s-pack36.adb: Likewise. * libgnat/s-pack37.adb: Likewise. * libgnat/s-pack38.adb: Likewise. * libgnat/s-pack39.adb: Likewise. * libgnat/s-pack40.adb: Likewise. * libgnat/s-pack41.adb: Likewise. * libgnat/s-pack42.adb: Likewise. * libgnat/s-pack43.adb: Likewise. * libgnat/s-pack44.adb: Likewise. * libgnat/s-pack45.adb: Likewise. * libgnat/s-pack46.adb: Likewise. * libgnat/s-pack47.adb: Likewise. * libgnat/s-pack48.adb: Likewise. * libgnat/s-pack49.adb: Likewise. * libgnat/s-pack50.adb: Likewise. * libgnat/s-pack51.adb: Likewise. * libgnat/s-pack52.adb: Likewise. * libgnat/s-pack53.adb: Likewise. * libgnat/s-pack54.adb: Likewise. * libgnat/s-pack55.adb: Likewise. * libgnat/s-pack56.adb: Likewise. * libgnat/s-pack57.adb: Likewise. * libgnat/s-pack58.adb: Likewise. * libgnat/s-pack59.adb: Likewise. * libgnat/s-pack60.adb: Likewise. * libgnat/s-pack61.adb: Likewise. * libgnat/s-pack62.adb: Likewise. * libgnat/s-pack63.adb: Likewise. * libgnat/s-pack65.adb: Likewise. * libgnat/s-pack66.adb: Likewise. * libgnat/s-pack67.adb: Likewise. * libgnat/s-pack68.adb: Likewise. * libgnat/s-pack69.adb: Likewise. * libgnat/s-pack70.adb: Likewise. * libgnat/s-pack71.adb: Likewise. * libgnat/s-pack72.adb: Likewise. * libgnat/s-pack73.adb: Likewise. * libgnat/s-pack74.adb: Likewise. * libgnat/s-pack75.adb: Likewise. * libgnat/s-pack76.adb: Likewise. * libgnat/s-pack77.adb: Likewise. * libgnat/s-pack78.adb: Likewise. * libgnat/s-pack79.adb: Likewise. * libgnat/s-pack80.adb: Likewise. * libgnat/s-pack81.adb: Likewise. * libgnat/s-pack82.adb: Likewise. * libgnat/s-pack83.adb: Likewise. * libgnat/s-pack84.adb: Likewise. * libgnat/s-pack85.adb: Likewise. * libgnat/s-pack86.adb: Likewise. * libgnat/s-pack87.adb: Likewise. * libgnat/s-pack88.adb: Likewise. * libgnat/s-pack89.adb: Likewise. * libgnat/s-pack90.adb: Likewise. * libgnat/s-pack91.adb: Likewise. * libgnat/s-pack92.adb: Likewise. * libgnat/s-pack93.adb: Likewise. * libgnat/s-pack94.adb: Likewise. * libgnat/s-pack95.adb: Likewise. * libgnat/s-pack96.adb: Likewise. * libgnat/s-pack97.adb: Likewise. * libgnat/s-pack98.adb: Likewise. * libgnat/s-pack99.adb: Likewise.
2023-07-10ada: Simplify assertion to remove CodePeer messageYannick Moy1-3/+1
CodePeer is correctly warning on a test always true in an assertion. It can be rewritten without loss of proof to avoid that message. gcc/ada/ * libgnat/s-aridou.adb (Lemma_Powers_Of_2_Commutation): Rewrite assertion.
2023-07-10ada: Adapt proof of System.Arith_Double to remove CVC4Yannick Moy1-9/+75
The proof of System.Arith_Double still required the use of CVC4, now replaced by its successor cvc5. Adapt the proof to be able to remove CVC4 in the proof of run-time units. gcc/ada/ * libgnat/s-aridou.adb (Lemma_Div_Mult): New simple lemma. (Lemma_Powers_Of_2_Commutation): State post in else branch. (Lemma_Div_Pow2): Introduce local lemma and use it. (Scaled_Divide): Use cut operations in assertions, lemmas, new assertions. Introduce local lemma and use it.
2023-07-06ada: Refactor the proof of the Value and Image runtime unitsClaire Dross37-729/+828
The aim of this refactoring is to avoid unnecessary dependencies between Image and Value units even though they share the same specification functions. These functions are grouped inside ghost packages which are then withed by Image and Value units. gcc/ada/ * libgnat/s-vs_int.ads: Instance of Value_I_Spec for Integer. * libgnat/s-vs_lli.ads: Instance of Value_I_Spec for Long_Long_Integer. * libgnat/s-vsllli.ads: Instance of Value_I_Spec for Long_Long_Long_Integer. * libgnat/s-vs_uns.ads: Instance of Value_U_Spec for Unsigned. * libgnat/s-vs_llu.ads: Instance of Value_U_Spec for Long_Long_Unsigned. * libgnat/s-vslllu.ads: Instance of Value_U_Spec for Long_Long_Long_Unsigned. * libgnat/s-imagei.ads: Take instances of Value_*_Spec as parameters. * libgnat/s-imagei.adb: Idem. * libgnat/s-imageu.ads: Idem. * libgnat/s-imageu.adb: Idem. * libgnat/s-valuei.ads: Idem. * libgnat/s-valuei.adb: Idem. * libgnat/s-valueu.ads: Idem. * libgnat/s-valueu.adb: Idem. * libgnat/s-imgint.ads: Adapt instance to new ghost parameters. * libgnat/s-imglli.ads: Adapt instance to new ghost parameters. * libgnat/s-imgllli.ads: Adapt instance to new ghost parameters. * libgnat/s-imglllu.ads: Adapt instance to new ghost parameters. * libgnat/s-imgllu.ads: Adapt instance to new ghost parameters. * libgnat/s-imguns.ads: Adapt instance to new ghost parameters. * libgnat/s-valint.ads: Adapt instance to new ghost parameters. * libgnat/s-vallli.ads: Adapt instance to new ghost parameters. * libgnat/s-valllli.ads: Adapt instance to new ghost parameters. * libgnat/s-vallllu.ads: Adapt instance to new ghost parameters. * libgnat/s-valllu.ads: Adapt instance to new ghost parameters. * libgnat/s-valuns.ads: Adapt instance to new ghost parameters. * libgnat/s-vaispe.ads: Take instance of Value_U_Spec as parameter and remove unused declaration. * libgnat/s-vaispe.adb: Idem. * libgnat/s-vauspe.ads: Remove unused declaration. * libgnat/s-valspe.ads: Factor out the specification part of Val_Util. * libgnat/s-valspe.adb: Idem. * libgnat/s-valuti.ads: Move specification to Val_Spec. * libgnat/s-valuti.adb: Idem. * libgnat/s-valboo.ads: Use Val_Spec. * libgnat/s-valboo.adb: Idem. * libgnat/s-imgboo.adb: Idem. * libgnat/s-imagef.adb: Adapt instances to new ghost parameters. * Makefile.rtl: List new files.
2023-06-27ada: Correct the contract of Ada.Text_IO.Get_LineClaire Dross1-9/+13
Item might not be entirely initialized after a call to Get_Line. gcc/ada/ * libgnat/a-textio.ads (Get_Line): Use Relaxed_Initialization on the Item parameter of Get_Line.
2023-06-20ada: Add CHERI intrinsic bindings and helper functions.Daniel King2-0/+545
The package Interfaces.CHERI provides intrinsic bindings and helper functions to allow software to query, create, and manipulate CHERI capabilities. gcc/ada/ * libgnat/i-cheri.ads: Add CHERI intrinsics and helper functions. * libgnat/i-cheri.adb: Likewise
2023-06-20ada: Update annotations in runtime for proofYannick Moy3-1/+15
With bump of stable SPARK used for proof of the runtime, some annotations need to change. gcc/ada/ * libgnat/s-aridou.adb (Scaled_Divide): Add assertions. * libgnat/s-valuti.adb: Add Loop_Variant. * libgnat/s-valuti.ads: Add Exceptional_Cases on No_Return procedure.
2023-06-20ada: Remove references to Might_Not_Return and Always_ReturnClaire Dross35-459/+393
The Might_Not_Return and Always_Return annotations for GNATprove should now be replaced by the two more precise aspects Exceptional_Cases and Always_Terminates. They allow to specify whether a subprogram is allowed to raise exceptions or fail to complete. gcc/ada/ * libgnat/a-strfix.ads: Replace Might_Not_Return annotations by Exceptional_Cases and Always_Terminates aspects. * libgnat/a-tideio.ads: Idem. * libgnat/a-tienio.ads: Idem. * libgnat/a-tifiio.ads: Idem. * libgnat/a-tiflio.ads: Idem. * libgnat/a-tiinio.ads: Idem. * libgnat/a-timoio.ads: Idem. * libgnat/a-textio.ads: Idem. Also mark functions Name, Col, Line, and Page as out of SPARK as they might raise Layout_Error. * libgnarl/a-reatim.ads: Replace Always_Return annotations by Always_Terminates aspects. * libgnat/a-chahan.ads: Idem. * libgnat/a-nbnbig.ads: Idem. * libgnat/a-nbnbin.ads: Idem. * libgnat/a-nbnbre.ads: Idem. * libgnat/a-ngelfu.ads: Idem. * libgnat/a-nlelfu.ads: Idem. * libgnat/a-nllefu.ads: Idem. * libgnat/a-nselfu.ads: Idem. * libgnat/a-nuelfu.ads: Idem. * libgnat/a-strbou.ads: Idem. * libgnat/a-strmap.ads: Idem. * libgnat/a-strsea.ads: Idem. * libgnat/a-strsup.ads: Idem. * libgnat/a-strunb.ads: Idem. * libgnat/a-strunb__shared.ads: Idem. * libgnat/g-souinf.ads: Idem. * libgnat/i-c.ads: Idem. * libgnat/interfac.ads: Idem. * libgnat/interfac__2020.ads: Idem. * libgnat/s-aridou.adb: Idem. * libgnat/s-arit32.adb: Idem. * libgnat/s-atacco.ads: Idem. * libgnat/s-spcuop.ads: Idem. * libgnat/s-stoele.ads: Idem. * libgnat/s-vaispe.ads: Idem. * libgnat/s-vauspe.ads: Idem. * libgnat/i-cstrin.ads: Add a precondition instead of a Might_Not_Return annotation.
2023-06-20ada: Fix edge case in Ada.Calendar.Formatting.Time_OfRonan Desplanques1-28/+3
Before this patch, Ada.Calendar.Formatting.Time_Of executed extra code when passed a number of seconds equal to the number of seconds in a day. This caused the result to be off, perhaps because a statement resetting the number of seconds to zero was missing. Instead of adding such a statement, this patch removes the special handling of the problematic case, which gives the intended result. gcc/ada/ * libgnat/a-calfor.adb (Time_Of): Fix handling of special case.
2023-06-15ada: Adjust QNX Ada priorities to match QNX system prioritiesJohannes Kliemann1-8/+6
The Ada priority range of the QNX runtime started from 0, differing from the QNX system priorities range starting from 1. As this may cause confusion, especially if used in a mixed language environment, the Ada priority range now starts at 1. The default priority of Ada tasks as mandated is the middle of the priority range. On QNX this means the default priority of Ada tasks is 30. This is much higher than the default QNX priority of 10 and may cause unexpected system interruptions when Ada tasks take a lot of CPU time. gcc/ada/ * libgnarl/s-osinte__qnx.adb: Adjust priority conversion function. * libgnat/system-qnx-arm.ads: Adjust priority range and default priority.
2023-06-13ada: Add No_Elaboration_Code_All pragma to System.Storage_ElementsDaniel King1-0/+3
Allows System.Storage_Elements to be used in units that have the No_Elaboration_Code_All restriction. gcc/ada/ * libgnat/s-stoele.ads: Add No_Elaboration_Code_All pragma.
2023-06-13ada: Use ghost predicate in standard libraryYannick Moy1-1/+1
In preparation for attribute Initialized to become ghost, use aspect Ghost_Predicate instead of Predicate in unit Ada.Strings.Superbounded of the standard library. gcc/ada/ * libgnat/a-strsup.ads: Change predicate aspect. * sem_ch13.adb (Add_Predicate): Fix for first predicate.
2023-05-30ada: Ensure Default_Stack_Size is greater than Minimum_Stack_SizeJohannes Kliemann3-2/+13
The Default_Stack_Size function does not check that the binder specified default stack size is greater than the minimum stack size for the runtime. This can result in tasks using default stack sizes less than the minimum stack size because the Adjust_Storage_Size only adjusts storages sizes for tasks that explicitly specify a storage size. To avoid this, the binder specified default stack size is round up to the minimum stack size if required. gcc/ada/ * libgnat/s-parame.adb: Check that Default_Stack_Size >= Minimum_Stack_size. * libgnat/s-parame__rtems.adb: Ditto. * libgnat/s-parame__vxworks.adb: Check that Default_Stack_Size >= Minimum_Stack_size and use the proper Minimum_Stack_Size if Stack_Check_Limits is enabled.
generated by cgit v1.1 at 2025-08-04 13:59:29 +0000