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 small fallout of previous change
2023-05-29
Yannick Moy
a
d
a: Restore SPARK_Mode On for numerical functions
commit
|
commitdiff
|
tree
2023-05-26
Ya
n
nick Moy
ad
a
: Def
a
ult ini
t
ial
i
ze
entity to
avoid CodePeer message
commit
|
commitdiff
|
tree
2023-05-26
Y
annick Moy
a
d
a: Minor do
c
clarificati
o
n
commit
|
commitdiff
|
tree
2023-05-26
Yanni
c
k
M
oy
ada: Complete contracts of SPARK units
commit
|
commitdiff
|
tree
2023-05-23
Yannick
M
oy
ada: Ad
d
default value at
i
nitializat
i
on f
o
r CodeP
e
er
commit
|
commitdiff
|
tree
2023-05-23
Yannick Moy
ada:
Facilitat
e
p
r
o
o
f of
I
n
terfa
c
es
.
C
.
To_Ada
commit
|
commitdiff
|
tree
2023-05-16
Yannick Moy
ada: U
p
da
t
e pr
o
of of ru
n
time
u
nit
s
commit
|
commitdiff
|
tree
2023-05-16
Yannick
M
oy
ada: Simplif
y
dra
m
atic
a
ll
y
ghost
c
ode f
o
r pr
o
o
f of
.
.
.
commit
|
commitdiff
|
tree
2023-05-16
Y
annick Moy
ada:
A
dd int
e
rm
e
diate asserti
o
n
s
for
p
ro
o
f of
S
uper_Tail
commit
|
commitdiff
|
tree
2023-05-16
Yannick Moy
ada
:
Set Loop_Variant assertion
p
olicy to
Ignore in
.
.
.
commit
|
commitdiff
|
tree
2023-05-16
Yannick Moy
ad
a
: Restore proof of Syste
m
.
Arith_Doubl
e
commit
|
commitdiff
|
tree
2023-05-15
Yannick Moy
ada
:
Ad
d
a
n
n
otati
o
ns for pr
o
o
f
o
f
te
r
mination of runtime
.
.
.
commit
|
commitdiff
|
tree
2023-05-15
Yannick Mo
y
ada: Recov
e
r proof of r
u
ntime
u
nits
commit
|
commitdiff
|
tree
2023-05-15
Yanni
c
k
Moy
ad
a
: Reco
v
e
r pr
o
of of Int
e
r
fa
c
es
.
C for term
i
nation
commit
|
commitdiff
|
tree
2023-05-15
Yannick Moy
ada: Update comm
e
nt aft
e
r SPA
R
K RM change
commit
|
commitdiff
|
tree
2023-05-15
Y
a
n
nick Moy
ada:
F
ix han
d
ling of p
r
ag
m
a W
a
rnings (Toolna
m
e, Off/On)
commit
|
commitdiff
|
tree
2023-05-15
Ya
n
n
i
ck Moy
ad
a
:
A
llow pragma
s
Annotat
e
betwe
e
n loo
p
pragmas
commit
|
commitdiff
|
tree
2022-12-06
Yannick
M
oy
ada:
Allow
No_Caching on volatile types
commit
|
commitdiff
|
tree
2022-11-28
Y
a
nnick Moy
ad
a
: Im
p
leme
n
t cha
n
ge to S
P
ARK RM rule on
state ref
i
nement
commit
|
commitdiff
|
tree
2022-11-14
Yannick
Moy
a
d
a: F
i
x e
r
ror on
S
PARK_Mode on librar
y
-lev
e
l se
p
arate
.
.
.
commit
|
commitdiff
|
tree
2022-11-14
Yannick Moy
a
d
a:
I
mprove l
o
cation
o
f erro
r
messag
e
s
in
i
n
s
tantiati
o
n
s
commit
|
commitdiff
|
tree
2022-10-06
Yannick Moy
ada:
Do not iss
u
e compiler w
a
rni
n
g
s in GNATprov
e
mode
commit
|
commitdiff
|
tree
2022-09-12
Yannick Moy
[
A
da] J
u
stify false alarm
f
rom CodePe
e
r
analysis of
.
.
.
commit
|
commitdiff
|
tree
2022-09-12
Yannick M
o
y
[Ada] Accept explicit SPARK_Mo
d
e
Aut
o
as conf
i
guration
.
.
.
commit
|
commitdiff
|
tree
2022-09-12
Yannick Mo
y
[Ada] Reject use in
SPARK
o
f
A
sm intrinsics
for code
.
.
.
commit
|
commitdiff
|
tree
2022-09-02
Yannick Moy
[
A
da] Recover proof o
f
Scaled_Divide in Sys
t
em
.
Arith_64
commit
|
commitdiff
|
tree
2022-07-13
Yann
i
ck M
o
y
[Ada]
F
i
x
i
ncorr
e
ct handling o
f
Ghost aspect
commit
|
commitdiff
|
tree
2022-07-13
Y
an
n
ick Moy
[Ad
a
]
F
ix proof
o
f
runtime
u
n
i
t
S
ystem
.
Arith
_
6
4
commit
|
commitdiff
|
tree
2022-07-13
Yannick Moy
[Ada
]
Fix autom
a
tic proof o
n
System
.
A
r
it
h
_32
commit
|
commitdiff
|
tree
2022-07-12
Yannick M
o
y
[Ada] Ignore swi
t
c
h
e
s
for c
o
n
t
ro
l
l
i
n
g frontend warnings
.
.
.
commit
|
commitdiff
|
tree
2022-07-06
Yann
i
c
k Moy
[Ada] De
f
erred constant c
o
nsidered as not preela
b
orabl
e
commit
|
commitdiff
|
tree
2022-07-06
Yannick Moy
[
Ad
a
] Support ghost
gener
i
c for
m
al p
a
ra
m
ete
r
s
commit
|
commitdiff
|
tree
2022-07-05
Y
annick Moy
[Ada
]
Fix spurious erro
r
on object renaming with ghost
.
.
.
commit
|
commitdiff
|
tree
2022-07-05
Yann
i
ck Moy
[Ada] Spuri
o
us
erro
r
on qu
a
lifie
d
prefix
i
n Pack
.
Func
.
.
.
commit
|
commitdiff
|
tree
2022-06-02
Yannick Moy
[
Ada]
F
ix
s
purious errors
on g
h
ost code i
n
generics
commit
|
commitdiff
|
tree
2022-06-02
Yannick Moy
[Ada] Issue err
o
rs on
wrong
c
ontext for ghos
t
entities
commit
|
commitdiff
|
tree
2022-06-02
Yannick Mo
y
[
A
d
a]
Re
m
oval of dea
d
code Anal
y
ze_
L
abel_Ent
i
ty
commit
|
commitdiff
|
tree
2022-06-01
Y
a
nnick Mo
y
[Ada] Allow conf
i
rming
v
olatile properties on
N
o
_
Cach
i
n
g
.
.
.
commit
|
commitdiff
|
tree
2022-06-01
Yanni
c
k Moy
[Ada] Fix classificat
i
on of Subprogram_V
a
riant as assertion
.
.
.
commit
|
commitdiff
|
tree
2022-06-01
Yannick Moy
[Ada] Issue a warning
o
n entity h
i
dd
e
n in use_
c
la
u
se
.
.
.
commit
|
commitdiff
|
tree
2022-06-01
Ya
n
nick Moy
[Ada] Issue better error
messa
g
e for
out-of-order k
e
yword
s
.
.
.
commit
|
commitdiff
|
tree
2022-05-30
Ya
n
nic
k
Moy
[Ada] Update pr
o
ofs of d
o
uble arithmetic unit after
.
.
.
commit
|
commitdiff
|
tree
2022-05-30
Yan
n
ick
Moy
[Ada] Adapt proof of runtime unit s
-
arit3
2
commit
|
commitdiff
|
tree
2022-05-30
Yan
n
ick Moy
[Ada] PR a
d
a
/
1
05303 Fi
x
u
se of Asser
t
ion_Policy in
.
.
.
commit
|
commitdiff
|
tree
2022-05-19
Y
anni
c
k Moy
[Ada]
F
u
r
ther adapt pr
o
of of
double arithmetic runtime
.
.
.
commit
|
commitdiff
|
tree
2022-05-18
Y
a
nnick Moy
[Ada] Adapt proof of
d
ouble arith
m
e
tic runtime unit
commit
|
commitdiff
|
tree
2022-05-18
Yannick Moy
[Ada] Fix proof
of runtime units
commit
|
commitdiff
|
tree
2022-05-18
Yan
n
ick Moy
[Ada
]
Sp
u
r
iou
s
error on freez
i
n
g
of tagged ty
p
es
i
n
.
.
.
commit
|
commitdiff
|
tree
2022-05-17
Yannic
k
Moy
[A
d
a] Allo
w
inlining for proof inside g
e
neric
s
commit
|
commitdiff
|
tree
2022-05-17
Y
annick
M
oy
[Ada] Fix insertion of declarat
i
on insid
e
qu
a
ntified
.
.
.
commit
|
commitdiff
|
tree
2022-05-16
Y
annick M
o
y
[Ada]
Fi
x
proo
f
of doub
l
e arithmetic units
commit
|
commitdiff
|
tree
2022-05-16
Ya
n
nick Moy
[Ada] Up
d
a
te comment justi
f
yin
g
non-inlinin
g
for proof
.
.
.
commit
|
commitdiff
|
tree
2022-05-13
Yannick Moy
[
A
d
a
] S
i
m
p
lify helper unit
s
for formal
hashed
s
ets
.
.
.
commit
|
commitdiff
|
tree
2022-05-13
Yanni
c
k Moy
[Ad
a
] A
d
apt body o
f
f
o
rmal sets and m
a
ps for
SPARK
commit
|
commitdiff
|
tree
2022-05-13
Y
a
nnick Moy
[Ada] Remove dependency on tamperin
g
che
c
ks and controlled
.
.
.
commit
|
commitdiff
|
tree
2022-05-13
Yannick Moy
[Ada] Fac
i
l
i
tate proof
of Ov
e
rw
r
ite
i
n
bounded str
i
ngs
.
.
.
commit
|
commitdiff
|
tree
2022-05-12
Yannick
M
oy
[Ada] Remove useless pragma
W
ar
n
ings Off from runtime
.
.
.
commit
|
commitdiff
|
tree
2022-05-12
Y
a
nnick Moy
[Ada] D
o
not
issue a
warning
on a pos
t
condition of
.
.
.
commit
|
commitdiff
|
tree
2022-05-12
Yan
n
ick Moy
[Ada] Add g
h
ost code to fa
c
ilit
a
te p
r
oo
f
wi
t
h SPARK
commit
|
commitdiff
|
tree
2022-05-12
Yannick Moy
[
Ada] Remove use of use-clauses in loaded
runt
i
m
e
u
ni
t
s
commit
|
commitdiff
|
tree
2022-05-12
Y
a
nnick Moy
[Ada] Ad
a
pt Co
d
e
P
e
e
r analysis of GNAT to changes in
.
.
.
commit
|
commitdiff
|
tree
2022-05-12
Yannick Moy
[Ada] Pr
o
of of
'
I
mage support for sig
n
ed inte
g
ers
commit
|
commitdiff
|
tree
2022-05-11
Y
a
nnick Moy
[Ada] Proof of 'Imag
e
s
upport
f
o
r unsigned int
e
gers
commit
|
commitdiff
|
tree
2022-05-11
Y
annick Moy
[
A
da] Adapt p
r
o
o
f o
f
Sy
s
tem
.
Arith_Doub
l
e after update
.
.
.
commit
|
commitdiff
|
tree
2022-05-10
Yann
i
ck
Mo
y
[Ada] Fix inde
n
tation t
o
follow uniform style across
.
.
.
commit
|
commitdiff
|
tree
2022-05-09
Yannick
M
o
y
[A
d
a] S
u
ggest use
o
f First
_
Valid/Last_Valid
on
t
yp
e
.
.
.
commit
|
commitdiff
|
tree
2022-05-09
Yannick Moy
[Ada] S
e
t Error_M
s
g_Warn before us
e
of << i
n
sertion
commit
|
commitdiff
|
tree
2022-01-11
Y
annick Moy
[
A
da
]
A
d
apt
p
r
o
of of
S
ystem
.
Arith_
D
ouble
commit
|
commitdiff
|
tree
2022-01-11
Yannick Moy
[A
d
a
]
Recover pro
o
f of
Ada
.
Stri
n
g
s
.
Fixed
w
i
th assertion
s
commit
|
commitdiff
|
tree
2022-01-11
Yann
i
ck
Moy
[Ada] Pro
o
f
of unit
S
ystem
.
Case_Util
commit
|
commitdiff
|
tree
2022-01-11
Yan
n
ick Moy
[Ada] Adapt gh
o
s
t
code to
m
ai
n
tain pro
o
f
commit
|
commitdiff
|
tree
2022-01-11
Yannick Moy
[Ada] Pro
o
f
of
S
ystem
.
Vectors
.
Boole
a
n_Operat
i
ons
commit
|
commitdiff
|
tree
2022-01-06
Yannick Moy
[Ada] P
r
oof of Syst
e
m
.
Generic_
A
r
r
ay_Oper
a
ti
o
n
s
a
t
s
ilver
.
.
.
commit
|
commitdiff
|
tree
2022-01-06
Yannic
k
M
o
y
[Ada
]
Ju
s
tify false
p
o
s
itive messa
g
e fr
o
m Co
d
ePeer
.
.
.
commit
|
commitdiff
|
tree
2022-01-06
Y
a
n
nick Moy
[Ada] Proof of
ru
n
time unit for non-binary
modu
l
ar
.
.
.
commit
|
commitdiff
|
tree
2022-01-06
Yannick Moy
[Ada] Proof of runt
i
me uni
t
s for
binary modular exponent
i
ation
commit
|
commitdiff
|
tree
2022-01-05
Yanni
c
k Moy
[Ada
]
Add
c
o
n
t
r
acts for the p
r
o
o
f
o
f
Syste
m
.
Arith_128
commit
|
commitdiff
|
tree
2022-01-05
Y
a
nnick Moy
[Ada] Pr
o
o
f of
r
unt
i
me
u
nits for
i
n
teger
e
xpone
n
tiation
.
.
.
commit
|
commitdiff
|
tree
2022-01-05
Yannick Moy
[Ada] Proof of r
u
n
time units for
integer expone
n
tiation
.
.
.
commit
|
commitdiff
|
tree
2022-01-05
Yanni
c
k Moy
[Ada
]
Re
n
ame param
e
ter-
d
ependent constants in
generic
.
.
.
commit
|
commitdiff
|
tree
2022-01-05
Yannick Moy
[A
d
a] Fix lemma in generi
c
unit Syst
e
m
.
Ari
t
h_D
o
uble
commit
|
commitdiff
|
tree
2021-12-02
Yannick Moy
[
Ada] Proof
of System
.
Arit
h
_32 for double arithmetic
.
.
.
commit
|
commitdiff
|
tree
2021-12-02
Y
a
nnick Moy
[Ada] Am
e
nd pro
o
f of
S
ystem
.
Ar
i
th_
D
o
u
b
le to r
e
move
.
.
.
commit
|
commitdiff
|
tree
2021-12-02
Yanni
c
k
Moy
[Ada] Add
p
ragma A
n
notate for CodePeer analy
s
is
commit
|
commitdiff
|
tree
2021-12-02
Yannick Moy
[Ada] Proof
o
f support units for 'Wi
d
th on signed integers
commit
|
commitdiff
|
tree
2021-12-02
Yannick M
o
y
[
A
da] Proo
f
of Inte
r
f
a
c
es
.
C
w
i
t
h SPARK
commit
|
commitdiff
|
tree
2021-12-02
Y
annick Moy
[
A
da]
Pr
o
of of System
.
Val_Util utilities for 'Value
.
.
.
commit
|
commitdiff
|
tree
2021-12-02
Yannick Moy
[Ada] Proof of Boo
l
ea
n
'
Ima
g
e
and Boolean'Value
commit
|
commitdiff
|
tree
2021-12-01
Yan
n
ick
Moy
[Ada] I
m
pr
o
ve err
o
r m
e
ssa
g
es for dot notation when
.
.
.
commit
|
commitdiff
|
tree
2021-12-01
Y
a
nnick Moy
[Ada] Add
q
uery
f
or
e
xtended precisi
o
n flo
a
ting-point
.
.
.
commit
|
commitdiff
|
tree
2021-12-01
Yannick Mo
y
[Ada]
I
m
prove messages on incorrect state refinement
.
.
.
commit
|
commitdiff
|
tree
2021-11-10
Yannick Moy
[Ad
a
] Cr
e
a
t
e exp
l
icit ghost mirror u
n
it for b
i
g
integers
commit
|
commitdiff
|
tree
2021-11-10
Yann
i
ck Moy
[Ada] B
e
tter error mes
s
age
o
n
missing parentheses
commit
|
commitdiff
|
tree
2021-11-09
Y
annick
M
oy
[Ada]
C
om
p
lete support for prefixed call on
subtype
s
.
.
.
commit
|
commitdiff
|
tree
2021-11-09
Yannic
k
M
o
y
[Ada] Fix support for prefixed c
a
ll with incom
p
l
e
t
e
.
.
.
commit
|
commitdiff
|
tree
2021-10-25
Yann
i
ck Moy
[A
d
a] Issue er
r
or on inval
i
d use of Ghos
t
inside
pragma
.
.
.
commit
|
commitdiff
|
tree
2021-10-20
Yan
n
ick Moy
[Ada
]
Proof of the runti
m
e
support for a
t
tribute 'Width
commit
|
commitdiff
|
tree
2021-10-20
Yanni
c
k
M
oy
[Ada] Provide dumm
y
bo
d
y for big i
n
tegers library used
.
.
.
commit
|
commitdiff
|
tree
2021-10-20
Y
a
nnick Moy
[Ada] I
s
sue warn
i
n
g
on unused quan
t
ified e
x
pr
e
ssion
commit
|
commitdiff
|
tree
2021-10-05
Yannick Moy
[
Ada] I
m
p
ro
v
e error message
o
n
array aggregates
commit
|
commitdiff
|
tree
next