projects
/
gcc.git
/ search
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
[Ada] Ada_2020: ongoing work for aggregates for bounded containers
2020-10-21
Yannick Moy
[Ada] Fix target configuration file used for CodePeer...
commit
|
commitdiff
|
tree
2020-10-20
Yannick Moy
[Ada] Fixes for pretty command-line GNATprove output...
commit
|
commitdiff
|
tree
2020-10-20
Yannick Moy
[Ada] Fix comments as volatility properties can apply...
commit
|
commitdiff
|
tree
2020-10-20
Yannick Moy
[Ada] Display source code pointing at locations in...
commit
|
commitdiff
|
tree
2020-10-19
Yannick Moy
[Ada] Alternative display of multi-line messages for...
commit
|
commitdiff
|
tree
2020-10-19
Yannick Moy
[Ada] Reject use of Relaxed_Initialization on scalar...
commit
|
commitdiff
|
tree
2020-10-19
Yannick Moy
[Ada] Clarify protection offered by preconditions on...
commit
|
commitdiff
|
tree
2020-10-19
Yannick Moy
[Ada] Clarify current design of Errout wrt global variable...
commit
|
commitdiff
|
tree
2020-10-16
Yannick Moy
[Ada] SPARK: update for effectively volatile types...
commit
|
commitdiff
|
tree
2020-07-15
Yannick Moy
[Ada] Mark standard containers as not in SPARK
commit
|
commitdiff
|
tree
2020-07-10
Yannick Moy
[Ada] Fix detection of volatile properties in SPARK
commit
|
commitdiff
|
tree
2020-07-10
Yannick Moy
[Ada] Fix assertion failure on (in-)out function parameter
commit
|
commitdiff
|
tree
2020-07-10
Yannick Moy
[Ada] Remove use of debug flag -gnatdF for GNATprove
commit
|
commitdiff
|
tree
2020-07-08
Yannick Moy
[Ada] Add utility function to recognize attribute ...
commit
|
commitdiff
|
tree
2020-06-05
Yannick Moy
[Ada] Add comment about function only used in CodePeer
2020-06-05
Yannick Moy
<moy@adacore.com>
commit
|
commitdiff
|
tree
2020-06-03
Yannick Moy
[Ada] Improve handling of SPARK_Mode in generic instances
2020-06-03
Yannick Moy
<moy@adacore.com>
commit
|
commitdiff
|
tree
2020-06-03
Yannick Moy
[Ada] Fix missing overflow checks in analysis of predefined...
2020-06-03
Yannick Moy
<moy@adacore.com>
commit
|
commitdiff
|
tree
2020-06-02
Yannick Moy
[Ada] Allow GNATprove to set overflow mode
2020-06-02
Yannick Moy
<moy@adacore.com>
commit
|
commitdiff
|
tree
2020-05-25
Yannick Moy
[Ada] Fix spurious error on checking of null Abstract_State
2020-05-25
Yannick Moy
<moy@adacore.com>
commit
|
commitdiff
|
tree
2020-05-25
Yannick Moy
[Ada] Change pragma Compile_Time_Error to force compile...
2020-05-25
Yannick Moy
<moy@adacore.com>
commit
|
commitdiff
|
tree
2019-12-16
Yannick Moy
[Ada] Do not issue restriction violations on ignored...
2019-12-16
Yannick Moy
<moy@adacore.com>
commit
|
commitdiff
|
tree
2019-12-13
Yannick Moy
[Ada] Avoid spurious mismatch error of assertion policy...
2019-12-13
Yannick Moy
<moy@adacore.com>
commit
|
commitdiff
|
tree
2019-12-13
Yannick Moy
[Ada] Avoid spurious errors on Global/Depends in instantiations
2019-12-13
Yannick Moy
<moy@adacore.com>
commit
|
commitdiff
|
tree
2019-12-13
Yannick Moy
[Ada] Prevent inlining inside condition of while loop...
2019-12-13
Yannick Moy
<moy@adacore.com>
commit
|
commitdiff
|
tree
2019-10-10
Yannick Moy
[Ada] Fix inlining of subprograms with deep param/result...
2019-10-10
Yannick Moy
<moy@adacore.com>
commit
|
commitdiff
|
tree
2019-10-10
Yannick Moy
[Ada] Do not inline subprograms with deep parameter...
2019-10-10
Yannick Moy
<moy@adacore.com>
commit
|
commitdiff
|
tree
2019-09-19
Yannick Moy
[Ada] Use declared type for deciding on SPARK pointer...
2019-09-19
Yannick Moy
<moy@adacore.com>
commit
|
commitdiff
|
tree
2019-09-19
Yannick Moy
[Ada] Disable inlining of traversal function in GNATprove
2019-09-19
Yannick Moy
<moy@adacore.com>
commit
|
commitdiff
|
tree
2019-09-19
Yannick Moy
[Ada] Allow constants of access type in Global contracts
2019-09-19
Yannick Moy
<moy@adacore.com>
commit
|
commitdiff
|
tree
2019-09-19
Yannick Moy
[Ada] Move SPARK borrow-checker to gnat2why codebase
2019-09-19
Yannick Moy
<moy@adacore.com>
commit
|
commitdiff
|
tree
2019-09-18
Yannick Moy
[Ada] Skip entity name qualification in GNATprove mode
2019-09-18
Yannick Moy
<moy@adacore.com>
commit
|
commitdiff
|
tree
2019-09-17
Yannick Moy
[Ada] Fix rounding of fixed-point arithmetic operation
2019-09-17
Yannick Moy
<moy@adacore.com>
commit
|
commitdiff
|
tree
2019-09-17
Yannick Moy
[Ada] Minor fixes mostly in comments of runtime arithmetic...
2019-09-17
Yannick Moy
<moy@adacore.com>
commit
|
commitdiff
|
tree
2019-09-17
Yannick Moy
[Ada] Raise Constraint_Error in overflow case involving...
2019-09-17
Yannick Moy
<moy@adacore.com>
commit
|
commitdiff
|
tree
2019-09-17
Yannick Moy
[Ada] Fix possible suppressed overflows in arithmetic...
2019-09-17
Yannick Moy
<moy@adacore.com>
commit
|
commitdiff
|
tree
2019-09-17
Yannick Moy
[Ada] GNATprove: avoid crash on illegal borrow during...
2019-09-17
Yannick Moy
<moy@adacore.com>
commit
|
commitdiff
|
tree
2019-09-17
Yannick Moy
[Ada] Do not inline dispatching operations in GNATprove...
2019-09-17
Yannick Moy
<moy@adacore.com>
commit
|
commitdiff
|
tree
2019-08-21
Yannick Moy
[Ada] More precise propagation of Size attribute in...
2019-08-21
Yannick Moy
<moy@adacore.com>
commit
|
commitdiff
|
tree
2019-08-21
Yannick Moy
[Ada] Update references to the SPARK RM
2019-08-21
Yannick Moy
<moy@adacore.com>
commit
|
commitdiff
|
tree
2019-08-21
Yannick Moy
[Ada] Avoid spurious error in GNATprove mode on non...
2019-08-21
Yannick Moy
<moy@adacore.com>
commit
|
commitdiff
|
tree
2019-08-21
Yannick Moy
[Ada] Ignore subprogram address in ownership checking
2019-08-21
Yannick Moy
<moy@adacore.com>
commit
|
commitdiff
|
tree
2019-08-20
Yannick Moy
[Ada] Adapt GNATprove expansion for slices with access...
2019-08-20
Yannick Moy
<moy@adacore.com>
commit
|
commitdiff
|
tree
2019-08-19
Yannick Moy
[Ada] Do not skip non-aliasing checking when inlining...
2019-08-19
Yannick Moy
<moy@adacore.com>
commit
|
commitdiff
|
tree
2019-08-14
Yannick Moy
[Ada] Expose part of ownership checking for use in...
2019-08-14
Yannick Moy
<moy@adacore.com>
commit
|
commitdiff
|
tree
2019-08-14
Yannick Moy
[Ada] Check SPARK restriction on Old/Loop_Entry with...
2019-08-14
Yannick Moy
<moy@adacore.com>
commit
|
commitdiff
|
tree
2019-08-14
Yannick Moy
[Ada] Fix spurious ownership error in GNATprove
2019-08-14
Yannick Moy
<moy@adacore.com>
commit
|
commitdiff
|
tree
2019-08-14
Yannick Moy
[Ada] Fix failing assertions on SPARK elaboration
2019-08-14
Yannick Moy
<moy@adacore.com>
commit
|
commitdiff
|
tree
2019-08-13
Yannick Moy
[Ada] Avoid crash in GNATprove_Mode on allocator inside...
2019-08-13
Yannick Moy
<moy@adacore.com>
commit
|
commitdiff
|
tree
2019-08-13
Yannick Moy
[Ada] Avoid crash in GNATprove due to inlining inside...
2019-08-13
Yannick Moy
<moy@adacore.com>
commit
|
commitdiff
|
tree
2019-08-13
Yannick Moy
[Ada] Avoid spurious errors on dimensionality checking...
2019-08-13
Yannick Moy
<moy@adacore.com>
commit
|
commitdiff
|
tree
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
next