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: Disable PIE mode during the build of the Ada front-end
2023-05-29
Y
a
nnick Moy
a
d
a: Restor
e
SPAR
K
_Mode On for numerical fun
c
ti
o
n
s
commit
|
commitdiff
|
tree
2023-05-26
Yannick Mo
y
ada: Default ini
t
ialize
e
ntity to avoid CodePeer messag
e
commit
|
commitdiff
|
tree
2023-05-26
Yannic
k
M
oy
ada:
Minor doc
clarification
commit
|
commitdiff
|
tree
2023-05-26
Yann
i
ck Moy
ada: Compl
e
te contra
c
ts of SPARK units
commit
|
commitdiff
|
tree
2023-05-23
Yannick Mo
y
a
d
a: Add default val
u
e at initializ
a
t
ion for CodePee
r
commit
|
commitdiff
|
tree
2023-05-23
Yanni
c
k Moy
ada: Facilitate pro
o
f
of Inte
r
fa
c
es
.
C
.
To_Ad
a
commit
|
commitdiff
|
tree
2023-05-16
Yannick Moy
ada: Update proof of run
t
i
m
e units
commit
|
commitdiff
|
tree
2023-05-16
Yannick M
o
y
ada: Simpli
f
y dramat
i
cally
g
host code for proof of
.
.
.
commit
|
commitdiff
|
tree
2023-05-16
Y
a
nnick
M
oy
ada: Add
interme
d
i
ate ass
e
rtions for proof
o
f Sup
e
r
_Tail
commit
|
commitdiff
|
tree
2023-05-16
Yan
n
ick Mo
y
ada: Set Loop_Variant assertio
n
policy t
o
I
gno
r
e
in
.
.
.
commit
|
commitdiff
|
tree
2023-05-16
Yannick Moy
a
d
a
:
Res
t
ore p
r
o
of
o
f System
.
Arith_Doub
l
e
commit
|
commitdiff
|
tree
2023-05-15
Yannick Mo
y
a
da: Add annot
a
tions fo
r
proof of termina
t
i
o
n of
ru
n
time
.
.
.
commit
|
commitdiff
|
tree
2023-05-15
Yannick Moy
ada:
R
ecover proof of runtime uni
t
s
commit
|
commitdiff
|
tree
2023-05-15
Yann
i
ck Moy
a
da: Recover proo
f
o
f
Inte
r
face
s
.
C for termination
commit
|
commitdiff
|
tree
2023-05-15
Yann
i
ck Moy
ada: Up
d
at
e
comme
n
t
a
fter SPARK
R
M
change
commit
|
commitdiff
|
tree
2023-05-15
Ya
n
nick
Moy
ada: Fix handling
o
f pragma Warnings (Toolname,
O
ff
/
O
n)
commit
|
commitdiff
|
tree
2023-05-15
Ya
n
nick Moy
ada: Allow
p
r
agmas Annotate
b
etween loop pragmas
commit
|
commitdiff
|
tree
2022-12-06
Yannick M
o
y
ada:
Al
l
ow No_C
a
c
h
ing on volati
l
e ty
p
es
commit
|
commitdiff
|
tree
2022-11-28
Yannick Moy
ada: Implement change
t
o
SPA
R
K RM rule on state refine
m
ent
commit
|
commitdiff
|
tree
2022-11-14
Yannick Moy
ad
a
: Fix err
o
r
on SPARK_
M
od
e
on li
b
r
ary-leve
l
separ
a
t
e
.
.
.
commit
|
commitdiff
|
tree
2022-11-14
Yannick Moy
ada: Improve location of error
m
es
s
ages in
i
n
stantiations
commit
|
commitdiff
|
tree
2022-10-06
Y
a
nnic
k
Moy
ada
:
Do not issue c
o
mp
i
l
e
r warn
i
ngs in GNATprove mod
e
commit
|
commitdiff
|
tree
2022-09-12
Yannick Moy
[
Ad
a
]
J
ustify false alarm fr
o
m CodePeer
a
nalysis of
.
.
.
commit
|
commitdiff
|
tree
2022-09-12
Yann
i
c
k Moy
[Ada] Accep
t
e
xplicit SPARK_Mo
d
e Auto as con
f
igur
a
tion
.
.
.
commit
|
commitdiff
|
tree
2022-09-12
Yan
n
ic
k
Moy
[A
d
a] Reject
u
se
in S
P
ARK of
A
sm intrinsics for code
.
.
.
commit
|
commitdiff
|
tree
2022-09-02
Yan
n
ick Moy
[Ada] Recove
r
p
r
oof of Scaled_D
i
vide in System
.
A
r
ith_64
commit
|
commitdiff
|
tree
2022-07-13
Ya
n
nick Moy
[Ada] Fix incorrect hand
l
ing of
G
ho
s
t
a
spect
commit
|
commitdiff
|
tree
2022-07-13
Yannick Moy
[A
d
a
]
F
ix proof of runtime unit
S
ystem
.
Ari
t
h_64
commit
|
commitdiff
|
tree
2022-07-13
Yannick
M
oy
[
Ada]
Fix
a
utomatic proof on Syste
m
.
Arith_32
commit
|
commitdiff
|
tree
2022-07-12
Ya
n
nick
M
oy
[Ada] Ignore swi
t
c
he
s
for controlling fron
t
end warnings
.
.
.
commit
|
commitdiff
|
tree
2022-07-06
Yannick Moy
[Ada] De
f
e
r
red const
a
nt
c
onsidered as not preelaborable
commit
|
commitdiff
|
tree
2022-07-06
Ya
n
nick Moy
[Ad
a
]
Support ghost generic formal p
a
rame
t
ers
commit
|
commitdiff
|
tree
2022-07-05
Ya
n
n
i
ck Moy
[Ada] F
i
x spurious error on object
r
enamin
g
wit
h
ghost
.
.
.
commit
|
commitdiff
|
tree
2022-07-05
Yanni
c
k
Moy
[Ada] Spurious error on qualif
i
ed pref
i
x
in Pack
.
Func
.
.
.
commit
|
commitdiff
|
tree
2022-06-02
Yannick Moy
[Ada] Fix spuri
o
us errors on ghost cod
e
i
n
gen
e
r
ics
commit
|
commitdiff
|
tree
2022-06-02
Yannick Moy
[Ada
]
Is
s
ue
e
rro
r
s on wrong co
n
text
f
or ghost entiti
e
s
commit
|
commitdiff
|
tree
2022-06-02
Yannick Moy
[Ada]
R
e
moval of dea
d
code An
a
lyze_
L
abel_Entity
commit
|
commitdiff
|
tree
2022-06-01
Yan
n
i
c
k
Moy
[Ada] All
o
w confi
r
ming v
o
lat
i
le
p
r
o
pe
r
ties
on No
_
Cac
h
ing
.
.
.
commit
|
commitdiff
|
tree
2022-06-01
Y
anni
c
k Moy
[Ada] Fix cla
s
sification of Subprogram_Variant
as asser
t
io
n
.
.
.
commit
|
commitdiff
|
tree
2022-06-01
Yannick Moy
[Ada] Issue a warn
i
n
g on enti
t
y hidde
n
in use_cl
a
use
.
.
.
commit
|
commitdiff
|
tree
2022-06-01
Yannick Moy
[Ada
]
I
s
sue b
e
tter
error message
for ou
t
-of-order ke
y
words
.
.
.
commit
|
commitdiff
|
tree
2022-05-30
Y
a
nnick Moy
[Ada]
U
pdate p
r
oofs of double arith
m
e
t
ic unit after
.
.
.
commit
|
commitdiff
|
tree
2022-05-30
Y
annick M
o
y
[A
d
a]
A
d
a
pt
proof of runtime unit s-arit32
commit
|
commitdiff
|
tree
2022-05-30
Yanni
c
k M
o
y
[Ada] PR ada/1053
0
3 F
i
x us
e
of Asse
r
ti
o
n_Policy in
.
.
.
commit
|
commitdiff
|
tree
2022-05-19
Yannick Moy
[Ad
a
] Further adapt proo
f
o
f double
arit
h
metic
runtime
.
.
.
commit
|
commitdiff
|
tree
2022-05-18
Yanni
c
k Moy
[
A
da] Adap
t
proo
f
of double arithmetic runtime
unit
commit
|
commitdiff
|
tree
2022-05-18
Y
annick Moy
[Ada] Fix proof of runtim
e
u
n
its
commit
|
commitdiff
|
tree
2022-05-18
Yannick Moy
[Ada
]
Spurious error on freez
i
ng o
f
t
a
gge
d
types i
n
.
.
.
commit
|
commitdiff
|
tree
2022-05-17
Yannick Moy
[
A
da] A
l
low i
n
l
i
ning for proof insi
d
e generics
commit
|
commitdiff
|
tree
2022-05-17
Yanni
c
k M
o
y
[Ada]
F
ix insertion of declar
a
tion
insi
d
e quantified
.
.
.
commit
|
commitdiff
|
tree
2022-05-16
Y
a
nnick Moy
[
Ada] Fix proof of double
a
rit
h
metic units
commit
|
commitdiff
|
tree
2022-05-16
Yannick Moy
[Ada] Up
d
ate commen
t
ju
s
ti
f
yin
g
non-inlinin
g
fo
r
p
r
oof
.
.
.
commit
|
commitdiff
|
tree
2022-05-13
Yannick
M
oy
[
A
da]
S
impl
i
fy helper units for forma
l
hashed set
s
.
.
.
commit
|
commitdiff
|
tree
2022-05-13
Yannick Moy
[A
d
a] Adapt b
o
dy of formal set
s
and maps for S
P
A
RK
commit
|
commitdiff
|
tree
2022-05-13
Yannick
M
oy
[Ada] Remove d
e
penden
c
y on tampering checks and contr
o
lled
.
.
.
commit
|
commitdiff
|
tree
2022-05-13
Yannick Moy
[Ada] Faci
l
itate proof of Overwrite in b
o
unded stri
n
gs
.
.
.
commit
|
commitdiff
|
tree
2022-05-12
Yannick Moy
[A
d
a]
Remove
usele
s
s
p
ragma
W
arnings Off from
r
u
n
time
.
.
.
commit
|
commitdiff
|
tree
2022-05-12
Yannick
Moy
[Ada] Do not i
s
sue a warning
o
n a pos
t
condition of
.
.
.
commit
|
commitdiff
|
tree
2022-05-12
Y
a
nnick M
o
y
[
Ada] Add ghos
t
code to facilitate
proof
w
i
t
h SPARK
commit
|
commitdiff
|
tree
2022-05-12
Yannic
k
Moy
[Ada] Remove use
of
us
e
-clauses in loaded runtime
u
nits
commit
|
commitdiff
|
tree
2022-05-12
Yannic
k
Moy
[Ada] Adapt CodePee
r
an
a
lysis of
G
NAT to chan
g
es
i
n
.
.
.
commit
|
commitdiff
|
tree
2022-05-12
Yanni
c
k
M
oy
[Ada
]
Pro
o
f of 'I
m
age
s
upport f
o
r
s
i
gned integers
commit
|
commitdiff
|
tree
2022-05-11
Yann
i
c
k
Mo
y
[Ada] Proof of 'Im
a
ge support for unsign
e
d
integers
commit
|
commitdiff
|
tree
2022-05-11
Yann
i
ck Moy
[Ada] A
d
apt proof o
f
System
.
Arith_Dou
b
le after
u
pdate
.
.
.
commit
|
commitdiff
|
tree
2022-05-10
Y
annick Moy
[Ad
a
] Fix indentat
i
on t
o
follow unifor
m
style ac
r
oss
.
.
.
commit
|
commitdiff
|
tree
2022-05-09
Yanni
c
k
M
oy
[A
d
a
]
Suggest us
e
o
f First_Va
l
id/Last_
V
a
lid o
n
type
.
.
.
commit
|
commitdiff
|
tree
2022-05-09
Yannic
k
Moy
[Ada
]
Set Error_Msg_Wa
r
n
befo
r
e
use of << ins
e
rtion
commit
|
commitdiff
|
tree
2022-01-11
Yannick Moy
[Ada] Adapt
proof of Syste
m
.
A
rith_Doub
l
e
commit
|
commitdiff
|
tree
2022-01-11
Yannick
Moy
[Ad
a
]
Recover
p
roof
of Ada
.
Strings
.
Fixed
w
ith
assertions
commit
|
commitdiff
|
tree
2022-01-11
Yan
n
ick Moy
[Ad
a
] Pr
o
of of unit Syste
m
.
C
ase
_
Util
commit
|
commitdiff
|
tree
2022-01-11
Yanni
c
k Moy
[
A
da] Adapt ghost cod
e
to mainta
i
n proof
commit
|
commitdiff
|
tree
2022-01-11
Ya
n
nick Moy
[Ada]
P
roof of S
y
stem
.
Vectors
.
Boolean_Opera
t
i
ons
commit
|
commitdiff
|
tree
2022-01-06
Y
a
nni
c
k Moy
[Ada] P
r
oo
f
of System
.
G
e
n
e
r
ic_Ar
r
a
y_Operations at
s
ilver
.
.
.
commit
|
commitdiff
|
tree
2022-01-06
Yannick Moy
[Ada
]
Justify fa
l
se positive
m
e
ssage from CodePeer
.
.
.
commit
|
commitdiff
|
tree
2022-01-06
Y
annick Moy
[Ad
a
]
Pr
o
of of
r
untim
e
un
i
t for non-binary m
o
du
l
ar
.
.
.
commit
|
commitdiff
|
tree
2022-01-06
Yanni
c
k Moy
[
Ada] P
r
oof
o
f
run
t
ime units for bi
n
ary
m
odular
exponentiation
commit
|
commitdiff
|
tree
2022-01-05
Yannick Moy
[Ada] Add co
n
tracts for the proof of S
y
stem
.
Arith_12
8
commit
|
commitdiff
|
tree
2022-01-05
Yannick M
o
y
[Ada] Proof of runtime u
n
i
t
s
f
or integer ex
p
onentiation
.
.
.
commit
|
commitdiff
|
tree
2022-01-05
Yannick Moy
[Ada] Proof of runtime uni
t
s for intege
r
expone
n
tiation
.
.
.
commit
|
commitdiff
|
tree
2022-01-05
Yann
i
c
k
Moy
[Ada] Ren
a
me par
a
meter-dependent constan
t
s in generi
c
.
.
.
commit
|
commitdiff
|
tree
2022-01-05
Yannick Moy
[Ada] F
i
x lemma in generi
c
unit
Sys
t
em
.
Arith
_
Do
u
b
l
e
commit
|
commitdiff
|
tree
2021-12-02
Yannick Moy
[
Ada]
Pr
o
o
f o
f
S
y
ste
m
.
Arith_32 f
o
r double
a
r
i
thmet
i
c
.
.
.
commit
|
commitdiff
|
tree
2021-12-02
Y
a
nnic
k
Mo
y
[
A
da] Amen
d
pro
o
f of Sy
s
tem
.
Arit
h
_Double t
o
remo
v
e
.
.
.
commit
|
commitdiff
|
tree
2021-12-02
Y
a
n
nick Moy
[Ada] A
d
d pragma Annotat
e
for CodePee
r
analysis
commit
|
commitdiff
|
tree
2021-12-02
Yanni
c
k Mo
y
[
A
da]
P
r
o
of of support unit
s
fo
r
'
W
idth on signed integers
commit
|
commitdiff
|
tree
2021-12-02
Yannick Moy
[Ada] Proof of Interfaces
.
C with SPAR
K
commit
|
commitdiff
|
tree
2021-12-02
Yannic
k
Moy
[A
d
a] Proof of System
.
V
a
l_U
t
il utiliti
e
s for 'V
a
lu
e
.
.
.
commit
|
commitdiff
|
tree
2021-12-02
Y
annick Moy
[Ada] Proof of Boole
a
n'Image
a
nd
B
ool
e
an'Va
l
u
e
commit
|
commitdiff
|
tree
2021-12-01
Yannick Moy
[Ada] Im
p
r
ov
e
erro
r
messages for dot notat
i
on when
.
.
.
commit
|
commitdiff
|
tree
2021-12-01
Yannick Moy
[
A
d
a] Add q
u
ery for
exte
n
d
ed
precision floating-
p
o
i
nt
.
.
.
commit
|
commitdiff
|
tree
2021-12-01
Yannick
Moy
[
Ada] Improve mes
s
ages on incorrec
t
s
tate refineme
n
t
.
.
.
commit
|
commitdiff
|
tree
2021-11-10
Yan
n
ic
k
M
oy
[Ada]
C
r
e
at
e
expli
c
it ghost mi
r
ror u
n
it for big intege
r
s
commit
|
commitdiff
|
tree
2021-11-10
Yann
i
ck Moy
[Ad
a
] Better error message on mi
s
sing parentheses
commit
|
commitdiff
|
tree
2021-11-09
Y
anni
c
k
Moy
[Ada] Complete
support for
p
refi
x
ed cal
l
on subty
p
es
.
.
.
commit
|
commitdiff
|
tree
2021-11-09
Yannic
k
M
o
y
[A
d
a
]
Fix support for pref
i
x
ed call
w
ith incomplete
.
.
.
commit
|
commitdiff
|
tree
2021-10-25
Yannic
k
Moy
[
A
da] Issue error
o
n
invalid use of
G
ho
s
t in
s
id
e
p
rag
m
a
.
.
.
commit
|
commitdiff
|
tree
2021-10-20
Ya
n
nick Moy
[A
d
a] Proof o
f
the r
u
nt
i
me sup
p
ort fo
r
attribut
e
'Width
commit
|
commitdiff
|
tree
2021-10-20
Ya
n
nic
k
Mo
y
[A
d
a
]
Provide dummy bod
y
for big i
n
te
g
e
r
s library
u
sed
.
.
.
commit
|
commitdiff
|
tree
2021-10-20
Yannick Mo
y
[Ada] Iss
u
e warning on unused quantified
e
xpres
s
ion
commit
|
commitdiff
|
tree
2021-10-05
Y
a
nnick Moy
[Ada]
Impro
v
e
e
rror message on array agg
r
egates
commit
|
commitdiff
|
tree
next