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: Minor tweaks for comparison operators
2023-10-19
Yan
n
ick M
o
y
a
d
a: Support new SP
A
R
K
a
spect Side_Effects
commit
|
commitdiff
|
tree
2023-09-26
Yannick Moy
a
da: Clarify RM ref
e
r
ences
that justify a constraint
.
.
.
commit
|
commitdiff
|
tree
2023-09-14
Y
annick M
o
y
ada: I
m
prove detection of d
e
acti
v
ated code
for warnings
.
.
.
commit
|
commitdiff
|
tree
2023-08-07
Yanni
c
k Moy
ad
a
: Cra
s
h
in GNATprove due to
w
rong
d
etec
t
ion of i
n
lining
commit
|
commitdiff
|
tree
2023-08-01
Yann
i
ck Moy
a
d
a: Fix printing of
n
umbers in JSO
N
output for data
.
.
.
commit
|
commitdiff
|
tree
2023-08-01
Yan
n
ick Moy
ada:
Disa
b
le
i
nlin
i
n
g of subprog
r
a
m
s
w
ith
Skip(_F
l
ow_And
.
.
.
commit
|
commitdiff
|
tree
2023-08-01
Y
annick M
o
y
ada:
F
ix genera
t
ion of JS
O
N
ou
t
p
ut for
d
a
t
a r
e
p
re
s
entation
commit
|
commitdiff
|
tree
2023-07-18
Yann
i
ck Moy
ada: All
o
w w
a
rni
n
gs with explain co
d
e
commit
|
commitdiff
|
tree
2023-07-10
Y
a
nnick Moy
ada: Simplify
assertion to re
m
ove
C
odePeer messa
g
e
commit
|
commitdiff
|
tree
2023-07-10
Yanni
c
k Moy
ada: Adapt pro
o
f
o
f System
.
Arith_
D
ouble to remove CVC4
commit
|
commitdiff
|
tree
2023-07-06
Yann
i
ck Moy
ada: Improve e
r
ror mess
a
ge on viola
t
io
n
o
f
SPARK_Mode
.
.
.
commit
|
commitdiff
|
tree
2023-07-04
Yan
n
ick Moy
ada
:
Fix list o
f
inhe
r
ited subp
r
ograms
i
n
q
u
e
ry f
o
r
.
.
.
commit
|
commitdiff
|
tree
2023-06-20
Y
annick Moy
a
da: Fix crash on
in
l
ining in GNATprove
commit
|
commitdiff
|
tree
2023-06-20
Yanni
c
k Moy
ada: Do not issue
warn
i
ng on postcondi
t
ion in some
.
.
.
commit
|
commitdiff
|
tree
2023-06-20
Y
annick
M
o
y
ada:
A
dd the ability to add
e
rror codes to error messages
commit
|
commitdiff
|
tree
2023-06-20
Y
annick Moy
a
da: Update
a
nnotations in runtim
e
for proof
commit
|
commitdiff
|
tree
2023-06-15
Yannic
k
Moy
ada:
Reject Loop_Entry inside
pre
f
ix of
Loop_Entry
commit
|
commitdiff
|
tree
2023-06-13
Yannick Moy
a
d
a: Mar
k
attribute Ini
t
ialized as ghost code
commit
|
commitdiff
|
tree
2023-06-13
Yannick Moy
ada: Use gh
o
st
p
re
d
i
c
a
te in standard libra
r
y
commit
|
commitdiff
|
tree
2023-06-13
Yannick Moy
a
da
:
Support new
GNAT-specific aspect
Ghost
_
Predicat
e
commit
|
commitdiff
|
tree
2023-05-29
Yann
i
ck
Moy
ada: Rest
o
re SP
A
R
K
_Mode On
f
or numeric
a
l functio
n
s
commit
|
commitdiff
|
tree
2023-05-26
Yannick Moy
ada
:
Defaul
t
initialize ent
i
t
y t
o
avoid Cod
e
Pe
e
r
message
commit
|
commitdiff
|
tree
2023-05-26
Ya
n
nic
k
Moy
ada: Mi
n
or doc
cl
a
rificat
i
on
commit
|
commitdiff
|
tree
2023-05-26
Yannick Moy
a
d
a
: Com
p
lete contracts
o
f
SPARK uni
t
s
commit
|
commitdiff
|
tree
2023-05-23
Ya
n
n
i
ck Moy
ada: Add d
e
fau
l
t value at in
i
tializati
o
n for CodePeer
commit
|
commitdiff
|
tree
2023-05-23
Y
a
nnic
k
Moy
ada: Faci
l
ita
t
e
p
roof
o
f
Interfaces
.
C
.
To
_
Ada
commit
|
commitdiff
|
tree
2023-05-16
Yann
i
ck Moy
ad
a
: Update proof of
r
untime units
commit
|
commitdiff
|
tree
2023-05-16
Yannick Moy
ada: Sim
p
l
i
fy dramatically ghost code fo
r
pro
o
f of
.
.
.
commit
|
commitdiff
|
tree
2023-05-16
Yannick Mo
y
ada:
A
d
d i
n
termediate
a
ss
e
rt
i
ons for
p
roof of Super_Tail
commit
|
commitdiff
|
tree
2023-05-16
Yan
n
ic
k
Moy
a
da: Set L
o
op_Variant
assertion
p
olicy to Ignore in
.
.
.
commit
|
commitdiff
|
tree
2023-05-16
Yannick
Moy
ada: Restore proof of S
y
s
t
em
.
Arith_Doub
l
e
commit
|
commitdiff
|
tree
2023-05-15
Y
a
nnick M
o
y
ada: Add annotations
fo
r
p
roof
of
t
ermination of runtime
.
.
.
commit
|
commitdiff
|
tree
2023-05-15
Yannick Moy
ada: R
e
cover pro
o
f of runtime units
commit
|
commitdiff
|
tree
2023-05-15
Yannick Moy
ada: Recov
e
r proof of Interfa
c
e
s
.
C
for
termina
t
ion
commit
|
commitdiff
|
tree
2023-05-15
Yann
i
ck Moy
ada: Update
comment a
f
ter SPA
R
K RM cha
n
ge
commit
|
commitdiff
|
tree
2023-05-15
Y
a
nnick Moy
ada: Fix han
d
li
n
g of pragma W
a
rning
s
(To
o
lname, O
f
f/On)
commit
|
commitdiff
|
tree
2023-05-15
Y
ann
i
ck
Moy
a
d
a:
Al
l
ow p
r
agmas
Annotate between loop prag
m
as
commit
|
commitdiff
|
tree
2022-12-06
Yannick Mo
y
ada:
Allow No_Caching on
vo
l
atile
t
ypes
commit
|
commitdiff
|
tree
2022-11-28
Ya
n
ni
c
k Moy
ada: Implement change to
S
PARK RM rule on state
refin
e
ment
commit
|
commitdiff
|
tree
2022-11-14
Yannick M
o
y
ada: F
i
x error
on SPARK_Mode o
n
library-level separat
e
.
.
.
commit
|
commitdiff
|
tree
2022-11-14
Yannick Moy
ada: Imp
r
ove lo
c
ation of error messages i
n
instantiations
commit
|
commitdiff
|
tree
2022-10-06
Ya
n
n
i
c
k Moy
a
d
a: D
o
no
t
i
s
sue compiler warn
i
ngs in
G
NAT
p
rove mode
commit
|
commitdiff
|
tree
2022-09-12
Ya
n
nick
M
oy
[Ada] Justify fals
e
alar
m
from CodePeer analysis of
.
.
.
commit
|
commitdiff
|
tree
2022-09-12
Yannick Moy
[Ad
a
] Accept
ex
p
li
c
it S
P
ARK_Mode Auto as configuration
.
.
.
commit
|
commitdiff
|
tree
2022-09-12
Yan
n
ick M
o
y
[Ad
a
] Reject use in
S
PARK o
f
Asm intrinsic
s
for code
.
.
.
commit
|
commitdiff
|
tree
2022-09-02
Yannick Moy
[Ada] Recover proof of Scal
e
d
_
Di
v
ide in
S
yste
m
.
Arith_64
commit
|
commitdiff
|
tree
2022-07-13
Yannick Moy
[Ada] Fix
inc
o
rr
e
ct handling of Gho
s
t aspect
commit
|
commitdiff
|
tree
2022-07-13
Yannick M
o
y
[Ad
a
] F
i
x proof o
f
r
u
n
time
u
nit S
y
stem
.
Arit
h
_64
commit
|
commitdiff
|
tree
2022-07-13
Yannick Moy
[Ada] Fix a
u
to
m
at
i
c proof on System
.
Arith_3
2
commit
|
commitdiff
|
tree
2022-07-12
Y
ann
i
ck Moy
[
A
da] I
g
n
o
r
e
switches for
c
ontrol
l
ing frontend warnings
.
.
.
commit
|
commitdiff
|
tree
2022-07-06
Ya
n
nick Moy
[Ada] De
f
erred c
o
n
s
ta
n
t considere
d
as not preela
b
orable
commit
|
commitdiff
|
tree
2022-07-06
Yannick Moy
[Ada] Support ghost generic fo
r
mal parameters
commit
|
commitdiff
|
tree
2022-07-05
Yannick
Moy
[A
d
a] Fix spurio
u
s
error
on
o
bjec
t
renaming with g
h
ost
.
.
.
commit
|
commitdiff
|
tree
2022-07-05
Yanni
c
k Moy
[Ada] Spurious error on qua
l
ifi
e
d prefix in Pack
.
Func
.
.
.
commit
|
commitdiff
|
tree
2022-06-02
Yannick
M
oy
[
A
da] Fi
x
spurious e
r
rors on ghos
t
code in generics
commit
|
commitdiff
|
tree
2022-06-02
Yannick Moy
[Ada] Issue error
s
on wrong context for
g
host e
n
tities
commit
|
commitdiff
|
tree
2022-06-02
Y
annick M
o
y
[Ada] Removal
of dead code A
n
al
y
ze
_
Label_Entity
commit
|
commitdiff
|
tree
2022-06-01
Yannick Moy
[
Ada] Allow
c
onfirmi
n
g
v
o
latile properties on N
o
_Caching
.
.
.
commit
|
commitdiff
|
tree
2022-06-01
Y
a
nnick Moy
[Ada] Fix
c
lassification of Subprogra
m
_Varia
n
t as a
s
s
ertion
.
.
.
commit
|
commitdiff
|
tree
2022-06-01
Yannick Moy
[Ada] Issue a w
a
rning on ent
i
ty hi
d
den in us
e
_cla
u
se
.
.
.
commit
|
commitdiff
|
tree
2022-06-01
Yannick
M
oy
[Ada] I
s
sue bett
e
r error mes
s
age
f
or o
u
t
-of-o
r
der keywords
.
.
.
commit
|
commitdiff
|
tree
2022-05-30
Yannick M
o
y
[Ada]
U
pdate proofs of double
a
rit
h
metic uni
t
after
.
.
.
commit
|
commitdiff
|
tree
2022-05-30
Yannick Moy
[Ada
]
Adapt
proof of runtime unit s-a
r
it32
commit
|
commitdiff
|
tree
2022-05-30
Yannick Moy
[Ada] PR
a
da/
1
05
3
0
3
F
ix use of
A
ssertion_Po
l
i
cy in
.
.
.
commit
|
commitdiff
|
tree
2022-05-19
Yannick Moy
[Ada] Further adapt proof
of double a
r
ithmet
i
c
r
untime
.
.
.
commit
|
commitdiff
|
tree
2022-05-18
Yannick
M
oy
[Ada] Adapt proof
of double ar
i
thmetic runtime unit
commit
|
commitdiff
|
tree
2022-05-18
Yannick Moy
[Ada] Fix proof of runti
m
e units
commit
|
commitdiff
|
tree
2022-05-18
Yannick M
o
y
[Ada] Spuri
o
us e
r
ror on
freezing o
f
tag
g
ed types in
.
.
.
commit
|
commitdiff
|
tree
2022-05-17
Y
a
nn
i
ck Moy
[
Ada
]
Allow
i
nlining f
o
r proof
i
nside generi
c
s
commit
|
commitdiff
|
tree
2022-05-17
Yannick Moy
[Ada] Fix i
n
sertion of decl
a
ration
i
nside q
u
antified
.
.
.
commit
|
commitdiff
|
tree
2022-05-16
Yannick Moy
[Ada] Fix pr
o
of of double
arithmeti
c
units
commit
|
commitdiff
|
tree
2022-05-16
Yanni
c
k Moy
[Ada] Update
c
omment justi
f
ying non-inli
n
i
n
g for proof
.
.
.
commit
|
commitdiff
|
tree
2022-05-13
Yannick Moy
[Ada] Simplify helper
units for form
a
l hashed sets
.
.
.
commit
|
commitdiff
|
tree
2022-05-13
Y
a
nnick Moy
[Ada] A
d
apt body of fo
r
mal
s
e
ts and
maps for SPARK
commit
|
commitdiff
|
tree
2022-05-13
Yann
i
ck Moy
[
A
da] Remove depe
n
dency on tamper
i
n
g
chec
k
s and controlle
d
.
.
.
commit
|
commitdiff
|
tree
2022-05-13
Yann
i
c
k
Moy
[Ada] F
a
cilita
t
e proof
o
f
O
v
erwrite
i
n bounded
strings
.
.
.
commit
|
commitdiff
|
tree
2022-05-12
Yan
n
ick Moy
[
Ada] Remove useles
s
pr
a
gma Warnings Off from
r
untime
.
.
.
commit
|
commitdiff
|
tree
2022-05-12
Yannick Moy
[
A
da] Do n
o
t iss
u
e a
w
ar
n
ing on a postco
n
dition of
.
.
.
commit
|
commitdiff
|
tree
2022-05-12
Ya
n
nick Moy
[Ada] Add ghost cod
e
to f
a
cilitate proof wit
h
SPAR
K
commit
|
commitdiff
|
tree
2022-05-12
Yannick Moy
[Ada]
R
emove use
of use-c
l
auses
i
n l
o
ad
e
d runtime un
i
ts
commit
|
commitdiff
|
tree
2022-05-12
Yannick Moy
[Ada] A
d
apt CodeP
e
er anal
y
sis of GNAT to
c
hang
e
s in
.
.
.
commit
|
commitdiff
|
tree
2022-05-12
Yannick Moy
[Ada] Proof of 'Imag
e
supp
o
r
t
for signed
i
ntegers
commit
|
commitdiff
|
tree
2022-05-11
Yannick Moy
[Ad
a
] Proof
o
f 'Ima
g
e
su
p
port for unsigned
integer
s
commit
|
commitdiff
|
tree
2022-05-11
Yannick M
o
y
[
Ada] Adapt
proof
o
f
System
.
Arith
_
Double a
f
t
e
r update
.
.
.
commit
|
commitdiff
|
tree
2022-05-10
Y
annick Moy
[Ada] Fix ind
e
ntatio
n
to follow uniform
sty
l
e
a
c
ross
.
.
.
commit
|
commitdiff
|
tree
2022-05-09
Yannick Mo
y
[
A
da] Su
g
ge
s
t
u
se
of F
i
rst_Valid/
L
ast_Vali
d
on type
.
.
.
commit
|
commitdiff
|
tree
2022-05-09
Ya
n
ni
c
k
M
oy
[Ada]
S
et Error_
M
sg_Warn before u
s
e
of
<< insertion
commit
|
commitdiff
|
tree
2022-01-11
Y
a
nnick
M
o
y
[
A
d
a] Adapt proo
f
of Sys
t
em
.
Arith
_
Doub
l
e
commit
|
commitdiff
|
tree
2022-01-11
Yann
i
ck Moy
[Ada] Recover
p
roof of Ad
a
.
Strings
.
Fixed
w
ith assertions
commit
|
commitdiff
|
tree
2022-01-11
Yanni
c
k
Moy
[Ada] Proof of un
i
t
Sys
t
em
.
Case_Util
commit
|
commitdiff
|
tree
2022-01-11
Yannick Moy
[Ada]
Adap
t
ghos
t
code to maintain proof
commit
|
commitdiff
|
tree
2022-01-11
Y
a
nnick Moy
[A
d
a] P
r
oof of
S
ystem
.
Vectors
.
Boolean_Operations
commit
|
commitdiff
|
tree
2022-01-06
Yannick
M
oy
[
Ada
]
Proof of System
.
Gen
e
r
i
c_Array_Operations at silver
.
.
.
commit
|
commitdiff
|
tree
2022-01-06
Yan
n
ick Moy
[
A
d
a] Justif
y
fals
e
positive messa
g
e from Co
d
ePeer
.
.
.
commit
|
commitdiff
|
tree
2022-01-06
Yannick Moy
[Ada] Pro
o
f of runtime
unit for non-b
i
nary modula
r
.
.
.
commit
|
commitdiff
|
tree
2022-01-06
Yan
n
ick Moy
[
A
d
a
]
P
r
oof of runtim
e
units for b
i
n
ary mo
d
ular expo
n
entiation
commit
|
commitdiff
|
tree
2022-01-05
Y
an
n
i
c
k
M
oy
[Ada] Add con
t
racts for t
h
e
p
roof of
S
ystem
.
A
rit
h
_128
commit
|
commitdiff
|
tree
2022-01-05
Yannic
k
Moy
[A
d
a]
Proof
o
f runtime units for integer exp
o
nentiati
o
n
.
.
.
commit
|
commitdiff
|
tree
2022-01-05
Yannick Moy
[Ada] Pro
o
f of ru
n
tim
e
units
f
or inte
g
er expone
n
tiation
.
.
.
commit
|
commitdiff
|
tree
2022-01-05
Yann
i
ck
M
o
y
[Ada] Rena
m
e par
a
m
e
t
er-depe
n
den
t
consta
n
ts in generic
.
.
.
commit
|
commitdiff
|
tree
next