Public Git Hosting - official-gcc.git/search

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
2022-05-13	Yannick Moy	[Ada] Facilitate proof of Overwrite in bounded strings...	commit \| commitdiff \| tree
2022-05-12	Yannick Moy	[Ada] Remove useless pragma Warnings Off from runtime...	commit \| commitdiff \| tree
2022-05-12	Yannick Moy	[Ada] Do not issue a warning on a postcondition of...	commit \| commitdiff \| tree
2022-05-12	Yannick Moy	[Ada] Add ghost code to facilitate proof with SPARK	commit \| commitdiff \| tree
2022-05-12	Yannick Moy	[Ada] Remove use of use-clauses in loaded runtime units	commit \| commitdiff \| tree
2022-05-12	Yannick Moy	[Ada] Adapt CodePeer analysis of GNAT to changes in...	commit \| commitdiff \| tree
2022-05-12	Yannick Moy	[Ada] Proof of 'Image support for signed integers	commit \| commitdiff \| tree
2022-05-11	Yannick Moy	[Ada] Proof of 'Image support for unsigned integers	commit \| commitdiff \| tree
2022-05-11	Yannick Moy	[Ada] Adapt proof of System.Arith_Double after update...	commit \| commitdiff \| tree
2022-05-10	Yannick Moy	[Ada] Fix indentation to follow uniform style across...	commit \| commitdiff \| tree
2022-05-09	Yannick Moy	[Ada] Suggest use of First_Valid/Last_Valid on type...	commit \| commitdiff \| tree
2022-05-09	Yannick Moy	[Ada] Set Error_Msg_Warn before use of << insertion	commit \| commitdiff \| tree
2022-01-11	Yannick Moy	[Ada] Adapt proof of System.Arith_Double	commit \| commitdiff \| tree
2022-01-11	Yannick Moy	[Ada] Recover proof of Ada.Strings.Fixed with assertions	commit \| commitdiff \| tree
2022-01-11	Yannick Moy	[Ada] Proof of unit System.Case_Util	commit \| commitdiff \| tree
2022-01-11	Yannick Moy	[Ada] Adapt ghost code to maintain proof	commit \| commitdiff \| tree
2022-01-11	Yannick Moy	[Ada] Proof of System.Vectors.Boolean_Operations	commit \| commitdiff \| tree
2022-01-06	Yannick Moy	[Ada] Proof of System.Generic_Array_Operations at silver...	commit \| commitdiff \| tree
2022-01-06	Yannick Moy	[Ada] Justify false positive message from CodePeer...	commit \| commitdiff \| tree
2022-01-06	Yannick Moy	[Ada] Proof of runtime unit for non-binary modular...	commit \| commitdiff \| tree
2022-01-06	Yannick Moy	[Ada] Proof of runtime units for binary modular exponentiation	commit \| commitdiff \| tree
2022-01-05	Yannick Moy	[Ada] Add contracts for the proof of System.Arith_128	commit \| commitdiff \| tree
2022-01-05	Yannick Moy	[Ada] Proof of runtime units for integer exponentiation...	commit \| commitdiff \| tree
2022-01-05	Yannick Moy	[Ada] Proof of runtime units for integer exponentiation...	commit \| commitdiff \| tree
2022-01-05	Yannick Moy	[Ada] Rename parameter-dependent constants in generic...	commit \| commitdiff \| tree
2022-01-05	Yannick Moy	[Ada] Fix lemma in generic unit System.Arith_Double	commit \| commitdiff \| tree
2021-12-02	Yannick Moy	[Ada] Proof of System.Arith_32 for double arithmetic...	commit \| commitdiff \| tree
2021-12-02	Yannick Moy	[Ada] Amend proof of System.Arith_Double to remove...	commit \| commitdiff \| tree
2021-12-02	Yannick Moy	[Ada] Add pragma Annotate for CodePeer analysis	commit \| commitdiff \| tree
2021-12-02	Yannick Moy	[Ada] Proof of support units for 'Width on signed integers	commit \| commitdiff \| tree
2021-12-02	Yannick Moy	[Ada] Proof of Interfaces.C with SPARK	commit \| commitdiff \| tree
2021-12-02	Yannick Moy	[Ada] Proof of System.Val_Util utilities for 'Value...	commit \| commitdiff \| tree
2021-12-02	Yannick Moy	[Ada] Proof of Boolean'Image and Boolean'Value	commit \| commitdiff \| tree
2021-12-01	Yannick Moy	[Ada] Improve error messages for dot notation when...	commit \| commitdiff \| tree
2021-12-01	Yannick Moy	[Ada] Add query for extended precision floating-point...	commit \| commitdiff \| tree
2021-12-01	Yannick Moy	[Ada] Improve messages on incorrect state refinement...	commit \| commitdiff \| tree
2021-11-10	Yannick Moy	[Ada] Create explicit ghost mirror unit for big integers	commit \| commitdiff \| tree
2021-11-10	Yannick Moy	[Ada] Better error message on missing parentheses	commit \| commitdiff \| tree
2021-11-09	Yannick Moy	[Ada] Complete support for prefixed call on subtypes...	commit \| commitdiff \| tree
2021-11-09	Yannick Moy	[Ada] Fix support for prefixed call with incomplete...	commit \| commitdiff \| tree
2021-10-25	Yannick Moy	[Ada] Issue error on invalid use of Ghost inside pragma...	commit \| commitdiff \| tree
2021-10-20	Yannick Moy	[Ada] Proof of the runtime support for attribute 'Width	commit \| commitdiff \| tree
2021-10-20	Yannick Moy	[Ada] Provide dummy body for big integers library used...	commit \| commitdiff \| tree
2021-10-20	Yannick Moy	[Ada] Issue warning on unused quantified expression	commit \| commitdiff \| tree
2021-10-05	Yannick Moy	[Ada] Improve error message on array aggregates	commit \| commitdiff \| tree
2021-10-05	Yannick Moy	[Ada] Improve error message on missing all/for in quantified...	commit \| commitdiff \| tree
2021-10-05	Yannick Moy	[Ada] Proof of Ada.Strings.Maps	commit \| commitdiff \| tree
2021-10-05	Yannick Moy	[Ada] Proof of Ada.Characters.Handling	commit \| commitdiff \| tree
2021-10-04	Yannick Moy	[Ada] Mark Ada.Text_IO in SPARK	commit \| commitdiff \| tree
2021-10-04	Yannick Moy	[Ada] Add Ada RM description of Ada.Strings.Bounded...	commit \| commitdiff \| tree
2021-09-23	Yannick Moy	[Ada] Minimize parts of Ada.Strings.Fixed marked SPARK_Mode...	commit \| commitdiff \| tree
next

Mirror of the offical gcc git repository hosted at gcc.gnu.org

RSS Atom