aboutsummaryrefslogtreecommitdiff
path: root/gcc/ada/exp_spark.adb
AgeCommit message (Expand)AuthorFilesLines
2024-01-22Update copyright years.Marc Poulhiès1-1/+1
2023-12-19ada: Fix SPARK expansion of container aggregatesYannick Moy1-0/+146
2023-11-21ada: Fix type for SPARK expansion on deep delta aggregatesYannick Moy1-1/+1
2023-11-21ada: Deep delta aggregatesSteve Baird1-6/+47
2023-05-16ada: Build invariant procedure while freezing in GNATprove modePiotr Trojanek1-8/+46
2023-01-09ada: Update copyright noticeArnaud Charlet1-1/+1
2022-11-08ada: Cleanup local variable that is only set as an out parameterPiotr Trojanek1-1/+1
2022-05-17[Ada] Allow inlining for proof inside genericsYannick Moy1-2/+5
2022-01-11[Ada] Update copyright notice and bump Gnatvsn.Current_YearArnaud Charlet1-1/+1
2022-01-05[Ada] Expand controlling functions wrappers in GNATprove modePiotr Trojanek1-0/+32
2021-12-02[Ada] Enable expansion of dispatching equality for GNATprovePiotr Trojanek1-15/+274
2021-10-20[Ada] Prevent use of an uninitialized AST field with universal integerPiotr Trojanek1-0/+1
2021-05-07[Ada] Minor reformattingsBob Duff1-23/+23
2021-05-07[Ada] Variable-sized node typesBob Duff1-2/+6
2021-05-03[Ada] Update copyright noticeArnaud Charlet1-1/+1
2020-11-30[Ada] Implement inheritance for Default_Initial_Condition and address other gapsGary Dismukes1-2/+5
2020-11-24[Ada] Replace chained if-then-elsif with case stmt for attribute idsPiotr Trojanek1-83/+87
2020-11-24[Ada] Remove SPARK-specific expansion of array aggregatesPiotr Trojanek1-126/+0
2020-10-27[Ada] Fix GNATprove support for iterated_component_associationsPiotr Trojanek1-60/+112
2020-10-26[Ada] Fix SPARK expansion of iterated_component_assoc in delta aggregatePiotr Trojanek1-0/+1
2020-10-26[Ada] Cleanup SPARK expansion of aggregates with iterated_component_assocPiotr Trojanek1-7/+3
2020-10-23[Ada] Fix crash in SPARK on array delta_aggregate with subtype_indicationPiotr Trojanek1-8/+13
2020-10-23[Ada] Decorate iterated_component_association in SPARK expansionPiotr Trojanek1-1/+94
2020-07-27[Ada] Add range check for GNATprove on 'Pos to Long_Integer conversionPiotr Trojanek1-3/+9
2020-07-15[Ada] Fix for possibly null ranges in 'Update and delta_aggregatePiotr Trojanek1-2/+2
2020-07-10[Ada] Reformatting and typo correctionsGary Dismukes1-8/+8
2020-07-10[Ada] Reuse SPARK expansion of attribute Update for delta_aggregatePiotr Trojanek1-160/+198
2020-07-10[Ada] Fix expansion of 'Update with multiple choices in GNATprovePiotr Trojanek1-9/+57
2020-07-07[Ada] Set range checks for for 'Update on arrays in GNATprove expansionPiotr Trojanek1-10/+76
2020-07-06[Ada] Set range checks flag on 'Update for GNATprove in expansionPiotr Trojanek1-0/+47
2020-06-16[Ada] Reuse Is_Object where possiblePiotr Trojanek1-1/+1
2020-06-11[Ada] Consolidate handling of implicit dereferences into semantic analysisEric Botcazou1-50/+0
2020-06-10[Ada] Revert workaround for expansion of Enum_Rep in GNATprove modePiotr Trojanek1-9/+2
2020-06-10[Ada] Fold Enum_Rep attribute in evaluation and not in expansionPiotr Trojanek1-23/+0
2020-06-08[Ada] Port a modified expansion of Enum_Rep from GNAT to GNATprovePiotr Trojanek1-10/+3
2020-06-08[Ada] Reuse standard expansion of 'First and 'Last in GNATprove modePiotr Trojanek1-0/+7
2020-06-08[Ada] Reuse Get_Index_Subtype in the special expander for GNATprovePiotr Trojanek1-26/+4
2020-06-02[Ada] Bump copyright yearArnaud Charlet1-1/+1
2019-09-18[Ada] Factor out code for deciding statically known Constrained attributesClaire Dross1-0/+15
2019-08-20[Ada] Adapt GNATprove expansion for slices with access prefixYannick Moy1-20/+22
2019-08-12[Ada] More precise handling of Size/Object_Size in GNATproveYannick Moy1-4/+7
2019-08-12[Ada] SPARK: disable expansion of Enum_RepYannick Moy1-1/+25
2019-07-22[Ada] Remove obsolete Is_For_Access_Subtype machineryEric Botcazou1-6/+0
2019-07-09[Ada] Expand Enum_Rep attribute reference in GNATprove modeYannick Moy1-0/+7
2019-01-08[Ada] Bump copyright years to 2019Pierre-Marie de Rodat1-1/+1
2018-05-24[Ada] Quadratic compile time with tagged typesJustin Squirek1-1/+1
2018-01-11[Ada] Bump copyright notices to 2018Arnaud Charlet1-1/+1
2017-11-08[multiple changes]Pierre-Marie de Rodat1-1/+1
2017-10-09[multiple changes]Pierre-Marie de Rodat1-37/+38
2017-10-09[multiple changes]Pierre-Marie de Rodat1-33/+58
generated by cgit v1.1 at 2024-09-27 21:02:11 +0000