projects
/
gcc.git
/ search
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
[Ada] Complete the more extended AST traversal used in GNATprove
2019-08-13
Yannick Moy
[Ada] Complete the more extended AST traversal used...
2019-08-13
Yannick Moy
<moy@adacore.com>
commit
|
commitdiff
|
tree
2019-08-12
Yannick Moy
[Ada] New aspect/pragma No_Caching for analysis of...
2019-08-12
Yannick Moy
<moy@adacore.com>
commit
|
commitdiff
|
tree
2019-08-12
Yannick Moy
[Ada] Adapt new extended traversal of AST to have optional...
2019-08-12
Yannick Moy
<moy@adacore.com>
commit
|
commitdiff
|
tree
2019-08-12
Yannick Moy
[Ada] More precise handling of Size/Object_Size in...
2019-08-12
Yannick Moy
<moy@adacore.com>
commit
|
commitdiff
|
tree
2019-08-12
Yannick Moy
[Ada] SPARK: disable expansion of Enum_Rep
2019-08-12
Yannick Moy
<moy@adacore.com>
commit
|
commitdiff
|
tree
2019-08-12
Yannick Moy
[Ada] Extended traversal subprograms for GNATprove
2019-08-12
Yannick Moy
<moy@adacore.com>
commit
|
commitdiff
|
tree
2019-07-23
Yannick Moy
[Ada] Issue error on SPARK ownership rule violation
2019-07-23
Yannick Moy
<moy@adacore.com>
commit
|
commitdiff
|
tree
2019-07-23
Yannick Moy
[Ada] Fix binding of ghost units with finalizer
2019-07-23
Yannick Moy
<moy@adacore.com>
commit
|
commitdiff
|
tree
2019-07-22
Yannick Moy
[Ada] Adapt ownership checking in SPARK to traversal...
2019-07-22
Yannick Moy
<moy@adacore.com>
commit
|
commitdiff
|
tree
2019-07-22
Yannick Moy
[Ada] Issue warning or error message on ignored typing...
2019-07-22
Yannick Moy
<moy@adacore.com>
commit
|
commitdiff
|
tree
2019-07-11
Yannick Moy
[Ada] Avoid spurious errors on dimensionality checking...
2019-07-11
Yannick Moy
<moy@adacore.com>
commit
|
commitdiff
|
tree
2019-07-11
Yannick Moy
[Ada] Flip the meaning of debug switch -gnatdF
2019-07-11
Yannick Moy
<moy@adacore.com>
commit
|
commitdiff
|
tree
2019-07-11
Yannick Moy
[Ada] Avoid spurious warning on assertions with Loop_Entry
2019-07-11
Yannick Moy
<moy@adacore.com>
commit
|
commitdiff
|
tree
2019-07-11
Yannick Moy
[Ada] Avoid spurious warning on wrong order of operator...
2019-07-11
Yannick Moy
<moy@adacore.com>
commit
|
commitdiff
|
tree
2019-07-10
Yannick Moy
[Ada] Fix spurious messages on global variables for...
2019-07-10
Yannick Moy
<moy@adacore.com>
commit
|
commitdiff
|
tree
2019-07-10
Yannick Moy
[Ada] Allow multiple units per file in GNATprove
2019-07-10
Yannick Moy
<moy@adacore.com>
commit
|
commitdiff
|
tree
2019-07-10
Yannick Moy
[Ada] Fix crashes on ownership checking in SPARK
2019-07-10
Yannick Moy
<moy@adacore.com>
commit
|
commitdiff
|
tree
2019-07-10
Yannick Moy
[Ada] Use renamings in GNATprove mode for side-effects...
2019-07-10
Yannick Moy
<moy@adacore.com>
commit
|
commitdiff
|
tree
2019-07-09
Yannick Moy
[Ada] Sinfo: refine comment for Do_Range_Check
2019-07-09
Yannick Moy
<moy@adacore.com>
commit
|
commitdiff
|
tree
2019-07-09
Yannick Moy
[Ada] Expand Enum_Rep attribute reference in GNATprove...
2019-07-09
Yannick Moy
<moy@adacore.com>
commit
|
commitdiff
|
tree
2019-07-09
Yannick Moy
[Ada] Prevent inconsistent state for inlining in GNATprove
2019-07-09
Yannick Moy
<moy@adacore.com>
commit
|
commitdiff
|
tree
2019-07-09
Yannick Moy
[Ada] Expand type of static expressions in GNATprove...
2019-07-09
Yannick Moy
<moy@adacore.com>
commit
|
commitdiff
|
tree
2019-07-09
Yannick Moy
[Ada] Handle implicit moves in SPARK ownership pointer...
2019-07-09
Yannick Moy
<moy@adacore.com>
commit
|
commitdiff
|
tree
2019-07-09
Yannick Moy
[Ada] Issue error on illegal ownership in SPARK
2019-07-09
Yannick Moy
<moy@adacore.com>
commit
|
commitdiff
|
tree
2019-07-09
Yannick Moy
[Ada] Fix ownership checking for pointers in SPARK
2019-07-09
Yannick Moy
<moy@adacore.com>
commit
|
commitdiff
|
tree
2019-07-08
Yannick Moy
[Ada] Do not erase precise type on fixed-point real...
2019-07-08
Yannick Moy
<moy@adacore.com>
commit
|
commitdiff
|
tree
2019-07-05
Yannick Moy
[Ada] Accept compilation switches -Og/-Ofast in non...
2019-07-05
Yannick Moy
<moy@adacore.com>
commit
|
commitdiff
|
tree
2019-07-05
Yannick Moy
[Ada] Fix inlining in GNATprove inside quantified expressions
2019-07-05
Yannick Moy
<moy@adacore.com>
commit
|
commitdiff
|
tree
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
next