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] Fix insertion of declaration inside quantified expression
2022-05-17
Yannick Moy
[Ada] Fix i
n
sert
i
o
n
of declaration in
s
ide quantified
.
.
.
commit
|
commitdiff
|
tree
2022-05-16
Yannick
M
oy
[Ada] Fix proof of double arithmetic units
commit
|
commitdiff
|
tree
2022-05-16
Y
a
nnick Moy
[
A
d
a] Update comm
e
nt just
i
fying non-i
n
lining for
p
roof
.
.
.
commit
|
commitdiff
|
tree
2022-05-13
Yann
i
c
k
M
oy
[Ada]
S
i
m
p
lify helper
u
nits for form
a
l hashed sets
.
.
.
commit
|
commitdiff
|
tree
2022-05-13
Ya
n
nick Moy
[Ada] Ada
p
t body of formal s
e
ts
a
nd
maps for SPARK
commit
|
commitdiff
|
tree
2022-05-13
Yannick Moy
[Ada] Remove depe
n
de
n
cy
o
n tampering c
h
ecks and c
o
ntrolled
.
.
.
commit
|
commitdiff
|
tree
2022-05-13
Ya
n
nick Moy
[
A
da] Facilitate pro
o
f of Overwrite in bounde
d
strings
.
.
.
commit
|
commitdiff
|
tree
2022-05-12
Yannick Moy
[Ad
a
] Remove
u
seless pr
a
gma
W
arnings Off from runtime
.
.
.
commit
|
commitdiff
|
tree
2022-05-12
Yanni
c
k Moy
[
A
da] Do n
o
t
i
ssue a warnin
g
on a
postcon
d
ition of
.
.
.
commit
|
commitdiff
|
tree
2022-05-12
Yannick Moy
[Ada] Add
gho
s
t code to fac
i
litate proo
f
w
i
th SPARK
commit
|
commitdiff
|
tree
2022-05-12
Yann
i
c
k
M
oy
[
Ad
a
] Remove use of use-clauses in
l
o
a
ded runtime
units
commit
|
commitdiff
|
tree
2022-05-12
Yannick Moy
[Ada] Adapt Co
d
ePeer analysis
o
f GNAT to ch
a
nges
in
.
.
.
commit
|
commitdiff
|
tree
2022-05-12
Yannick Moy
[A
d
a
]
Proof
of 'Image support for signed integers
commit
|
commitdiff
|
tree
2022-05-11
Yannick Moy
[Ada] Proof of 'Im
a
ge support
f
or unsi
g
n
ed
i
nt
e
gers
commit
|
commitdiff
|
tree
2022-05-11
Yannick Moy
[Ada] Adapt proof
o
f Syste
m
.
A
r
ith_D
o
uble after update
.
.
.
commit
|
commitdiff
|
tree
2022-05-10
Yanni
c
k
Moy
[Ada] Fix
indentatio
n
t
o follow uniform style
a
cross
.
.
.
commit
|
commitdiff
|
tree
2022-05-09
Yannick
Moy
[Ada] Suggest
use of First_Valid/L
a
st_Valid
on
typ
e
.
.
.
commit
|
commitdiff
|
tree
2022-05-09
Yannick Mo
y
[
Ad
a
]
Set Error_Msg_Warn
b
e
fore use of << insertion
commit
|
commitdiff
|
tree
2022-01-11
Ya
n
nick Moy
[Ada
]
Adapt proof of System
.
Arith
_
Doub
l
e
commit
|
commitdiff
|
tree
2022-01-11
Yanni
c
k
Moy
[Ada] Recover proof of Ad
a
.
St
r
ings
.
F
i
xed wi
t
h assertio
n
s
commit
|
commitdiff
|
tree
2022-01-11
Y
a
nnick Moy
[Ada] Proof of
uni
t
System
.
Case_
U
til
commit
|
commitdiff
|
tree
2022-01-11
Yannick Moy
[
Ada] Adapt ghost
code to
maint
a
in proof
commit
|
commitdiff
|
tree
2022-01-11
Yannick
M
oy
[Ada] Proof
o
f
System
.
Vectors
.
Boolean_Operations
commit
|
commitdiff
|
tree
2022-01-06
Yannick Moy
[Ad
a
]
P
roof of System
.
Generic_Array_Oper
a
tions at silver
.
.
.
commit
|
commitdiff
|
tree
2022-01-06
Yannick Moy
[Ada
]
Justify
f
alse
p
osit
i
ve
message from
C
od
e
Peer
.
.
.
commit
|
commitdiff
|
tree
2022-01-06
Yan
n
ick
Moy
[Ada] Proof of runtime unit f
o
r non-bin
a
ry modu
l
ar
.
.
.
commit
|
commitdiff
|
tree
2022-01-06
Y
a
nnick Moy
[Ada
]
Proo
f
of
ru
n
time unit
s
for binary modular exponen
t
iat
i
on
commit
|
commitdiff
|
tree
2022-01-05
Y
annick M
o
y
[Ad
a
]
Add contracts
f
or
t
he
proo
f
of S
y
s
t
e
m
.
Arith_
1
2
8
commit
|
commitdiff
|
tree
2022-01-05
Yanni
c
k Moy
[
A
da]
P
roof of run
t
i
m
e units
for integer expon
e
ntiation
.
.
.
commit
|
commitdiff
|
tree
2022-01-05
Yannick Moy
[Ada] Proof of ru
n
time units for
i
n
t
e
ger
ex
p
onentia
t
i
on
.
.
.
commit
|
commitdiff
|
tree
2022-01-05
Yannick Mo
y
[
A
da] Renam
e
param
e
ter-de
p
e
n
dent constants
in generic
.
.
.
commit
|
commitdiff
|
tree
2022-01-05
Yann
i
ck
M
oy
[Ada] Fi
x
l
e
m
ma in g
e
ner
i
c unit Sys
t
em
.
Arith_Double
commit
|
commitdiff
|
tree
2021-12-02
Yanni
c
k Moy
[Ada] Proof
o
f
System
.
Arit
h
_32 fo
r
dou
b
le arithmetic
.
.
.
commit
|
commitdiff
|
tree
2021-12-02
Yann
i
c
k
Moy
[Ada] Amend p
r
oof
o
f Syste
m
.
Ari
t
h_Double to rem
o
ve
.
.
.
commit
|
commitdiff
|
tree
2021-12-02
Y
a
n
n
i
ck Moy
[Ada] A
d
d pragma
Annotate for CodeP
e
er ana
l
ysi
s
commit
|
commitdiff
|
tree
2021-12-02
Yannick
M
oy
[Ada]
P
roof of support units
f
or 'Wid
t
h on signed
i
ntegers
commit
|
commitdiff
|
tree
2021-12-02
Y
annick M
o
y
[Ada] Proof of Interface
s
.
C with SPARK
commit
|
commitdiff
|
tree
2021-12-02
Yanni
c
k Moy
[
Ada] Proof of System
.
V
a
l
_
Util
util
i
t
i
es for 'Value
.
.
.
commit
|
commitdiff
|
tree
2021-12-02
Yan
n
ick Moy
[Ada] Proof of Boolean'Image a
n
d Boolean'Value
commit
|
commitdiff
|
tree
2021-12-01
Yannick Moy
[Ada] Improv
e
er
r
or messages for dot notation
w
h
e
n
.
.
.
commit
|
commitdiff
|
tree
2021-12-01
Yannick Moy
[Ada] Add
q
uer
y
for extend
e
d
pre
c
ision floating-poi
n
t
.
.
.
commit
|
commitdiff
|
tree
2021-12-01
Y
annick Moy
[Ada] Improve mess
a
ges on
incorrect state refinement
.
.
.
commit
|
commitdiff
|
tree
2021-11-10
Yannick Moy
[A
d
a] Create explicit gho
s
t
mirror unit for big i
n
tegers
commit
|
commitdiff
|
tree
2021-11-10
Yan
n
ick Moy
[Ada] Bet
t
er e
r
ror m
e
ssage on mis
s
ing pa
r
enthe
s
es
commit
|
commitdiff
|
tree
2021-11-09
Yannick Mo
y
[Ad
a
] Compl
e
te support for
p
refixed call on subtypes
.
.
.
commit
|
commitdiff
|
tree
2021-11-09
Yannick
Moy
[Ada]
F
ix supp
o
r
t
for
prefixed call with i
n
complete
.
.
.
commit
|
commitdiff
|
tree
2021-10-25
Yannick
M
oy
[Ada] Issu
e
error on inval
i
d use of Ghost inside p
r
agm
a
.
.
.
commit
|
commitdiff
|
tree
2021-10-20
Ya
n
nick Moy
[
Ada] Proof
o
f
t
h
e runtime
s
u
p
port for attri
b
ute 'W
i
dt
h
commit
|
commitdiff
|
tree
2021-10-20
Ya
n
nick Moy
[
A
da]
P
rovide
d
ummy bod
y
for big integers l
i
brary
u
sed
.
.
.
commit
|
commitdiff
|
tree
2021-10-20
Y
a
nnick Moy
[Ad
a
] I
s
sue warning on unu
s
ed quantified
e
xpres
s
io
n
commit
|
commitdiff
|
tree
2021-10-05
Ya
n
nick Moy
[Ad
a
] I
m
prove error m
e
ssage on
a
r
r
ay aggre
g
ates
commit
|
commitdiff
|
tree
2021-10-05
Yannick Moy
[Ada] Improve er
r
or mess
a
ge on mi
s
sing al
l
/for in
q
u
antified
.
.
.
commit
|
commitdiff
|
tree
2021-10-05
Y
annick Moy
[Ada] Proof of A
d
a
.
Strin
g
s
.
Maps
commit
|
commitdiff
|
tree
2021-10-05
Yannick Moy
[Ada] P
r
oof
o
f
A
da
.
C
h
ar
a
cters
.
Handling
commit
|
commitdiff
|
tree
2021-10-04
Yannick Moy
[
A
da] Mark Ada
.
Tex
t
_IO in SPARK
commit
|
commitdiff
|
tree
2021-10-04
Yannick Moy
[
A
da] Add Ada
R
M desc
r
ipt
i
o
n of Ada
.
Strings
.
Bounded
.
.
.
commit
|
commitdiff
|
tree
2021-09-23
Yan
n
ick
M
o
y
[Ada]
Minimize parts
o
f A
d
a
.
St
r
i
n
gs
.
Fixed
m
arked SPARK_Mo
d
e
.
.
.
commit
|
commitdiff
|
tree
2021-09-22
Yannick Moy
[Ada] Simplify contract of A
d
a
.
Str
i
ngs
.
Fixed
.
Trim
for
.
.
.
commit
|
commitdiff
|
tree
2021-09-22
Yannick Moy
[Ada] Spurious
er
r
o
r
on def
e
rr
e
d
c
o
nstant with
p
redica
t
e
commit
|
commitdiff
|
tree
2021-09-22
Y
a
nni
c
k Moy
[
Ada]
Clar
i
f
y parts
of Ada
.
S
tri
n
gs
.
Unbou
n
ded in
SPARK
.
.
.
commit
|
commitdiff
|
tree
2021-09-22
Yann
i
ck Moy
[
Ada] Add adequate guard before c
a
l
l
ing First_Rep_Item
commit
|
commitdiff
|
tree
2021-09-22
Y
annick Moy
[Ad
a
]
Fix
i
nfinit
e
loo
p
in co
m
pila
t
i
on o
f
illegal code
commit
|
commitdiff
|
tree
2021-09-22
Yan
n
ick
M
o
y
[Ada] More preci
s
e an
a
lysis of
f
unction
renam
i
ngs in
.
.
.
commit
|
commitdiff
|
tree
2021-09-22
Yanni
c
k Mo
y
[Ada]
Fi
x
a
ccess
to predicat
e
d pa
r
ent in
I
type
commit
|
commitdiff
|
tree
2021-09-22
Yan
n
i
c
k Moy
[Ada]
Fix obsolete comments/n
a
me r
e
fe
r
r
ing t
o
g
i
rder
.
.
.
commit
|
commitdiff
|
tree
2021-09-21
Y
a
nn
i
ck Moy
[Ada] Rename "option
a
l" node subtypes that allow Em
p
ty
commit
|
commitdiff
|
tree
2021-09-21
Yannick
Moy
[Ada] Excepti
o
n r
a
ised o
n
em
p
ty file in GNA
T
prov
e
mode
commit
|
commitdiff
|
tree
2021-07-08
Yannic
k
M
o
y
[Ada] Skip types in error for test to comput
e
ar
r
ay
.
.
.
commit
|
commitdiff
|
tree
2021-07-08
Yannick Moy
[A
d
a] Fi
x
o
n computation of packed
a
rra
y
size in case
.
.
.
commit
|
commitdiff
|
tree
2021-07-08
Yannick Moy
[Ada] Compute s
i
zes when possible fo
r
packed array
.
.
.
commit
|
commitdiff
|
tree
2021-07-07
Y
a
nnick Mo
y
[Ada] Simplify handling
o
f sure e
r
ror
s
i
n
GNATprove
.
.
.
commit
|
commitdiff
|
tree
2021-07-07
Yanni
c
k Moy
[A
d
a] Fix pr
e
condition of
C
ot for code
ana
l
yzers
commit
|
commitdiff
|
tree
2021-07-06
Yannick Moy
[
A
d
a
] Missing space
i
n erro
r
messag
e
for pattern matching
commit
|
commitdiff
|
tree
2021-07-05
Yannick
Moy
[Ada] Adap
t
S
PA
R
K RM rule o
n
non-effe
c
t
i
vely
volat
i
le
.
.
.
commit
|
commitdiff
|
tree
2021-07-05
Yan
n
ick Moy
[Ada] Adapt SPARK checking af
t
er change in rules rega
r
di
n
g
.
.
.
commit
|
commitdiff
|
tree
2021-06-16
Yannick Moy
[
Ada] Do not
generate an I
t
ype_Reference node
f
or sl
i
ces
.
.
.
commit
|
commitdiff
|
tree
2021-06-15
Y
a
nnick Mo
y
[Ad
a
] Ex
t
end function to retrieve fi
r
st/last
no
d
e
s
.
.
.
commit
|
commitdiff
|
tree
2021-06-15
Yann
i
ck Moy
[Ada]
C
larify the semant
i
cs
o
f signe
d
intrinsic shift
.
.
.
commit
|
commitdiff
|
tree
2021-05-07
Yannick M
o
y
[
A
da] Generate war
n
ing for negativ
e
li
t
eral of
a modul
a
r
.
.
.
commit
|
commitdiff
|
tree
2021-05-04
Yannic
k
Moy
[
A
da]
M
inor
t
weak i
n
pret
t
y-prin
t
ing of
e
x
press
i
o
ns
commit
|
commitdiff
|
tree
2021-05-04
Y
a
nn
i
ck Moy
[
Ada
]
Move match fu
n
ction for pr
a
gma Warni
n
gs to pu
b
lic
.
.
.
commit
|
commitdiff
|
tree
2021-05-04
Yannick Moy
[
Ada
]
Use error m
a
r
k
e
r f
o
r mes
s
a
g
es in G
N
ATprove mode
commit
|
commitdiff
|
tree
2021-05-04
Yannick Moy
[Ada] Fix cont
i
n
uation me
s
sage for
missing A
L
L in access
.
.
.
commit
|
commitdiff
|
tree
2021-04-29
Yannick M
o
y
[Ada] Add c
o
l
o
rs to GNATprove messages output to a
.
.
.
commit
|
commitdiff
|
tree
2021-04-29
Yannick M
o
y
[Ada] Fix evaluati
o
n
of expressions in inlined code
commit
|
commitdiff
|
tree
2021-04-29
Ya
n
nick Moy
[Ada] Fixes in the
u
se of spans fo
r
err
o
r locatio
n
s
commit
|
commitdiff
|
tree
2021-04-28
Yannick Moy
[
A
da] Use spa
n
s i
n
stead of locations f
o
r compiler diagnostics
commit
|
commitdiff
|
tree
2021-04-28
Y
annic
k
Moy
[A
d
a] Improve
e
r
r
or me
s
sage f
o
r ghost in predicate
commit
|
commitdiff
|
tree
2020-12-17
Yannic
k
M
oy
[Ada] Fi
x
es for GNAT
e
rror/warning messages
commit
|
commitdiff
|
tree
2020-12-16
Y
a
nn
i
ck Moy
[
A
da
]
Mark generic b
o
dy ou
t
side o
f
SPARK
commit
|
commitdiff
|
tree
2020-12-15
Y
annic
k
Moy
[Ada
]
Ma
r
k generic body outside of
S
PARK
commit
|
commitdiff
|
tree
2020-12-14
Yannick Moy
[Ada] Fix warning control cha
r
acter for message o
n
.
.
.
commit
|
commitdiff
|
tree
2020-12-14
Yann
i
ck
M
oy
[Ada
]
Ref
i
ne
e
rror
m
e
s
sag
e
s on ille
g
a
l Refine
d
_State
.
.
.
commit
|
commitdiff
|
tree
2020-12-14
Yanni
c
k Moy
[Ada
]
Corre
c
t
l
y
mark
subprogram as not al
w
ay
s
inlined
.
.
.
commit
|
commitdiff
|
tree
2020-11-30
Yan
n
i
c
k M
o
y
[Ada] Add comment on
s
p
eci
a
l
H
eap variable used
i
n
.
.
.
commit
|
commitdiff
|
tree
2020-11-30
Yanni
c
k Moy
[Ada] A
d
d c
o
ntinuation
message when
o
t
h
ers choice no
t
.
.
.
commit
|
commitdiff
|
tree
2020-11-27
Yannick Moy
[
A
da
]
D
o
not app
l
y range chec
k
s inside generics in
.
.
.
commit
|
commitdiff
|
tree
2020-11-26
Yannic
k
Moy
[Ada] New wa
r
ning on questionable missing pa
r
e
n
thes
e
s
commit
|
commitdiff
|
tree
2020-11-26
Ya
n
nick
M
oy
[
Ada] Issue advi
c
e for
e
rror regarding Old/Loop_En
t
r
y
.
.
.
commit
|
commitdiff
|
tree
2020-11-25
Yannick Moy
[Ada] Min
i
mi
z
e si
d
e-effect removal in GNA
T
prove
mode
commit
|
commitdiff
|
tree
next