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
2023-05-29
Yannick Moy
ada: R
e
st
o
re
S
P
AR
K
_Mo
d
e On for numeri
c
al functio
n
s
commit
|
commitdiff
|
tree
2023-05-26
Yan
n
ick Moy
ada: Default ini
t
ialize entity t
o
avoid CodePeer me
s
sage
commit
|
commitdiff
|
tree
2023-05-26
Yannick
M
oy
ad
a
: Minor doc clarif
i
ca
t
i
on
commit
|
commitdiff
|
tree
2023-05-26
Yanni
c
k Moy
a
da: Complete contracts of SPARK units
commit
|
commitdiff
|
tree
2023-05-23
Yannick Moy
ada: Add default value at
initializati
o
n
for C
o
dePeer
commit
|
commitdiff
|
tree
2023-05-23
Y
a
nnick Moy
ada
:
Facilitate pr
o
o
f of Inter
f
aces
.
C
.
To_
A
da
commit
|
commitdiff
|
tree
2023-05-16
Yannic
k
M
oy
ada: Update proof o
f
ru
n
time units
commit
|
commitdiff
|
tree
2023-05-16
Yannick
Mo
y
ada: Si
m
plif
y
dramatically
g
host code for proof of
.
.
.
commit
|
commitdiff
|
tree
2023-05-16
Y
an
n
ick M
o
y
a
d
a: Add in
t
ermedia
t
e assert
i
o
n
s for
p
roof
o
f
Super_
T
ai
l
commit
|
commitdiff
|
tree
2023-05-16
Yannick Moy
ada: Set Loop
_
Va
r
iant assertion policy to Ignore in
.
.
.
commit
|
commitdiff
|
tree
2023-05-16
Y
annick Moy
ada: R
e
store proof of Syst
e
m
.
Ar
i
th_Double
commit
|
commitdiff
|
tree
2023-05-15
Yannick
M
oy
ada:
A
d
d annot
a
tions for proo
f
of ter
m
ina
t
i
o
n of r
u
ntime
.
.
.
commit
|
commitdiff
|
tree
2023-05-15
Yan
n
ick Moy
ada: Re
c
over pro
o
f of runtime units
commit
|
commitdiff
|
tree
2023-05-15
Ya
n
nick Moy
ad
a
:
R
ecover pr
o
of of
Interfac
e
s
.
C
for terminati
o
n
commit
|
commitdiff
|
tree
2023-05-15
Yannick
M
oy
ada:
Updat
e
c
o
m
m
ent
after
S
PARK RM change
commit
|
commitdiff
|
tree
2023-05-15
Ya
n
nick Moy
a
da:
F
ix handling o
f
pragma Warnin
g
s (T
o
olname, Off/On)
commit
|
commitdiff
|
tree
2023-05-15
Yannick
M
o
y
ada: Allow pra
g
ma
s
Annotate bet
w
e
en l
o
op pragmas
commit
|
commitdiff
|
tree
2022-12-06
Yannick Moy
ada
:
A
l
low No
_
Caching on volatile types
commit
|
commitdiff
|
tree
2022-11-28
Ya
n
nick Moy
ada:
Imp
l
eme
n
t
change t
o
SPARK RM
r
ul
e
on state r
e
finement
commit
|
commitdiff
|
tree
2022-11-14
Yannick Moy
a
da: Fix error on SPARK
_
Mode on l
i
brary
-
l
e
vel separa
t
e
.
.
.
commit
|
commitdiff
|
tree
2022-11-14
Yan
n
i
ck M
o
y
a
d
a
: Imp
r
o
ve location of
error messag
e
s in instan
t
iations
commit
|
commitdiff
|
tree
2022-10-06
Yannick Moy
ada: Do not issu
e
compiler war
n
ings in
G
NATp
r
ove mode
commit
|
commitdiff
|
tree
2022-09-12
Yannick Moy
[Ada] Justify
fals
e
alarm
from CodePeer
a
na
l
ysis
o
f
.
.
.
commit
|
commitdiff
|
tree
2022-09-12
Yannick M
o
y
[Ada] Accept explici
t
SPARK_Mode Auto as confi
g
ur
a
tion
.
.
.
commit
|
commitdiff
|
tree
2022-09-12
Yann
i
ck
Mo
y
[Ada] R
e
ject use
in SPARK
o
f Asm int
r
insics for
code
.
.
.
commit
|
commitdiff
|
tree
2022-09-02
Yannick Moy
[Ada] Recove
r
proof of
S
ca
l
ed_
D
i
vide in
S
y
s
tem
.
Arith_64
commit
|
commitdiff
|
tree
2022-07-13
Yannic
k
Moy
[Ada] Fix incorrec
t
ha
n
dling of Ghost aspect
commit
|
commitdiff
|
tree
2022-07-13
Yannick Moy
[A
d
a] Fix
p
r
o
of o
f
runtime unit System
.
Arit
h
_64
commit
|
commitdiff
|
tree
2022-07-13
Yan
n
ick Moy
[
Ada] Fix automat
i
c
proof on System
.
Arith_32
commit
|
commitdiff
|
tree
2022-07-12
Yannick Mo
y
[A
d
a
]
Ignore sw
i
tches
f
o
r controlling f
r
o
nte
n
d wa
r
n
i
n
g
s
.
.
.
commit
|
commitdiff
|
tree
2022-07-06
Yannick Moy
[Ada] Def
e
rred constant considered as
not preel
a
borable
commit
|
commitdiff
|
tree
2022-07-06
Yannick Moy
[Ada] Support ghost generic formal parameters
commit
|
commitdiff
|
tree
2022-07-05
Ya
n
nick M
o
y
[Ada]
Fix spurious erro
r
on object renami
n
g
with gh
o
st
.
.
.
commit
|
commitdiff
|
tree
2022-07-05
Yannick Moy
[Ad
a
]
S
purio
u
s error on q
u
a
l
ified pre
f
i
x
in Pack
.
Func
.
.
.
commit
|
commitdiff
|
tree
2022-06-02
Yannick Mo
y
[Ada] Fix spurio
u
s
e
rro
r
s
on ghost c
o
de in
g
enerics
commit
|
commitdiff
|
tree
2022-06-02
Yanni
c
k Moy
[Ada] Issue errors on wro
n
g context f
o
r g
h
ost entitie
s
commit
|
commitdiff
|
tree
2022-06-02
Yannick Moy
[Ada]
Rem
o
va
l
of dead code Anal
y
ze
_
Label_Entity
commit
|
commitdiff
|
tree
2022-06-01
Yanni
c
k
Mo
y
[
A
d
a] Allow confirming volatile propertie
s
on No_C
a
ching
.
.
.
commit
|
commitdiff
|
tree
2022-06-01
Yannick Moy
[Ada
]
Fix c
l
a
s
si
f
ication of Subpro
g
ram_Variant as ass
e
r
t
ion
.
.
.
commit
|
commitdiff
|
tree
2022-06-01
Y
a
nnick Moy
[Ada] Iss
u
e a
w
a
rni
n
g on en
t
ity h
i
dden in
use_clause
.
.
.
commit
|
commitdiff
|
tree
2022-06-01
Yannick Moy
[Ada]
I
s
su
e
b
etter error messa
g
e
fo
r
out-
o
f-ord
e
r
keywords
.
.
.
commit
|
commitdiff
|
tree
2022-05-30
Yannick Moy
[Ada]
U
pdate proo
f
s of double
a
r
ithm
e
tic un
i
t
after
.
.
.
commit
|
commitdiff
|
tree
2022-05-30
Yann
i
ck
M
o
y
[Ada] Adapt proof of runtime u
n
it s-arit3
2
commit
|
commitdiff
|
tree
2022-05-30
Y
a
nnick Moy
[Ada
]
PR ad
a
/
105303 Fix use of Assertion
_
Polic
y
in
.
.
.
commit
|
commitdiff
|
tree
2022-05-19
Yannick
M
o
y
[
Ada
]
Fur
t
her ada
p
t proof of
d
oub
l
e arithmetic
r
u
n
tim
e
.
.
.
commit
|
commitdiff
|
tree
2022-05-18
Y
a
n
nick Mo
y
[Ada]
Ada
p
t
proof
of dou
b
le
a
rithmetic
r
untime u
n
i
t
commit
|
commitdiff
|
tree
2022-05-18
Y
annick Moy
[
Ada] F
i
x proof of runtime units
commit
|
commitdiff
|
tree
2022-05-18
Ya
n
n
i
ck M
o
y
[Ada
]
Sp
u
rious
error on freezi
n
g of tagged
t
ypes
i
n
.
.
.
commit
|
commitdiff
|
tree
2022-05-17
Yan
n
ick Moy
[Ada] Allow inlining for proof inside generics
commit
|
commitdiff
|
tree
2022-05-17
Yannick Mo
y
[
A
da]
F
ix inse
r
tion of declarat
i
on inside quantified
.
.
.
commit
|
commitdiff
|
tree
2022-05-16
Y
a
nnic
k
Moy
[
Ada] Fix proof of double arithme
t
ic
u
n
its
commit
|
commitdiff
|
tree
2022-05-16
Yannic
k
Mo
y
[Ada] Update comment justifying non-inlining for proof
.
.
.
commit
|
commitdiff
|
tree
2022-05-13
Yannic
k
Moy
[Ada] Simplif
y
helper units for formal h
a
s
h
ed sets
.
.
.
commit
|
commitdiff
|
tree
2022-05-13
Yannick Moy
[Ada] Adapt body of f
o
r
mal
s
ets and maps for SPARK
commit
|
commitdiff
|
tree
2022-05-13
Yannick Moy
[A
d
a]
R
em
o
v
e
dependency on tampering checks
a
nd contro
l
l
e
d
.
.
.
commit
|
commitdiff
|
tree
2022-05-13
Yannick Moy
[Ada] Facilitate
proof of O
v
e
r
write in bounde
d
stri
n
g
s
.
.
.
commit
|
commitdiff
|
tree
2022-05-12
Yann
i
c
k Moy
[
Ada] R
e
move usel
e
ss pragma Warnings Off from runtime
.
.
.
commit
|
commitdiff
|
tree
2022-05-12
Y
a
nni
c
k Moy
[Ada] Do no
t
i
s
s
u
e a w
a
rning o
n
a postco
n
dition of
.
.
.
commit
|
commitdiff
|
tree
2022-05-12
Yannick Moy
[Ada
]
A
d
d ghost code
t
o facilitate p
r
oof with
SPAR
K
commit
|
commitdiff
|
tree
2022-05-12
Yanni
c
k Mo
y
[Ada] Remove use of use-clau
s
es
in lo
a
ded run
t
ime units
commit
|
commitdiff
|
tree
2022-05-12
Yannick Moy
[
Ada] Ada
p
t CodePeer
analy
s
is
o
f GNAT to
c
ha
n
ges in
.
.
.
commit
|
commitdiff
|
tree
2022-05-12
Yannick Moy
[Ada]
P
roo
f
of 'Ima
g
e sup
p
ort for signed integers
commit
|
commitdiff
|
tree
2022-05-11
Yannick Mo
y
[Ada] Pro
o
f of 'Ima
g
e
s
upport for unsign
e
d in
t
egers
commit
|
commitdiff
|
tree
2022-05-11
Yannick Moy
[Ada
]
A
d
apt
p
r
o
of of
S
ystem
.
Arith_Double after
upd
a
te
.
.
.
commit
|
commitdiff
|
tree
2022-05-10
Y
a
nnick Moy
[Ada]
Fix i
n
dentati
o
n
to fol
l
ow
u
niform
s
tyle across
.
.
.
commit
|
commitdiff
|
tree
2022-05-09
Yanni
c
k Moy
[Ad
a
]
Sug
g
est us
e
of First
_
Va
l
i
d
/Last_Val
i
d on type
.
.
.
commit
|
commitdiff
|
tree
2022-05-09
Y
annick Moy
[Ad
a
] S
e
t Error_Msg_Warn b
e
fore use of << inser
t
ion
commit
|
commitdiff
|
tree
2022-01-11
Yannic
k
M
o
y
[Ada]
Adapt proof of Sy
s
t
e
m
.
Ar
i
th_Double
commit
|
commitdiff
|
tree
2022-01-11
Yannick Moy
[
Ad
a
] Recover pro
o
f of
Ada
.
S
t
rings
.
Fixed with assertions
commit
|
commitdiff
|
tree
2022-01-11
Yannick Moy
[
Ad
a
]
Proo
f
of unit
System
.
Case
_
Util
commit
|
commitdiff
|
tree
2022-01-11
Yannick
Mo
y
[Ada]
Adapt ghost code
to
m
a
intain proof
commit
|
commitdiff
|
tree
2022-01-11
Y
a
n
nick M
o
y
[Ada] Proof of Sy
s
tem
.
Ve
c
tors
.
Boolean_Oper
a
tions
commit
|
commitdiff
|
tree
2022-01-06
Yannick Moy
[Ada] Proo
f
of Sys
t
e
m
.
Generic_Array_Operations at
s
ilver
.
.
.
commit
|
commitdiff
|
tree
2022-01-06
Yan
n
i
ck
M
o
y
[Ada] Justif
y
false pos
i
tiv
e
message fr
o
m CodePeer
.
.
.
commit
|
commitdiff
|
tree
2022-01-06
Yannick Moy
[
A
d
a
] Proof
of
ru
n
t
i
me unit for no
n
-binar
y
m
o
dular
.
.
.
commit
|
commitdiff
|
tree
2022-01-06
Y
a
n
n
ic
k
Moy
[Ada]
P
roof of runtime u
n
its for bi
n
ary modu
l
a
r
exponen
t
ia
t
i
o
n
commit
|
commitdiff
|
tree
2022-01-05
Yanni
c
k Moy
[Ada] Add contracts for
the proof of System
.
Arit
h
_128
commit
|
commitdiff
|
tree
2022-01-05
Yannic
k
Mo
y
[
A
da] P
r
oo
f
of runtime units for i
n
teg
e
r expon
e
nti
a
tion
.
.
.
commit
|
commitdiff
|
tree
2022-01-05
Yannick Moy
[A
d
a] P
r
oof
of runtime uni
t
s for
i
n
t
eg
e
r exponentia
t
io
n
.
.
.
commit
|
commitdiff
|
tree
2022-01-05
Yannick
Moy
[A
d
a] Ren
a
me par
a
meter-dependent constants in gener
i
c
.
.
.
commit
|
commitdiff
|
tree
2022-01-05
Yannick M
o
y
[Ada] F
i
x l
e
mma in generi
c
u
n
it System
.
A
rit
h
_Double
commit
|
commitdiff
|
tree
2021-12-02
Yannick Moy
[Ada]
Proof of System
.
Arith_32 for doub
l
e ari
t
hmetic
.
.
.
commit
|
commitdiff
|
tree
2021-12-02
Yannick Moy
[Ada] Am
e
n
d
proof of Syst
e
m
.
Arith_Double
t
o remo
v
e
.
.
.
commit
|
commitdiff
|
tree
2021-12-02
Yan
n
ick
Moy
[Ada] Add pragma Annotate
fo
r
Cod
e
Pe
e
r anal
y
sis
commit
|
commitdiff
|
tree
2021-12-02
Yann
i
c
k
Moy
[Ada
]
Proof of supp
o
rt
u
nits for 'Width o
n
signed int
e
ge
r
s
commit
|
commitdiff
|
tree
2021-12-02
Y
annick Moy
[Ada
]
Proof o
f
I
n
te
r
faces
.
C with SPARK
commit
|
commitdiff
|
tree
2021-12-02
Yannick
Moy
[Ada] Pr
o
o
f of System
.
Val_Uti
l
u
t
il
i
ties for
'Value
.
.
.
commit
|
commitdiff
|
tree
2021-12-02
Yanni
c
k Moy
[Ada] Proof
o
f
B
o
ol
e
an
'
Image and Boolean'Value
commit
|
commitdiff
|
tree
2021-12-01
Yannick Moy
[Ada] Impr
o
ve erro
r
me
s
sages for
dot n
o
tation
when
.
.
.
commit
|
commitdiff
|
tree
2021-12-01
Yannic
k
Moy
[Ada]
Add
q
uery
for
e
x
tended p
r
ecis
i
o
n
flo
a
ting-point
.
.
.
commit
|
commitdiff
|
tree
2021-12-01
Yannick Moy
[Ada] Impr
o
ve messages on in
c
orre
c
t state refinem
e
nt
.
.
.
commit
|
commitdiff
|
tree
2021-11-10
Yannick
Moy
[Ada] Creat
e
explicit ghost mi
r
r
o
r unit
f
or big integers
commit
|
commitdiff
|
tree
2021-11-10
Yannick
M
o
y
[Ada]
B
et
t
er error message
on m
i
ssing parentheses
commit
|
commitdiff
|
tree
2021-11-09
Yan
n
ick Moy
[Ada] Co
m
p
l
e
te suppor
t
f
or prefixed call o
n
s
u
b
t
ypes
.
.
.
commit
|
commitdiff
|
tree
2021-11-09
Y
a
nnick M
o
y
[Ada] Fix support for prefixed call wit
h
in
c
omplete
.
.
.
commit
|
commitdiff
|
tree
2021-10-25
Yannick Moy
[Ada] Iss
u
e error o
n
in
v
a
l
id use
o
f G
h
ost in
s
i
d
e
pragma
.
.
.
commit
|
commitdiff
|
tree
2021-10-20
Yannick Moy
[
Ada] Proof of the runtime support for
attribute 'Width
commit
|
commitdiff
|
tree
2021-10-20
Yan
n
ick Moy
[Ada] Pr
o
vide dummy body for
big inte
g
ers libra
r
y used
.
.
.
commit
|
commitdiff
|
tree
2021-10-20
Yannick
M
oy
[Ada] Issue
warning
o
n unused quantified
expression
commit
|
commitdiff
|
tree
2021-10-05
Yanni
c
k Moy
[Ada
]
Improve error message on array aggrega
t
es
commit
|
commitdiff
|
tree
next