aboutsummaryrefslogtreecommitdiff
path: root/gcc/ada/sem_spark.adb
AgeCommit message (Expand)AuthorFilesLines
2019-09-19[Ada] Move SPARK borrow-checker to gnat2why codebaseYannick Moy1-6179/+0
2019-09-17[Ada] GNATprove: avoid crash on illegal borrow during package elaborationYannick Moy1-4/+8
2019-09-17[Ada] Support chained calls to traversal functions in SPARKClaire Dross1-7/+56
2019-08-21[Ada] Minor refactorings/reformattingsPiotr Trojanek1-1/+1
2019-08-21[Ada] Update references to the SPARK RMYannick Moy1-6/+6
2019-08-21[Ada] Ignore subprogram address in ownership checkingYannick Moy1-0/+1
2019-08-20[Ada] Minor reformattingsGary Dismukes1-15/+12
2019-08-19[Ada] Allow reading a borrowed object inside a call to a pledge functionClaire Dross1-0/+36
2019-08-14[Ada] Expose part of ownership checking for use in GNATproveYannick Moy1-33/+179
2019-08-14[Ada] Check SPARK restriction on Old/Loop_Entry with pointersYannick Moy1-5/+120
2019-08-14[Ada] Fix spurious ownership error in GNATproveYannick Moy1-1/+8
2019-07-23[Ada] Issue error on SPARK ownership rule violationYannick Moy1-13/+50
2019-07-22[Ada] Adapt ownership checking in SPARK to traversal functionsYannick Moy1-18/+205
2019-07-11[Ada] Refactor ownership pointer checking in SPARK as a genericClaire Dross1-141/+272
2019-07-10[Ada] Fix spurious messages on global variables for SPARK pointer supportYannick Moy1-2/+50
2019-07-10[Ada] Fix possible crashes in GNATprove analysis of pointersClaire Dross1-20/+111
2019-07-10[Ada] Minor reformattingHristian Kirtchev1-5/+4
2019-07-10[Ada] Fix crashes on ownership checking in SPARKYannick Moy1-3/+23
2019-07-09[Ada] Minor reformattingHristian Kirtchev1-3/+4
2019-07-09[Ada] Handle implicit moves in SPARK ownership pointer supportYannick Moy1-48/+160
2019-07-09[Ada] Issue error on illegal ownership in SPARKYannick Moy1-1/+10
2019-07-09[Ada] Fix ownership checking for pointers in SPARKYannick Moy1-23/+51
2019-07-04[Ada] Fix crash in SPARK ownership checkingYannick Moy1-3/+6
2019-07-04[Ada] Skip code not in SPARK for ownership analysisYannick Moy1-28/+44
2019-07-04[Ada] Better error messages for ownership errors in SPARKYannick Moy1-62/+185
2019-07-03[Ada] Refine pointer support in SPARKYannick Moy1-51/+60
2019-07-03[Ada] Minor editorial corrections and reformattingGary Dismukes1-1/+1
2019-07-03[Ada] SPARK pointer support extended to local borrowers and observersYannick Moy1-175/+696
2019-07-01[Ada] Minor reformattingHristian Kirtchev1-1/+0
2019-07-01[Ada] SPARK support for pointers through ownershipYannick Moy1-2894/+2755
2019-01-08[Ada] Bump copyright years to 2019Pierre-Marie de Rodat1-1/+1
2018-12-11[Ada] Minor reformattingsGary Dismukes1-3/+3
2018-11-14[Ada] Minor reformattingHristian Kirtchev1-1/+0
2018-10-09[Ada] SPARK: fix bug related to non access object permissionsMaroua Maalej1-18/+2
2018-09-26[Ada] SPARK: fix a bug related to loop exit environmentMaroua Maalej1-23/+51
2018-09-26[Ada] SPARK: update borrowing effects for IN parametersMaroua Maalej1-19/+32
2018-08-21[Ada] Update for Ownership rules for access types according to AI12-0240Maroua Maalej1-2758/+1144
2018-05-23[Ada] Minor reformattingsHristian Kirtchev1-25/+29
2018-05-23[Ada] Fix of some permission rules of pointers in SPARKMaroua Maalej1-35/+60
2018-05-22[Ada] Ada2020: Reduction expressionsEd Schonberg1-6/+0
2018-01-11[Ada] Bump copyright notices to 2018Arnaud Charlet1-1/+1
2017-12-15[multiple changes]Pierre-Marie de Rodat1-0/+6
2017-11-08exp_ch3.adb (Expand_N_Object_Declaration): Save and restore relevant SPARK-re...Hristian Kirtchev1-0/+1
2017-10-09[multiple changes]Pierre-Marie de Rodat1-2/+2
2017-10-09[multiple changes]Pierre-Marie de Rodat1-0/+1
2017-09-12[multiple changes]Arnaud Charlet1-0/+6188
generated by cgit v1.1 at 2025-08-06 13:12:03 +0000