2019-07-04 |
Yannick Moy | [Ada] SPARK_Mode Off now allowed inside subprogram 2019-07-04 Yannick Moy <moy@adacore.com>
|
commit | commitdiff | tree |
2019-07-04 |
Yannick Moy | [Ada] Synchronized object definition in SPARK updated 2019-07-04 Yannick Moy <moy@adacore.com>
|
commit | commitdiff | tree |
2019-07-04 |
Yannick Moy | [Ada] Fix crash in SPARK ownership checking 2019-07-04 Yannick Moy <moy@adacore.com>
|
commit | commitdiff | tree |
2019-07-04 |
Yannick Moy | [Ada] Skip code not in SPARK for ownership analysis 2019-07-04 Yannick Moy <moy@adacore.com>
|
commit | commitdiff | tree |
2019-07-04 |
Yannick Moy | [Ada] Better error messages for ownership errors in... 2019-07-04 Yannick Moy <moy@adacore.com>
|
commit | commitdiff | tree |
2019-07-03 |
Yannick Moy | [Ada] Suppress warnings in generic instantiations with... 2019-07-03 Yannick Moy <moy@adacore.com>
|
commit | commitdiff | tree |
2019-07-03 |
Yannick Moy | [Ada] Refine pointer support in SPARK 2019-07-03 Yannick Moy <moy@adacore.com>
|
commit | commitdiff | tree |
2019-07-03 |
Yannick Moy | [Ada] SPARK pointer support extended to local borrowers... 2019-07-03 Yannick Moy <moy@adacore.com>
|
commit | commitdiff | tree |
2019-07-01 |
Yannick Moy | [Ada] SPARK support for pointers through ownership 2019-07-01 Yannick Moy <moy@adacore.com>
|
commit | commitdiff | tree |
2019-07-01 |
Yannick Moy | [Ada] Improve error message on mult/div between fixed... 2019-07-01 Yannick Moy <moy@adacore.com>
|
commit | commitdiff | tree |
2018-12-11 |
Yannick Moy | [Ada] Do not expand code inside ignored ghost bodies 2018-12-11 Yannick Moy <moy@adacore.com>
|
commit | commitdiff | tree |
2018-12-11 |
Yannick Moy | [Ada] Improve error message when named number passed... 2018-12-11 Yannick Moy <moy@adacore.com>
|
commit | commitdiff | tree |
2018-12-11 |
Yannick Moy | [Ada] Support access types in GNATprove 2018-12-11 Yannick Moy <moy@adacore.com>
|
commit | commitdiff | tree |
2018-12-11 |
Yannick Moy | [Ada] Better error message from GNATprove on illegal... 2018-12-11 Yannick Moy <moy@adacore.com>
|
commit | commitdiff | tree |
2018-10-09 |
Yannick Moy | [Ada] Ignore pragmas Compile_Time_Error/Warning in... 2018-10-09 Yannick Moy <moy@adacore.com>
|
commit | commitdiff | tree |
2018-09-26 |
Yannick Moy | [Ada] Issue info message on inlined subprograms in... 2018-09-26 Yannick Moy <moy@adacore.com>
|
commit | commitdiff | tree |
2018-09-26 |
Yannick Moy | [Ada] Do not issue by default info messages for inlining... 2018-09-26 Yannick Moy <moy@adacore.com>
|
commit | commitdiff | tree |
2018-08-21 |
Yannick Moy | [Ada] Document entries of the target parametrization... 2018-08-21 Yannick Moy <moy@adacore.com>
|
commit | commitdiff | tree |
2018-08-21 |
Yannick Moy | [Ada] Define versions of dimension system for Float... 2018-08-21 Yannick Moy <moy@adacore.com>
|
commit | commitdiff | tree |
2018-07-17 |
Yannick Moy | [Ada] Avoid confusing warning on exception propagation... 2018-07-17 Yannick Moy <moy@adacore.com>
|
commit | commitdiff | tree |
2018-07-16 |
Yannick Moy | [Ada] Inline: rewrap comment 2018-07-16 Yannick Moy <moy@adacore.com>
|
commit | commitdiff | tree |
2018-07-16 |
Yannick Moy | [Ada] Adjust inlining in GNATprove mode for predicate... 2018-07-16 Yannick Moy <moy@adacore.com>
|
commit | commitdiff | tree |
2018-06-11 |
Yannick Moy | [Ada] Mark parameters as coming from source for GNATprove 2018-06-11 Yannick Moy <moy@adacore.com>
|
commit | commitdiff | tree |
2018-06-11 |
Yannick Moy | [Ada] Reject violation of SPARK 6.1.4(12) with enclosing... 2018-06-11 Yannick Moy <moy@adacore.com>
|
commit | commitdiff | tree |
2018-06-11 |
Yannick Moy | [Ada] Add Suppressible argument to Assertion_Policy... 2018-06-11 Yannick Moy <moy@adacore.com>
|
commit | commitdiff | tree |
2018-06-11 |
Yannick Moy | [Ada] Do not query the representation information in... 2018-06-11 Yannick Moy <moy@adacore.com>
|
commit | commitdiff | tree |
2018-06-11 |
Yannick Moy | [Ada] Mark extended return of unconstrained type as... 2018-06-11 Yannick Moy <moy@adacore.com>
|
commit | commitdiff | tree |
2018-06-11 |
Yannick Moy | [Ada] Do not force Part_Of on generic units 2018-06-11 Yannick Moy <moy@adacore.com>
|
commit | commitdiff | tree |
2018-05-31 |
Yannick Moy | [Ada] Fix check on placement of multiple loop (in)variant... 2018-05-31 Yannick Moy <moy@adacore.com>
|
commit | commitdiff | tree |
2018-05-30 |
Yannick Moy | [Ada] Correctly ignore Assertion_Policy in modes CodePeer... 2018-05-30 Yannick Moy <moy@adacore.com>
|
commit | commitdiff | tree |
2018-05-28 |
Yannick Moy | [Ada] Update FE check following change in SPARK RM... 2018-05-28 Yannick Moy <moy@adacore.com>
|
commit | commitdiff | tree |
2018-05-28 |
Yannick Moy | [Ada] Further evaluation of type bounds in GNATprove... 2018-05-28 Yannick Moy <moy@adacore.com>
|
commit | commitdiff | tree |
2018-05-25 |
Yannick Moy | [Ada] Fix handling of Loop_Entry for CodePeer/SPARK 2018-05-25 Yannick Moy <moy@adacore.com>
|
commit | commitdiff | tree |
2018-05-25 |
Yannick Moy | [Ada] Detect misplaced assertions between loop invariants 2018-05-25 Yannick Moy <moy@adacore.com>
|
commit | commitdiff | tree |
2018-05-24 |
Yannick Moy | [Ada] Improve GNATprove messages on unproved checks 2018-05-24 Yannick Moy <moy@adacore.com>
|
commit | commitdiff | tree |
2018-05-23 |
Yannick Moy | [Ada] Clarify meaning of local pragma Warnings Off... 2018-05-23 Yannick Moy <moy@adacore.com>
|
commit | commitdiff | tree |
2018-05-23 |
Yannick Moy | [Ada] Fix implementation of utility for finding enclosing... 2018-05-23 Yannick Moy <moy@adacore.com>
|
commit | commitdiff | tree |
2018-05-21 |
Yannick Moy | [Ada] Use type conversion when inlining may trigger... 2018-05-21 Yannick Moy <moy@adacore.com>
|
commit | commitdiff | tree |
2018-05-21 |
Yannick Moy | [Ada] Spurious error in inlining for GNATprove on prefix... 2018-05-21 Yannick Moy <moy@adacore.com>
|
commit | commitdiff | tree |
2018-05-21 |
Yannick Moy | [Ada] Crash on incorrect frontend inlining in GNATprove... 2018-05-21 Yannick Moy <moy@adacore.com>
|
commit | commitdiff | tree |
2018-01-11 |
Yannick Moy | [Ada] Update description of restriction SPARK_05 with... 2018-01-11 Yannick Moy <moy@adacore.com>
|
commit | commitdiff | tree |
2017-11-09 |
Yannick Moy | exp_disp.adb (Make_DT): Default initialize Ifaces_List... 2017-11-09 Yannick Moy <moy@adacore.com>
|
commit | commitdiff | tree |
2017-09-11 |
Yannick Moy | lib-xref-spark_specific.adb: Minor rewrite. 2017-09-11 Yannick Moy <moy@adacore.com>
|
commit | commitdiff | tree |
2017-09-11 |
Yannick Moy | sem_util.adb (Check_Result_And_Post_State): Do not... 2017-09-11 Yannick Moy <moy@adacore.com>
|
commit | commitdiff | tree |
2017-09-11 |
Yannick Moy | gnat1drv.adb (Adjust_Global_Switches): Set Check_Validity_Of... 2017-09-11 Yannick Moy <moy@adacore.com>
|
commit | commitdiff | tree |
2017-09-08 |
Yannick Moy | sem_aux.adb, [...] (Get_Called_Entity): New function... 2017-09-08 Yannick Moy <moy@adacore.com>
|
commit | commitdiff | tree |
2017-09-06 |
Yannick Moy | sem_prag.adb (Analyze_Depends_In_Decl_Part): Add continuatio... 2017-09-06 Yannick Moy <moy@adacore.com> 2017-09-06 Yannick Moy <moy@adacore.com>
|
commit | commitdiff | tree |
2017-04-27 |
Yannick Moy | exp_util.ads, [...] (Evaluate_Name): Force evaluation... 2017-04-27 Yannick Moy <moy@adacore.com>
|
commit | commitdiff | tree |
2017-04-25 |
Yannick Moy | sem_util.adb: Minor refactoring. 2017-04-25 Yannick Moy <moy@adacore.com>
|
commit | commitdiff | tree |
2017-04-25 |
Yannick Moy | checks.adb (Apply_Scalar_Range_Check): Analyze precisely... 2017-04-25 Yannick Moy <moy@adacore.com>
|
commit | commitdiff | tree |
2017-04-25 |
Yannick Moy | checks.adb (Determine_Range_R): Special case type conversion... 2017-04-25 Yannick Moy <moy@adacore.com>
|
commit | commitdiff | tree |
2017-01-13 |
Yannick Moy | inline.adb, inline.ads (Call_Can_Be_Inlined_In_GNATprove_Mod... 2017-01-13 Yannick Moy <moy@adacore.com>
|
commit | commitdiff | tree |
2016-10-12 |
Yannick Moy | sem_prag.adb (Analyze_Refined_Depends_In_Decl_Part... 2016-10-12 Yannick Moy <moy@adacore.com>
|
commit | commitdiff | tree |
2016-07-07 |
Yannick Moy | sem_ch6.adb (Process_Formals): Set ghost flag on formal... 2016-07-07 Yannick Moy <moy@adacore.com>
|
commit | commitdiff | tree |
2016-07-06 |
Yannick Moy | sem_ch6.adb (Analyze_Expression_Function): Mark body... 2016-07-06 Yannick Moy <moy@adacore.com>
|
commit | commitdiff | tree |
2016-05-02 |
Yannick Moy | a-tigeli.adb (Get_Line): Always set Last prior to returning. 2016-05-02 Yannick Moy <moy@adacore.com> 2016-05-02 Yannick Moy <moy@adacore.com>
|
commit | commitdiff | tree |
2016-04-20 |
Yannick Moy | sem_ch4.adb: Fix typos in comments. 2016-04-20 Yannick Moy <moy@adacore.com>
|
commit | commitdiff | tree |
2015-10-20 |
Yannick Moy | fmap.adb, [...]: Fix coding style for marking start... 2015-10-20 Yannick Moy <moy@adacore.com> 2015-10-20 Yannick Moy <moy@adacore.com>
|
commit | commitdiff | tree |
2015-05-26 |
Yannick Moy | sem_aux.adb, [...] (Get_Low_Bound): Use Type_Low_Bound. 2015-05-26 Yannick Moy <moy@adacore.com>
|
commit | commitdiff | tree |
2015-05-26 |
Yannick Moy | inline.adb (Has_Initialized_Type): Adapt to new names. 2015-05-26 Yannick Moy <moy@adacore.com>
|
commit | commitdiff | tree |
2015-02-05 |
Yannick Moy | sem_prag.adb, [...]: Minor code clean up. 2015-02-05 Yannick Moy <moy@adacore.com>
|
commit | commitdiff | tree |
2015-02-05 |
Yannick Moy | par-prag.adb (Pragma_Warnings): Update for extended... 2015-02-05 Yannick Moy <moy@adacore.com>
|
commit | commitdiff | tree |
2015-02-05 |
Yannick Moy | opt.ads (Warn_On_Suspicious_Contract): Update comment... 2015-02-05 Yannick Moy <moy@adacore.com>
|
commit | commitdiff | tree |
2014-08-04 |
Yannick Moy | sem.adb, sem.ads (In_Default_Expr): Global flag that... 2014-08-04 Yannick Moy <moy@adacore.com>
|
commit | commitdiff | tree |
2014-07-31 |
Yannick Moy | sem_parg.adb, [...] (Collect_Subprogram_Inputs_Outputs... 2014-07-31 Yannick Moy <moy@adacore.com>
|
commit | commitdiff | tree |
2014-07-30 |
Yannick Moy | inline.adb (Build_Body_To_Inline): Issue more precise... 2014-07-30 Yannick Moy <moy@adacore.com>
|
commit | commitdiff | tree |
2014-07-30 |
Yannick Moy | einfo.ads (Is_Inlined): Document new use in GNATprove... 2014-07-30 Yannick Moy <moy@adacore.com>
|
commit | commitdiff | tree |
2014-07-30 |
Yannick Moy | gnat1drv.adb (Adjust_Global_Switches): Set Ineffective_Inlin... 2014-07-30 Yannick Moy <moy@adacore.com>
|
commit | commitdiff | tree |
2014-07-29 |
Yannick Moy | 2014-07-29 Yannick Moy <moy@adacore.com> 2014-07-29 Yannick Moy <moy@adacore.com>
|
commit | commitdiff | tree |
2014-05-21 |
Yannick Moy | 2014-05-21 Yannick Moy <moy@adacore.com> 2014-05-21 Yannick Moy <moy@adacore.com>
|
commit | commitdiff | tree |
2014-02-25 |
Yannick Moy | sem_ch3.adb, [...]: Mark most references to SPARK RM... 2014-02-25 Yannick Moy <moy@adacore.com>
|
commit | commitdiff | tree |
2014-01-22 |
Yannick Moy | errout.adb (Initialize): Remove trick to add dummy... 2014-01-22 Yannick Moy <moy@adacore.com>
|
commit | commitdiff | tree |
2014-01-20 |
Yannick Moy | exp_spark.adb (Expand_SPARK_Call): Remove procedure. 2014-01-20 Yannick Moy <moy@adacore.com> 2014-01-20 Yannick Moy <moy@adacore.com>
|
commit | commitdiff | tree |
2014-01-20 |
Yannick Moy | 2014-01-20 Yannick Moy <moy@adacore.com> 2014-01-20 Yannick Moy <moy@adacore.com>
|
commit | commitdiff | tree |
2013-04-24 |
Yannick Moy | snames.ads-tmpl: Minor change to list Loop_(In)variant... 2013-04-24 Yannick Moy <moy@adacore.com>
|
commit | commitdiff | tree |
2013-04-24 |
Yannick Moy | adabkend.adb, [...]: Everything with name 'Alfa' renamed... 2013-04-24 Yannick Moy <moy@adacore.com>
|
commit | commitdiff | tree |
2013-04-22 |
Yannick Moy | exp_prag.adb (Expand_Pragma_Loop_Variant): Rewrite... 2013-04-22 Yannick Moy <moy@adacore.com>
|
commit | commitdiff | tree |
2013-04-22 |
Yannick Moy | par-prag.adb, [...]: Remove all references to Pragma_Contrac... 2013-04-22 Yannick Moy <moy@adacore.com>
|
commit | commitdiff | tree |
2013-04-22 |
Yannick Moy | aspects.ads, [...]: Removal of references to Contract_Case. 2013-04-22 Yannick Moy <moy@adacore.com>
|
commit | commitdiff | tree |
2012-10-01 |
Yannick Moy | sem_ch13.adb (Add_Invariants): Analyze the invariant... 2012-10-01 Yannick Moy <moy@adacore.com>
|
commit | commitdiff | tree |
2012-03-30 |
Yannick Moy | lib-xref-alfa.adb, [...]: Minor addition of comments... 2012-03-30 Yannick Moy <moy@adacore.com>
|
commit | commitdiff | tree |
2012-03-30 |
Yannick Moy | lib-xref-alfa.adb (Generate_Dereference): Use Get_Code_Unit... 2012-03-30 Yannick Moy <moy@adacore.com>
|
commit | commitdiff | tree |
2012-03-30 |
Yannick Moy | lib-xref-alfa.adb (Add_Alfa_File): Take into account... 2012-03-30 Yannick Moy <moy@adacore.com>
|
commit | commitdiff | tree |
2012-03-20 |
Yannick Moy | gnat_rm.texi, [...]: Update documentation. 2012-03-20 Yannick Moy <moy@adacore.com>
|
commit | commitdiff | tree |
2012-03-15 |
Yannick Moy | aspects.adb, [...] (Aspect_Id): New GNAT aspect Aspect_Contr... 2012-03-15 Yannick Moy <moy@adacore.com>
|
commit | commitdiff | tree |
2011-12-02 |
Yannick Moy | sem_util.adb (Unique_Name): Reach through Unique_Entity... 2011-12-02 Yannick Moy <moy@adacore.com> 2011-12-02 Yannick Moy <moy@adacore.com>
|
commit | commitdiff | tree |
2011-09-02 |
Yannick Moy | usage.adb, [...]: Disable by default warnings on suspicious... 2011-09-02 Yannick Moy <moy@adacore.com>
|
commit | commitdiff | tree |
2011-08-30 |
Yannick Moy | * gcc-interface/Make-lang.in: Update dependencies.
|
commit | commitdiff | tree |
2011-08-04 |
Yannick Moy | gnat_rm.texi: Document new pragma and aspect. 2011-08-04 Yannick Moy <moy@adacore.com>
|
commit | commitdiff | tree |
2011-08-04 |
Yannick Moy | sem_ch3.adb (Constrain_Enumeration, [...]): remove... 2011-08-04 Yannick Moy <moy@adacore.com>
|
commit | commitdiff | tree |
2011-08-04 |
Yannick Moy | sem_ch3.adb (Analyze_Object_Declaration): remove obsolete... 2011-08-04 Yannick Moy <moy@adacore.com>
|
commit | commitdiff | tree |
2011-08-03 |
Yannick Moy | sem_ch11.adb (Analyze_Raise_xxx_Error): do not mark... 2011-08-03 Yannick Moy <moy@adacore.com>
|
commit | commitdiff | tree |
2011-08-02 |
Yannick Moy | sem_ch3.adb, [...]: Protect call to Current_Subprogram... 2011-08-02 Yannick Moy <moy@adacore.com>
|
commit | commitdiff | tree |
2011-08-02 |
Yannick Moy | sem_res.adb: Protect calls to Matching_Static_Array_Bounds... 2011-08-02 Yannick Moy <moy@adacore.com>
|
commit | commitdiff | tree |
2011-08-02 |
Yannick Moy | einfo.adb, einfo.ads (Body_Is_In_ALFA, [...]): get... 2011-08-02 Yannick Moy <moy@adacore.com>
|
commit | commitdiff | tree |
2011-08-02 |
Yannick Moy | sem_aggr.adb, [...]: cleanup of SPARK mode 2011-08-02 Yannick Moy <moy@adacore.com>
|
commit | commitdiff | tree |
2011-08-02 |
Yannick Moy | cstand.adb (Create_Standard): sets Is_In_ALFA component... 2011-08-02 Yannick Moy <moy@adacore.com>
|
commit | commitdiff | tree |
2011-08-02 |
Yannick Moy | errout.adb (First_Node): minor renaming 2011-08-02 Yannick Moy <moy@adacore.com>
|
commit | commitdiff | tree |
2011-08-02 |
Yannick Moy | par-ch6.adb: Correct obsolete name in comments 2011-08-02 Yannick Moy <moy@adacore.com>
|
commit | commitdiff | tree |
2011-08-02 |
Yannick Moy | sem_aggr.adb (Resolve_Aggregate): disable incorrectly... 2011-08-02 Yannick Moy <moy@adacore.com>
|
commit | commitdiff | tree |
next |