gcc.gnu.org Git - gcc.git/search

]> gcc.gnu.org Git - gcc.git/search

2024-07-02	Yannick Moy	ada: Fix analysis of Extensions_Visible	commit \| commitdiff \| tree
2024-06-20	Yannick Moy	ada: Fix checking of SPARK RM on ghost with concurrent...	commit \| commitdiff \| tree
2024-06-20	Yannick Moy	ada: Fix inlining of fixed-lower-bound array for GNATprove	commit \| commitdiff \| tree
2024-06-14	Yannick Moy	ada: Skip subprogram body entities inside scopes	commit \| commitdiff \| tree
2024-06-13	Yannick Moy	ada: Fix test for giving hint on ambiguous aggregate	commit \| commitdiff \| tree
2024-06-13	Yannick Moy	ada: List subprogram body entities in scopes	commit \| commitdiff \| tree
2024-06-13	Yannick Moy	ada: Do not inline subprogram which could cause SPARK...	commit \| commitdiff \| tree
2024-06-10	Yannick Moy	ada: Remove streaming facilities from generics for...	commit \| commitdiff \| tree
2024-05-14	Yannick Moy	ada: Update of SPARK RM legality rules on ghost code	commit \| commitdiff \| tree
2024-05-14	Yannick Moy	ada: Fix ghost policy in use for generic instantiation	commit \| commitdiff \| tree
2024-05-07	Yannick Moy	ada: Adapt proof of runtime units	commit \| commitdiff \| tree
2024-05-07	Yannick Moy	ada: Fix missing flag for GNATprove	commit \| commitdiff \| tree
2024-05-07	Yannick Moy	ada: Fix spurious error on generic state in SPARK	commit \| commitdiff \| tree
2024-05-07	Yannick Moy	ada: SPARK rule changed on functions with side effects	commit \| commitdiff \| tree
2024-05-06	Yannick Moy	ada: Fix detection of (Un)Hide_Info pragma in GNATprove...	commit \| commitdiff \| tree
2024-05-06	Yannick Moy	ada: Prevent inlining in GNATprove for memory leaks	commit \| commitdiff \| tree
2024-05-06	Yannick Moy	ada: Do not inline in GNATprove the subprograms with...	commit \| commitdiff \| tree
2023-12-19	Yannick Moy	ada: Fix SPARK expansion of container aggregates	commit \| commitdiff \| tree
2023-12-19	Yannick Moy	ada: Do not issue SPARK legality error if SPARK_Mode...	commit \| commitdiff \| tree
2023-12-19	Yannick Moy	ada: Cleanup SPARK legality checking	commit \| commitdiff \| tree
2023-11-30	Yannick Moy	ada: Remove SPARK legality checks	commit \| commitdiff \| tree
2023-11-30	Yannick Moy	ada: Fix spelling of functions with(out) "side effects"	commit \| commitdiff \| tree
2023-11-28	Yannick Moy	ada: Remove dependency on System.Val_Bool in System...	commit \| commitdiff \| tree
2023-11-21	Yannick Moy	ada: Fix type for SPARK expansion on deep delta aggregates	commit \| commitdiff \| tree
2023-11-07	Yannick Moy	ada: Rename Is_Limited_View to reflect actual query	commit \| commitdiff \| tree
2023-10-19	Yannick Moy	ada: Support new SPARK aspect Side_Effects	commit \| commitdiff \| tree
2023-09-26	Yannick Moy	ada: Clarify RM references that justify a constraint...	commit \| commitdiff \| tree
2023-09-14	Yannick Moy	ada: Improve detection of deactivated code for warnings...	commit \| commitdiff \| tree
2023-08-07	Yannick Moy	ada: Crash in GNATprove due to wrong detection of inlining	commit \| commitdiff \| tree
2023-08-01	Yannick Moy	ada: Fix printing of numbers in JSON output for data...	commit \| commitdiff \| tree
2023-08-01	Yannick Moy	ada: Disable inlining of subprograms with Skip(_Flow_And...	commit \| commitdiff \| tree
2023-08-01	Yannick Moy	ada: Fix generation of JSON output for data representation	commit \| commitdiff \| tree
2023-07-18	Yannick Moy	ada: Allow warnings with explain code	commit \| commitdiff \| tree
2023-07-10	Yannick Moy	ada: Simplify assertion to remove CodePeer message	commit \| commitdiff \| tree
2023-07-10	Yannick Moy	ada: Adapt proof of System.Arith_Double to remove CVC4	commit \| commitdiff \| tree
2023-07-06	Yannick Moy	ada: Improve error message on violation of SPARK_Mode...	commit \| commitdiff \| tree
2023-07-04	Yannick Moy	ada: Fix list of inherited subprograms in query for...	commit \| commitdiff \| tree
2023-06-20	Yannick Moy	ada: Fix crash on inlining in GNATprove	commit \| commitdiff \| tree
2023-06-20	Yannick Moy	ada: Do not issue warning on postcondition in some...	commit \| commitdiff \| tree
2023-06-20	Yannick Moy	ada: Add the ability to add error codes to error messages	commit \| commitdiff \| tree
2023-06-20	Yannick Moy	ada: Update annotations in runtime for proof	commit \| commitdiff \| tree
2023-06-15	Yannick Moy	ada: Reject Loop_Entry inside prefix of Loop_Entry	commit \| commitdiff \| tree
2023-06-13	Yannick Moy	ada: Mark attribute Initialized as ghost code	commit \| commitdiff \| tree
2023-06-13	Yannick Moy	ada: Use ghost predicate in standard library	commit \| commitdiff \| tree
2023-06-13	Yannick Moy	ada: Support new GNAT-specific aspect Ghost_Predicate	commit \| commitdiff \| tree
2023-05-29	Yannick Moy	ada: Restore SPARK_Mode On for numerical functions	commit \| commitdiff \| tree
2023-05-26	Yannick Moy	ada: Default initialize entity to avoid CodePeer message	commit \| commitdiff \| tree
2023-05-26	Yannick Moy	ada: Minor doc clarification	commit \| commitdiff \| tree
2023-05-26	Yannick Moy	ada: Complete contracts of SPARK units	commit \| commitdiff \| tree
2023-05-23	Yannick Moy	ada: Add default value at initialization for CodePeer	commit \| commitdiff \| tree
2023-05-23	Yannick Moy	ada: Facilitate proof of Interfaces.C.To_Ada	commit \| commitdiff \| tree
2023-05-16	Yannick Moy	ada: Update proof of runtime units	commit \| commitdiff \| tree
2023-05-16	Yannick Moy	ada: Simplify dramatically ghost code for proof of...	commit \| commitdiff \| tree
2023-05-16	Yannick Moy	ada: Add intermediate assertions for proof of Super_Tail	commit \| commitdiff \| tree
2023-05-16	Yannick Moy	ada: Set Loop_Variant assertion policy to Ignore in...	commit \| commitdiff \| tree
2023-05-16	Yannick Moy	ada: Restore proof of System.Arith_Double	commit \| commitdiff \| tree
2023-05-15	Yannick Moy	ada: Add annotations for proof of termination of runtime...	commit \| commitdiff \| tree
2023-05-15	Yannick Moy	ada: Recover proof of runtime units	commit \| commitdiff \| tree
2023-05-15	Yannick Moy	ada: Recover proof of Interfaces.C for termination	commit \| commitdiff \| tree
2023-05-15	Yannick Moy	ada: Update comment after SPARK RM change	commit \| commitdiff \| tree
2023-05-15	Yannick Moy	ada: Fix handling of pragma Warnings (Toolname, Off/On)	commit \| commitdiff \| tree
2023-05-15	Yannick Moy	ada: Allow pragmas Annotate between loop pragmas	commit \| commitdiff \| tree
2022-12-06	Yannick Moy	ada: Allow No_Caching on volatile types	commit \| commitdiff \| tree
2022-11-28	Yannick Moy	ada: Implement change to SPARK RM rule on state refinement	commit \| commitdiff \| tree
2022-11-14	Yannick Moy	ada: Fix error on SPARK_Mode on library-level separate...	commit \| commitdiff \| tree
2022-11-14	Yannick Moy	ada: Improve location of error messages in instantiations	commit \| commitdiff \| tree
2022-10-06	Yannick Moy	ada: Do not issue compiler warnings in GNATprove mode	commit \| commitdiff \| tree
2022-09-12	Yannick Moy	[Ada] Justify false alarm from CodePeer analysis of...	commit \| commitdiff \| tree
2022-09-12	Yannick Moy	[Ada] Accept explicit SPARK_Mode Auto as configuration...	commit \| commitdiff \| tree
2022-09-12	Yannick Moy	[Ada] Reject use in SPARK of Asm intrinsics for code...	commit \| commitdiff \| tree
2022-09-02	Yannick Moy	[Ada] Recover proof of Scaled_Divide in System.Arith_64	commit \| commitdiff \| tree
2022-07-13	Yannick Moy	[Ada] Fix incorrect handling of Ghost aspect	commit \| commitdiff \| tree
2022-07-13	Yannick Moy	[Ada] Fix proof of runtime unit System.Arith_64	commit \| commitdiff \| tree
2022-07-13	Yannick Moy	[Ada] Fix automatic proof on System.Arith_32	commit \| commitdiff \| tree
2022-07-12	Yannick Moy	[Ada] Ignore switches for controlling frontend warnings...	commit \| commitdiff \| tree
2022-07-06	Yannick Moy	[Ada] Deferred constant considered as not preelaborable	commit \| commitdiff \| tree
2022-07-06	Yannick Moy	[Ada] Support ghost generic formal parameters	commit \| commitdiff \| tree
2022-07-05	Yannick Moy	[Ada] Fix spurious error on object renaming with ghost...	commit \| commitdiff \| tree
2022-07-05	Yannick Moy	[Ada] Spurious error on qualified prefix in Pack.Func...	commit \| commitdiff \| tree
2022-06-02	Yannick Moy	[Ada] Fix spurious errors on ghost code in generics	commit \| commitdiff \| tree
2022-06-02	Yannick Moy	[Ada] Issue errors on wrong context for ghost entities	commit \| commitdiff \| tree
2022-06-02	Yannick Moy	[Ada] Removal of dead code Analyze_Label_Entity	commit \| commitdiff \| tree
2022-06-01	Yannick Moy	[Ada] Allow confirming volatile properties on No_Caching...	commit \| commitdiff \| tree
2022-06-01	Yannick Moy	[Ada] Fix classification of Subprogram_Variant as assertion...	commit \| commitdiff \| tree
2022-06-01	Yannick Moy	[Ada] Issue a warning on entity hidden in use_clause...	commit \| commitdiff \| tree
2022-06-01	Yannick Moy	[Ada] Issue better error message for out-of-order keywords...	commit \| commitdiff \| tree
2022-05-30	Yannick Moy	[Ada] Update proofs of double arithmetic unit after...	commit \| commitdiff \| tree
2022-05-30	Yannick Moy	[Ada] Adapt proof of runtime unit s-arit32	commit \| commitdiff \| tree
2022-05-30	Yannick Moy	[Ada] PR ada/105303 Fix use of Assertion_Policy in...	commit \| commitdiff \| tree
2022-05-19	Yannick Moy	[Ada] Further adapt proof of double arithmetic runtime...	commit \| commitdiff \| tree
2022-05-18	Yannick Moy	[Ada] Adapt proof of double arithmetic runtime unit	commit \| commitdiff \| tree
2022-05-18	Yannick Moy	[Ada] Fix proof of runtime units	commit \| commitdiff \| tree
2022-05-18	Yannick Moy	[Ada] Spurious error on freezing of tagged types in...	commit \| commitdiff \| tree
2022-05-17	Yannick Moy	[Ada] Allow inlining for proof inside generics	commit \| commitdiff \| tree
2022-05-17	Yannick Moy	[Ada] Fix insertion of declaration inside quantified...	commit \| commitdiff \| tree
2022-05-16	Yannick Moy	[Ada] Fix proof of double arithmetic units	commit \| commitdiff \| tree
2022-05-16	Yannick Moy	[Ada] Update comment justifying non-inlining for proof...	commit \| commitdiff \| tree
2022-05-13	Yannick Moy	[Ada] Simplify helper units for formal hashed sets...	commit \| commitdiff \| tree
2022-05-13	Yannick Moy	[Ada] Adapt body of formal sets and maps for SPARK	commit \| commitdiff \| tree
2022-05-13	Yannick Moy	[Ada] Remove dependency on tampering checks and controlled...	commit \| commitdiff \| tree
next

GNU Compiler Collection

RSS Atom

This page took 0.414545 seconds and 5 git commands to generate.