aboutsummaryrefslogtreecommitdiff
path: root/gcc/ada/sem_prag.adb
AgeCommit message (Expand)AuthorFilesLines
2024-05-17ada: Expose utility routine for processing of Depends contracts in SPARKPiotr Trojanek1-29/+0
2024-05-17ada: Only record types with discriminants can be unconstrainedPiotr Trojanek1-7/+4
2024-05-17ada: Simplify code for private types with unknown discriminantsPiotr Trojanek1-2/+1
2024-05-17ada: Allow private items with unknown discriminants as Depends inputsPiotr Trojanek1-2/+4
2024-05-17ada: Tune detection of unconstrained and tagged items in Depends contractPiotr Trojanek1-4/+4
2024-05-16ada: Fix ordering of code for pragma Preelaborable_InitializationPiotr Trojanek1-80/+80
2024-05-16ada: Fix docs and comments about pragmas for Boolean-valued aspectsPiotr Trojanek1-23/+25
2024-05-14ada: Fix pragma Compile_Time_Error and -gnatdJ crashRonan Desplanques1-4/+4
2024-05-14ada: Fix crash with -gnatdJ and -gnatw.wRonan Desplanques1-1/+1
2024-05-14ada: Update of SPARK RM legality rules on ghost codeYannick Moy1-6/+6
2024-05-13ada: Deconstruct flag Split_PPC since splitting now is done in expansionPiotr Trojanek1-6/+2
2024-05-13ada: Move splitting of pre/post aspect expressions to expansionPiotr Trojanek1-18/+0
2024-05-13ada: Recognize pragma Lock_Free as specific to GNATPiotr Trojanek1-0/+1
2024-05-07ada: Improve pragma No_Return's pre-Ada2022 handling of functionsSteve Baird1-69/+97
2024-05-07ada: Bad internal naming when using pragma Compile_Time_ErrorJustin Squirek1-1/+17
2024-05-07ada: Accept constants of access types as globals of side-effect functionPiotr Trojanek1-1/+3
2024-05-07ada: Update comment about implicit inputs of Depends contractPiotr Trojanek1-2/+1
2024-05-06ada: Allow use of writable parameters inside function with side-effectsPiotr Trojanek1-2/+3
2024-05-06ada: Cleanup collecting of implicit outputsPiotr Trojanek1-11/+11
2024-05-06ada: Support writable parameters in Depends with side-effectsPiotr Trojanek1-8/+13
2024-05-06ada: Deconstruct support for abstract states with Relaxed_InitializationPiotr Trojanek1-16/+9
2024-01-22Update copyright years.Marc Poulhiès1-1/+1
2023-12-19ada: Ignore unconstrained components as inputs for DependsPiotr Trojanek1-36/+2
2023-12-19ada: Cleanup SPARK legality checkingYannick Moy1-7/+5
2023-11-30ada: Remove SPARK legality checksYannick Moy1-80/+0
2023-11-30ada: Ignore defered compile time errors without backendViljar Indus1-0/+10
2023-11-30ada: Fix spelling of functions with(out) "side effects"Yannick Moy1-6/+6
2023-11-07ada: Rename Is_Limited_View to reflect actual queryYannick Moy1-1/+1
2023-11-07ada: New Local_Restrictions and User_Aspect aspects.Steve Baird1-0/+182
2023-11-07ada: Simplify code for Ignore_Style_Checks_PragmasViljar Indus1-15/+11
2023-10-19ada: Support new SPARK aspect Side_EffectsYannick Moy1-39/+266
2023-07-06ada: Improve error message on violation of SPARK_Mode rulesYannick Moy1-1/+3
2023-06-20ada: Add the ability to add error codes to error messagesYannick Moy1-2/+3
2023-06-15ada: Accept aspect Always_Terminates on packagesPiotr Trojanek1-2/+18
2023-06-15ada: Accept aspect Always_Terminates on entriesPiotr Trojanek1-0/+5
2023-06-15ada: Reject aspect Always_Terminates on functions and generic functionsPiotr Trojanek1-0/+13
2023-06-15ada: Accept aspect Always_Terminates without expressionPiotr Trojanek1-36/+38
2023-06-13ada: Implement new aspect Always_Terminates for SPARKPiotr Trojanek1-0/+199
2023-06-13ada: Streamline expansion of controlled actions for aggregatesEric Botcazou1-1/+4
2023-06-13ada: Support new GNAT-specific aspect Ghost_PredicateYannick Moy1-4/+16
2023-05-29ada: Attach pre/post on access-to-subprogram to internal subprogram typePiotr Trojanek1-1/+5
2023-05-29ada: Fix internal error with pragma Compile_Time_{Warning,Error}Eric Botcazou1-2/+7
2023-05-29ada: Tune message for pre/post on access-to-subprogram in old AdaPiotr Trojanek1-1/+1
2023-05-29ada: Analyze pre/post on access-to-subprogram without a wrapperPiotr Trojanek1-4/+18
2023-05-26ada: Remove redundant guard against empty listsPiotr Trojanek1-3/+1
2023-05-26ada: Fix handling of Global contracts inside generic subprogramsPiotr Trojanek1-1/+3
2023-05-25ada: Fix comments for recently added SPARK aspectsPiotr Trojanek1-9/+9
2023-05-25ada: Fix copy-paste mistake in analysis of Exceptional_CasesPiotr Trojanek1-3/+3
2023-05-23ada: Accept and analyze new aspect Exceptional_CasesPiotr Trojanek1-0/+429
2023-05-23ada: Add new switch -gnatyzArnaud Charlet1-1/+1