repo.or.cz
/
official-gcc.git
/
search
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
log
|
graphiclog1
|
graphiclog2
|
commit
|
commitdiff
|
tree
|
refs
|
edit
|
fork
first
·
prev
·
next
ada: Make internal_error_function more robust
2021-10-05
Yannick Moy
[Ada] Imp
r
ove e
r
ror me
s
sage o
n
miss
i
ng all/for
in quant
i
fied
.
.
.
commit
|
commitdiff
|
tree
2021-10-05
Yannick Moy
[Ada] Proof of Ada
.
S
t
rings
.
M
a
p
s
commit
|
commitdiff
|
tree
2021-10-05
Y
a
nnick Moy
[Ad
a
]
P
roof of Ada
.
Cha
r
acters
.
Handling
commit
|
commitdiff
|
tree
2021-10-04
Yannick Moy
[Ada]
Ma
r
k Ada
.
Text
_
IO in
S
PARK
commit
|
commitdiff
|
tree
2021-10-04
Yannick Mo
y
[Ada]
A
dd Ada RM descri
p
tion of Ada
.
Strings
.
Bounded
.
.
.
commit
|
commitdiff
|
tree
2021-09-23
Y
a
nnick Moy
[Ada]
M
inimiz
e
parts of Ada
.
S
t
rin
g
s
.
F
i
xe
d
marke
d
SPARK_M
o
de
.
.
.
commit
|
commitdiff
|
tree
2021-09-22
Yanni
c
k
Moy
[A
d
a]
S
implify
co
n
tract of Ada
.
Strin
g
s
.
Fixed
.
Tri
m
f
or
.
.
.
commit
|
commitdiff
|
tree
2021-09-22
Yannick Mo
y
[Ada]
S
pur
i
ous
e
r
ror on def
e
rred
c
onstant w
i
th pre
d
icat
e
commit
|
commitdiff
|
tree
2021-09-22
Yannick Moy
[
A
da] Clar
i
fy parts of Ada
.
Strings
.
U
nbounded
i
n SPARK
.
.
.
commit
|
commitdiff
|
tree
2021-09-22
Yannick
M
oy
[Ada] Add adequate
guard before
c
all
i
ng First_Rep_Item
commit
|
commitdiff
|
tree
2021-09-22
Yannick
M
oy
[Ada] Fix i
n
finite loop in compilat
i
on of ille
g
al code
commit
|
commitdiff
|
tree
2021-09-22
Yannick Moy
[A
d
a] More
p
recise analy
s
is
o
f functi
o
n renamings in
.
.
.
commit
|
commitdiff
|
tree
2021-09-22
Yannick Moy
[Ad
a
] Fix a
c
cess to
p
r
e
dicated parent in Itype
commit
|
commitdiff
|
tree
2021-09-22
Yann
i
ck Moy
[Ada] Fix obsolet
e
commen
t
s/name re
f
e
r
ring to gi
r
der
.
.
.
commit
|
commitdiff
|
tree
2021-09-21
Y
a
nnick Moy
[Ada]
R
ename "o
p
tiona
l
" nod
e
subt
y
p
e
s that
a
llow
E
mpty
commit
|
commitdiff
|
tree
2021-09-21
Ya
n
nick Moy
[Ada] Exce
p
tio
n
r
a
ised on empt
y
f
i
le in
GNATprove mode
commit
|
commitdiff
|
tree
2021-07-08
Ya
n
ni
c
k Mo
y
[Ada] Sk
i
p types in e
r
ror for test
t
o
c
o
mpu
t
e array
.
.
.
commit
|
commitdiff
|
tree
2021-07-08
Ya
n
nick Moy
[Ada]
F
ix on c
o
mputation
o
f
p
acked array size
i
n cas
e
.
.
.
commit
|
commitdiff
|
tree
2021-07-08
Yannick M
o
y
[
Ada] Com
p
u
te siz
e
s when pos
s
ible for pack
e
d
array
.
.
.
commit
|
commitdiff
|
tree
2021-07-07
Yannick Moy
[Ada]
S
implify handling of sure e
r
r
ors
in GNATprove
.
.
.
commit
|
commitdiff
|
tree
2021-07-07
Ya
n
nic
k
M
oy
[A
d
a
]
Fix precondit
i
o
n
of Cot
f
or code
analyzers
commit
|
commitdiff
|
tree
2021-07-06
Yannick Mo
y
[Ada] Missing spa
c
e in error message for patte
r
n matching
commit
|
commitdiff
|
tree
2021-07-05
Yannick Moy
[Ada
]
A
d
ap
t
SP
A
RK R
M
rule o
n
n
on
-
effect
i
vely v
o
latile
.
.
.
commit
|
commitdiff
|
tree
2021-07-05
Yannick Moy
[A
d
a] Adapt SP
A
R
K ch
e
cking
after change in rules regarding
.
.
.
commit
|
commitdiff
|
tree
2021-06-16
Yannick Moy
[Ada] Do not generate a
n
Itype_Reference n
o
de for slices
.
.
.
commit
|
commitdiff
|
tree
2021-06-15
Yannick Moy
[Ada] Exten
d
f
unction to re
t
rieve f
i
r
s
t
/
last node
s
.
.
.
commit
|
commitdiff
|
tree
2021-06-15
Yannic
k
Moy
[Ada] Cl
a
ri
f
y the
s
emantics of signed
i
n
trinsi
c
s
hift
.
.
.
commit
|
commitdiff
|
tree
2021-05-07
Ya
n
nick Moy
[Ada] Ge
n
erate warning for negati
v
e lite
r
al of a mo
d
u
lar
.
.
.
commit
|
commitdiff
|
tree
2021-05-04
Yannick M
o
y
[A
d
a] Mi
n
o
r
t
weak in
p
r
e
tty-printing of ex
p
ressions
commit
|
commitdiff
|
tree
2021-05-04
Yan
n
ick Moy
[Ada] Move match function for pragm
a
Warn
i
n
gs to pub
l
ic
.
.
.
commit
|
commitdiff
|
tree
2021-05-04
Yann
i
ck Moy
[
A
da] Use error mar
k
er
for messages in GNATprove mode
commit
|
commitdiff
|
tree
2021-05-04
Yannick Moy
[
Ada
]
Fix con
t
i
n
uation message for missing AL
L
in
a
ccess
.
.
.
commit
|
commitdiff
|
tree
2021-04-29
Yannick Moy
[Ada] Add
colors
t
o GNATprove messages output to a
.
.
.
commit
|
commitdiff
|
tree
2021-04-29
Yannick
Moy
[A
d
a]
F
ix eva
l
uation of expres
s
ions in inlined code
commit
|
commitdiff
|
tree
2021-04-29
Yannick
M
o
y
[Ada] Fixes in the use
of
s
pans fo
r
error locations
commit
|
commitdiff
|
tree
2021-04-28
Yannick Moy
[Ada] U
s
e
s
pans instead of locat
i
o
ns f
o
r
compile
r
diagnosti
c
s
commit
|
commitdiff
|
tree
2021-04-28
Y
annick
M
o
y
[Ada] Impro
v
e
error mess
a
ge for ghost in pred
i
cate
commit
|
commitdiff
|
tree
2020-12-17
Yann
i
ck Moy
[
A
da] Fixe
s
for G
N
AT error/warning messages
commit
|
commitdiff
|
tree
2020-12-16
Yan
n
ick Moy
[Ada]
Mark ge
n
eric body outside
o
f SPARK
commit
|
commitdiff
|
tree
2020-12-15
Yannick Moy
[Ada]
M
a
r
k
generic
body outside of SPARK
commit
|
commitdiff
|
tree
2020-12-14
Yannick Moy
[A
d
a]
F
ix warn
i
ng control charac
t
er for message on
.
.
.
commit
|
commitdiff
|
tree
2020-12-14
Yannick Moy
[Ada] Refine err
o
r
messages on illeg
a
l
Re
f
ined_State
.
.
.
commit
|
commitdiff
|
tree
2020-12-14
Y
annick Moy
[
Ada] Correctly mark subprogram
a
s not always inli
n
ed
.
.
.
commit
|
commitdiff
|
tree
2020-11-30
Ya
n
nic
k
Moy
[Ada
]
Add comment
o
n special Heap
v
ariable used
in
.
.
.
commit
|
commitdiff
|
tree
2020-11-30
Yanni
c
k
Moy
[Ada] Add continuation me
s
sage w
h
en others ch
o
ice not
.
.
.
commit
|
commitdiff
|
tree
2020-11-27
Yannick Moy
[
Ada] Do not apply rang
e
checks i
n
s
i
d
e generics in
.
.
.
commit
|
commitdiff
|
tree
2020-11-26
Yann
i
ck Moy
[Ada]
N
ew warn
i
ng on questionable missing pa
r
entheses
commit
|
commitdiff
|
tree
2020-11-26
Y
a
nnick Moy
[Ada] Issue ad
v
i
c
e for
e
rror
r
e
gard
i
ng Old/Loop_
E
ntry
.
.
.
commit
|
commitdiff
|
tree
2020-11-25
Y
a
nnick Mo
y
[
Ada] Mini
m
ize side-effect
r
emoval in
GNATpr
o
ve mod
e
commit
|
commitdiff
|
tree
2020-11-25
Y
a
nni
c
k Moy
[
Ad
a
]
Fix inter
n
al comp
i
lation
error on circular type
.
.
.
commit
|
commitdiff
|
tree
2020-11-24
Yannick Moy
[Ada]
Fix cras
h
in GNATprove on inlin
e
d subprogram
.
.
.
commit
|
commitdiff
|
tree
2020-11-24
Y
annic
k
Moy
[Ada] Hand
l
e correctly cur
r
ent i
n
s
t
ance of PO in local
.
.
.
commit
|
commitdiff
|
tree
2020-11-24
Yannick Moy
[Ada] Fix spurious error o
n
child li
b
rary-level subprog
r
am
.
.
.
commit
|
commitdiff
|
tree
2020-11-24
Yannick Mo
y
[Ada] Rejec
t
Global/Depends contracts on null procedures
commit
|
commitdiff
|
tree
2020-10-26
Y
a
nnick Moy
[
A
da]
Fix GNATpro
v
e cras
h
on generics
w
ith a
c
cess types
commit
|
commitdiff
|
tree
2020-10-26
Yannick Moy
[Ada] Do no
t
inst
a
n
t
i
a
te generic b
o
dies outside o
f
.
.
.
commit
|
commitdiff
|
tree
2020-10-21
Y
annick Mo
y
[
Ada] Fix target con
f
iguration f
i
le use
d
for Code
P
eer
.
.
.
commit
|
commitdiff
|
tree
2020-10-20
Yannick Moy
[Ad
a
] Fi
x
es
for pretty comman
d
-line GNATpr
o
v
e outpu
t
.
.
.
commit
|
commitdiff
|
tree
2020-10-20
Yanni
c
k
M
oy
[Ada] Fix comments as volatility properties can a
p
ply
.
.
.
commit
|
commitdiff
|
tree
2020-10-20
Yannick Moy
[Ada] Display source
c
od
e
poi
n
tin
g
at locations in
.
.
.
commit
|
commitdiff
|
tree
2020-10-19
Y
a
nnick Moy
[A
d
a] A
l
te
r
native dis
p
l
a
y
of mult
i
-line mes
s
a
ges for
.
.
.
commit
|
commitdiff
|
tree
2020-10-19
Ya
n
nic
k
M
o
y
[Ada] Reject use of Relax
e
d
_Initialization o
n
scalar
.
.
.
commit
|
commitdiff
|
tree
2020-10-19
Yannick
Moy
[Ada] Clarify protection offere
d
by precondit
i
ons on
.
.
.
commit
|
commitdiff
|
tree
2020-10-19
Y
a
nnick Moy
[
A
da] Clarify current design of Errout wr
t
global varia
b
le
.
.
.
commit
|
commitdiff
|
tree
2020-10-16
Yannick Mo
y
[Ada] S
P
ARK: update for effecti
v
ely vol
a
t
i
le t
y
pes
.
.
.
commit
|
commitdiff
|
tree
2020-07-15
Yannick Moy
[Ada] Mark standard cont
a
iners as
n
ot in S
P
ARK
commit
|
commitdiff
|
tree
2020-07-10
Y
a
nn
i
ck M
o
y
[Ada] Fix detecti
o
n of vo
l
atile
p
rop
e
rties in SPARK
commit
|
commitdiff
|
tree
2020-07-10
Yannick Moy
[Ada] F
i
x asserti
o
n fa
i
lure on (
i
n-)out function param
e
ter
commit
|
commitdiff
|
tree
2020-07-10
Yanni
c
k Moy
[Ada] Re
m
ov
e
use of debug f
l
a
g
-gnatdF
for GN
A
Tprove
commit
|
commitdiff
|
tree
2020-07-08
Y
annick Moy
[Ada
]
A
dd utility function
to r
e
cognize attribute
.
.
.
commit
|
commitdiff
|
tree
2020-06-05
Yanni
c
k Moy
[Ada] Add co
m
ment ab
o
u
t functi
o
n o
n
ly
used i
n
CodePeer
2020-06-05
Yannick Moy
<moy@adacore.com>
commit
|
commitdiff
|
tree
2020-06-03
Yannick Mo
y
[Ada] Improve
handling of SP
A
RK
_
Mo
d
e
in generic instanc
e
s
2020-06-03
Yannick Moy
<moy@adacore.com>
commit
|
commitdiff
|
tree
2020-06-03
Y
annick Moy
[Ada] Fix missing overflow ch
e
cks
i
n analysis of pr
e
defined
.
.
.
2020-06-03
Yannick Moy
<moy@adacore.com>
commit
|
commitdiff
|
tree
2020-06-02
Yannick
M
o
y
[Ad
a
] A
l
low GNA
T
prove to set ov
e
r
f
low
m
ode
2020-06-02
Yannick Moy
<moy@adacore.com>
commit
|
commitdiff
|
tree
2020-05-25
Yann
i
c
k
M
o
y
[Ada] Fix
spurious
e
rror
on che
c
king o
f
null
Abstract_State
2020-05-25
Yannick Moy
<moy@adacore.com>
commit
|
commitdiff
|
tree
2020-05-25
Yannic
k
M
o
y
[Ada] Chan
g
e pragma Compile_Tim
e
_Error
t
o
forc
e
compile
.
.
.
2020-05-25
Yannick Moy
<moy@adacore.com>
commit
|
commitdiff
|
tree
2019-12-16
Yannick Moy
[
A
da
]
Do not issue
r
estriction violations on ign
o
red
.
.
.
2019-12-16
Yannick Moy
<moy@adacore.com>
commit
|
commitdiff
|
tree
2019-12-13
Yannick M
o
y
[Ada] Avoid spurious mism
a
tch
e
rror of
a
s
s
erti
o
n policy
.
.
.
2019-12-13
Yannick Moy
<moy@adacore.com>
commit
|
commitdiff
|
tree
2019-12-13
Yannick Moy
[Ada] A
v
oid
s
purious errors
o
n
Global/Depends in instant
i
a
tions
2019-12-13
Yannick Moy
<moy@adacore.com>
commit
|
commitdiff
|
tree
2019-12-13
Yann
i
ck Mo
y
[Ada] Prevent inlin
i
ng inside condition
o
f whi
l
e loo
p
.
.
.
2019-12-13
Yannick Moy
<moy@adacore.com>
commit
|
commitdiff
|
tree
2019-10-10
Yan
n
ick Moy
[Ada] Fix
i
nlining of subprogra
m
s wi
t
h
dee
p
param/resu
l
t
.
.
.
2019-10-10
Yannick Moy
<moy@adacore.com>
commit
|
commitdiff
|
tree
2019-10-10
Ya
n
nick M
o
y
[Ada]
Do not inline
s
u
bprog
r
a
ms
w
ith
d
e
ep
p
ar
a
m
e
ter
.
.
.
2019-10-10
Yannick Moy
<moy@adacore.com>
commit
|
commitdiff
|
tree
2019-09-19
Yannick Moy
[Ada] Use decla
r
ed type for de
c
iding
on
SPARK p
o
inter
.
.
.
2019-09-19
Yannick Moy
<moy@adacore.com>
commit
|
commitdiff
|
tree
2019-09-19
Yannick
M
oy
[A
d
a]
D
isable
i
n
lining of traversa
l
func
t
i
on in GNATprove
2019-09-19
Yannick Moy
<moy@adacore.com>
commit
|
commitdiff
|
tree
2019-09-19
Yann
i
ck
M
o
y
[
Ada] Allow c
o
ns
t
an
t
s
o
f
a
cc
e
ss type in Glo
b
al cont
r
act
s
2019-09-19
Yannick Moy
<moy@adacore.com>
commit
|
commitdiff
|
tree
2019-09-19
Y
annick Moy
[Ada] M
o
v
e
SPARK borrow-checker to gna
t
2why co
d
ebase
2019-09-19
Yannick Moy
<moy@adacore.com>
commit
|
commitdiff
|
tree
2019-09-18
Y
an
n
i
ck Moy
[Ada] Skip entity name
q
u
al
i
f
ication in GNATprov
e
mod
e
2019-09-18
Yannick Moy
<moy@adacore.com>
commit
|
commitdiff
|
tree
2019-09-17
Yann
i
ck M
o
y
[Ada] Fix rounding of fixed-po
i
nt arit
h
metic operation
2019-09-17
Yannick Moy
<moy@adacore.com>
commit
|
commitdiff
|
tree
2019-09-17
Y
a
nnick Moy
[Ada] Minor fixes mostly in comments of r
u
ntim
e
arithmetic
.
.
.
2019-09-17
Yannick Moy
<moy@adacore.com>
commit
|
commitdiff
|
tree
2019-09-17
Yannick Moy
[Ad
a
] R
a
ise Constraint_Error in
ov
e
rflow case involvin
g
.
.
.
2019-09-17
Yannick Moy
<moy@adacore.com>
commit
|
commitdiff
|
tree
2019-09-17
Yannic
k
M
o
y
[Ada
]
F
ix possible suppressed
overflow
s
in ari
t
hmetic
.
.
.
2019-09-17
Yannick Moy
<moy@adacore.com>
commit
|
commitdiff
|
tree
2019-09-17
Yannick Moy
[Ada] GNATprove: avoid crash on illegal borrow durin
g
.
.
.
2019-09-17
Yannick Moy
<moy@adacore.com>
commit
|
commitdiff
|
tree
2019-09-17
Yannick Moy
[Ad
a
]
Do not i
n
line disp
a
tching ope
r
ations
i
n GNATpr
o
ve
.
.
.
2019-09-17
Yannick Moy
<moy@adacore.com>
commit
|
commitdiff
|
tree
2019-08-21
Yannick Moy
[Ada] More precise pro
p
agation
o
f
Size att
r
ibute in
.
.
.
2019-08-21
Yannick Moy
<moy@adacore.com>
commit
|
commitdiff
|
tree
2019-08-21
Yannick Moy
[A
d
a] Update references to
th
e
SPARK R
M
2019-08-21
Yannick Moy
<moy@adacore.com>
commit
|
commitdiff
|
tree
2019-08-21
Y
annick Moy
[Ada] Avoid spurious error
i
n
GNAT
p
rove mo
d
e on non
.
.
.
2019-08-21
Yannick Moy
<moy@adacore.com>
commit
|
commitdiff
|
tree
2019-08-21
Yannick Moy
[
Ada] Ig
n
ore su
b
p
rogram address in
o
wnersh
i
p
ch
e
cking
2019-08-21
Yannick Moy
<moy@adacore.com>
commit
|
commitdiff
|
tree
2019-08-20
Y
a
nnick M
o
y
[Ad
a
] Adapt
G
NATp
r
ove exp
a
nsion for slices with access
.
.
.
2019-08-20
Yannick Moy
<moy@adacore.com>
commit
|
commitdiff
|
tree
2019-08-19
Yannick
M
oy
[
Ada] Do not skip non-aliasing checking when inlining
.
.
.
2019-08-19
Yannick Moy
<moy@adacore.com>
commit
|
commitdiff
|
tree
2019-08-14
Yan
n
ick Moy
[Ada] Expose part of own
e
rship c
h
e
cking for use in
.
.
.
2019-08-14
Yannick Moy
<moy@adacore.com>
commit
|
commitdiff
|
tree
next