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: Use ghost predicate in standard library
2023-06-13
Yannick
M
o
y
ada:
U
se gh
o
st
pred
i
cate in
s
tan
d
ard l
i
brar
y
commit
|
commitdiff
|
tree
2023-06-13
Yannick Moy
ada:
S
uppor
t
n
e
w GNA
T
-sp
e
c
i
fic a
s
pect Ghost_
P
r
e
dicate
commit
|
commitdiff
|
tree
2023-05-29
Yannick Moy
ada: Restore SPARK_
M
ode On for nu
m
e
rical functions
commit
|
commitdiff
|
tree
2023-05-26
Yannick Moy
ad
a
: Defa
u
lt in
i
tialize entity
t
o avoid Co
d
ePee
r
m
e
ssa
g
e
commit
|
commitdiff
|
tree
2023-05-26
Yannick
M
o
y
ada
:
Minor
d
oc c
l
ar
i
ficati
o
n
commit
|
commitdiff
|
tree
2023-05-26
Y
a
nnick Moy
a
d
a
:
Complet
e
c
o
ntr
a
c
t
s of SPARK units
commit
|
commitdiff
|
tree
2023-05-23
Y
annick Moy
ada: Add default value at
i
nitialization for CodePeer
commit
|
commitdiff
|
tree
2023-05-23
Yannick Moy
ada: Fa
c
ili
t
at
e
proo
f
of I
n
terface
s
.
C
.
To_Ada
commit
|
commitdiff
|
tree
2023-05-16
Yan
n
ick Mo
y
a
d
a
: Update p
r
oof of runt
i
me units
commit
|
commitdiff
|
tree
2023-05-16
Yann
i
ck M
o
y
ada
:
Simpli
f
y dr
a
matically ghost code for proof of
.
.
.
commit
|
commitdiff
|
tree
2023-05-16
Yannick Moy
a
d
a: A
d
d interme
d
iate asse
r
tio
n
s
for proof of
S
uper_Tail
commit
|
commitdiff
|
tree
2023-05-16
Yannick Mo
y
ada:
S
et Loop_Variant assertio
n
policy to Ignore in
.
.
.
commit
|
commitdiff
|
tree
2023-05-16
Yannic
k
Moy
ada
:
Restore proof o
f
System
.
Arith_Double
commit
|
commitdiff
|
tree
2023-05-15
Yannick Moy
ada:
Add
annotations for proof of terminatio
n
of ru
n
ti
m
e
.
.
.
commit
|
commitdiff
|
tree
2023-05-15
Yann
i
ck Moy
ada:
Recover
proof
of runtime units
commit
|
commitdiff
|
tree
2023-05-15
Yannick Moy
ada: Recover proo
f
o
f
Interfaces
.
C
for
t
erminat
i
on
commit
|
commitdiff
|
tree
2023-05-15
Yan
n
ick Moy
ada: Update com
m
e
n
t
a
f
te
r
SPA
R
K
R
M change
commit
|
commitdiff
|
tree
2023-05-15
Y
a
nnick Moy
ada
:
Fix
h
andling of prag
m
a
W
arnin
g
s (
T
oolname, Off/On)
commit
|
commitdiff
|
tree
2023-05-15
Y
a
nni
c
k
M
oy
ada:
All
o
w pragmas
A
nno
t
ate between
l
oop prag
m
as
commit
|
commitdiff
|
tree
2022-12-06
Yannick Moy
ada: Allo
w
No_Caching
on volatile types
commit
|
commitdiff
|
tree
2022-11-28
Yan
n
ic
k
Moy
ada: Implement change to S
P
ARK
R
M rul
e
on state refinement
commit
|
commitdiff
|
tree
2022-11-14
Y
a
nnick Moy
ad
a
: Fix error
o
n SPARK_Mod
e
on lib
r
ary-l
e
vel se
p
ara
t
e
.
.
.
commit
|
commitdiff
|
tree
2022-11-14
Y
annick
Moy
a
da:
Impr
o
v
e
locat
i
on of
e
rr
o
r message
s
in ins
t
antiations
commit
|
commitdiff
|
tree
2022-10-06
Yannick Moy
a
d
a: Do not
issue compiler warnings in GNATprov
e
mode
commit
|
commitdiff
|
tree
2022-09-12
Y
a
n
nick Moy
[Ada]
Jus
t
ify f
a
lse
a
l
a
r
m fro
m
Co
d
e
P
eer
a
n
alysis of
.
.
.
commit
|
commitdiff
|
tree
2022-09-12
Y
an
n
ick M
o
y
[Ada] Ac
c
ep
t
exp
l
icit SPARK_Mode Aut
o
as conf
i
guration
.
.
.
commit
|
commitdiff
|
tree
2022-09-12
Yannic
k
Moy
[Ada] R
e
j
e
ct
use
i
n SPARK of As
m
intrin
s
ics for code
.
.
.
commit
|
commitdiff
|
tree
2022-09-02
Yannick Moy
[A
d
a] R
e
cover
p
ro
o
f
of Scaled_Divide in
System
.
Arith_64
commit
|
commitdiff
|
tree
2022-07-13
Y
a
nnick M
o
y
[Ada] Fi
x
i
n
corre
c
t
handling o
f
Ghost
a
sp
e
ct
commit
|
commitdiff
|
tree
2022-07-13
Y
a
n
n
ick Moy
[Ada] Fix
p
r
oof of
r
unti
m
e unit
S
ystem
.
Arith_64
commit
|
commitdiff
|
tree
2022-07-13
Yannick Moy
[Ad
a
]
Fix auto
m
atic pr
o
of on System
.
Arith_32
commit
|
commitdiff
|
tree
2022-07-12
Ya
n
n
ick Moy
[Ada] Ignore s
w
itches for contr
o
lling frontend wa
r
ning
s
.
.
.
commit
|
commitdiff
|
tree
2022-07-06
Yannick
Moy
[Ada
]
Deferred
c
onsta
n
t cons
i
dered as n
o
t
preel
a
bor
a
bl
e
commit
|
commitdiff
|
tree
2022-07-06
Yann
i
ck Moy
[Ada] S
u
p
port ghost generi
c
formal parameters
commit
|
commitdiff
|
tree
2022-07-05
Y
a
nnick
Moy
[Ada] Fix spurious error
o
n object renaming with ghost
.
.
.
commit
|
commitdiff
|
tree
2022-07-05
Yanni
c
k Mo
y
[Ada]
S
purious error o
n
qualified prefix in Pa
c
k
.
F
unc
.
.
.
commit
|
commitdiff
|
tree
2022-06-02
Yannick Mo
y
[Ada]
Fix
s
purious er
r
ors on ghost code
in gener
i
cs
commit
|
commitdiff
|
tree
2022-06-02
Yannick Moy
[Ada] Issue errors on wrong context fo
r
ghost e
n
titie
s
commit
|
commitdiff
|
tree
2022-06-02
Yannick M
o
y
[Ada]
R
emoval of de
a
d
code Analyz
e
_Lab
e
l_En
t
ity
commit
|
commitdiff
|
tree
2022-06-01
Yannick Moy
[Ada
]
Allow c
o
nfirming vo
l
atile proper
t
ies on No_Caching
.
.
.
commit
|
commitdiff
|
tree
2022-06-01
Y
a
nnick
M
oy
[Ada] F
i
x class
i
fication of Subprogr
a
m_Va
r
iant as asse
r
tion
.
.
.
commit
|
commitdiff
|
tree
2022-06-01
Y
anni
c
k Moy
[Ada] Issue
a w
a
rning on entity hi
d
d
en in use_c
l
au
s
e
.
.
.
commit
|
commitdiff
|
tree
2022-06-01
Yann
i
c
k
Moy
[A
d
a] Issu
e
b
etter error m
e
ssage
for out-of-order keywo
r
d
s
.
.
.
commit
|
commitdiff
|
tree
2022-05-30
Yannick Moy
[Ad
a
] Upd
a
t
e proofs of double arithmet
i
c unit
after
.
.
.
commit
|
commitdiff
|
tree
2022-05-30
Yannick Moy
[A
d
a] Adapt pro
o
f of run
t
ime
unit
s
-
arit32
commit
|
commitdiff
|
tree
2022-05-30
Yanni
c
k
Moy
[
Ada]
P
R
a
da/105303 F
i
x
use o
f
Assertion_Policy in
.
.
.
commit
|
commitdiff
|
tree
2022-05-19
Yannick Moy
[Ada] F
u
rt
h
er adapt proof o
f
d
ouble arith
m
etic
r
u
ntime
.
.
.
commit
|
commitdiff
|
tree
2022-05-18
Yannick Moy
[Ada] Adapt proof of
double arithmetic run
t
i
m
e unit
commit
|
commitdiff
|
tree
2022-05-18
Yannick Mo
y
[A
d
a
] Fix
proof
of ru
n
time uni
t
s
commit
|
commitdiff
|
tree
2022-05-18
Y
a
nnick Moy
[Ada] Sp
u
rious error
o
n freez
i
ng of tagged
ty
p
es
in
.
.
.
commit
|
commitdiff
|
tree
2022-05-17
Yannick Moy
[
Ad
a
] Allow
inlining for pr
o
of in
s
ide
generics
commit
|
commitdiff
|
tree
2022-05-17
Yannick
M
oy
[Ada
]
Fix inserti
o
n of declaration
i
nsid
e
quantified
.
.
.
commit
|
commitdiff
|
tree
2022-05-16
Yan
n
ick Moy
[Ada] Fix proof of
double ar
i
t
h
me
t
ic units
commit
|
commitdiff
|
tree
2022-05-16
Ya
n
nick Mo
y
[
Ad
a
]
Updat
e
comm
e
nt justifying non-inlin
i
ng for proo
f
.
.
.
commit
|
commitdiff
|
tree
2022-05-13
Yann
i
c
k M
o
y
[Ada] Si
m
plif
y
helper u
n
its for forma
l
hashed
sets
.
.
.
commit
|
commitdiff
|
tree
2022-05-13
Yannick Moy
[Ada] Ad
a
pt body of
formal s
e
ts and maps for SPARK
commit
|
commitdiff
|
tree
2022-05-13
Yann
i
ck
M
oy
[Ada] Remo
v
e dependency on tamp
e
ring che
c
ks and controlled
.
.
.
commit
|
commitdiff
|
tree
2022-05-13
Yan
n
ick
Moy
[
A
da] Faci
l
itate proof
o
f Overwrite
i
n bounded strin
g
s
.
.
.
commit
|
commitdiff
|
tree
2022-05-12
Ya
n
n
i
ck Mo
y
[Ada] Rem
o
ve usel
e
ss
p
ra
g
ma
W
a
r
nings Off f
r
om runt
i
me
.
.
.
commit
|
commitdiff
|
tree
2022-05-12
Y
annick Moy
[Ada] Do not i
s
s
u
e
a warning on a pos
t
con
d
ition of
.
.
.
commit
|
commitdiff
|
tree
2022-05-12
Ya
n
ni
c
k Moy
[Ada] Add ghost code t
o
facilitate proof with SPAR
K
commit
|
commitdiff
|
tree
2022-05-12
Yannick M
o
y
[Ada]
Rem
o
ve use of us
e
-clauses in l
o
aded runtime
u
n
i
ts
commit
|
commitdiff
|
tree
2022-05-12
Yann
i
ck Moy
[A
d
a]
Adapt C
o
dePeer a
n
alysi
s
of GNAT to changes in
.
.
.
commit
|
commitdiff
|
tree
2022-05-12
Yannick
Moy
[Ad
a
]
P
roof
of 'Image
s
u
p
p
o
rt
for signed i
n
teger
s
commit
|
commitdiff
|
tree
2022-05-11
Yannick Mo
y
[Ada] Proof of 'Image supp
o
rt for u
n
s
igned i
n
tegers
commit
|
commitdiff
|
tree
2022-05-11
Yannick Moy
[Ada] Adapt p
r
o
o
f
o
f Syst
e
m
.
Arith_Doubl
e
after update
.
.
.
commit
|
commitdiff
|
tree
2022-05-10
Yan
n
ick Moy
[Ada] Fix indentatio
n
t
o
follow uniform style across
.
.
.
commit
|
commitdiff
|
tree
2022-05-09
Yannic
k
Moy
[Ada] Sug
g
es
t
use of
First_
V
alid/Last_Va
l
id on t
y
pe
.
.
.
commit
|
commitdiff
|
tree
2022-05-09
Yannick Moy
[Ada] Set Error_Msg_War
n
befor
e
use of << insertion
commit
|
commitdiff
|
tree
2022-01-11
Y
annic
k
Moy
[Ada] Adapt proof of Syste
m
.
Arith_D
o
u
ble
commit
|
commitdiff
|
tree
2022-01-11
Yannick Moy
[Ad
a
] Recov
e
r proof of Ada
.
S
trings
.
F
ixe
d
w
i
th ass
e
rtions
commit
|
commitdiff
|
tree
2022-01-11
Yanni
c
k Moy
[Ada] Proof of
u
nit Syste
m
.
Case
_
Util
commit
|
commitdiff
|
tree
2022-01-11
Yannick Mo
y
[Ad
a
]
Ada
p
t ghost
c
ode
t
o maintain proof
commit
|
commitdiff
|
tree
2022-01-11
Yannick Moy
[Ada]
P
roof of System
.
Vectors
.
Boolean_Operations
commit
|
commitdiff
|
tree
2022-01-06
Yann
i
c
k
Moy
[Ada] Proof of System
.
Gene
r
ic_Arra
y
_
O
perations a
t
silver
.
.
.
commit
|
commitdiff
|
tree
2022-01-06
Yannick
Moy
[Ada] Justify fals
e
p
o
s
iti
v
e
m
essage from CodePeer
.
.
.
commit
|
commitdiff
|
tree
2022-01-06
Ya
n
n
ick
Moy
[Ada] Proof of
r
untime unit for no
n
-binary m
o
dular
.
.
.
commit
|
commitdiff
|
tree
2022-01-06
Yanni
c
k
M
o
y
[Ada] Proof of run
t
ime units f
o
r binary m
o
dula
r
expo
n
entiation
commit
|
commitdiff
|
tree
2022-01-05
Yannick Mo
y
[Ada] Add contracts for the
pr
o
o
f
of System
.
Ari
t
h_1
2
8
commit
|
commitdiff
|
tree
2022-01-05
Yann
i
c
k M
o
y
[Ad
a
] Proof of ru
n
ti
m
e units for i
n
t
e
ge
r
exponentiation
.
.
.
commit
|
commitdiff
|
tree
2022-01-05
Yan
n
ic
k
Moy
[
A
da] Proo
f
of runtime uni
t
s for i
n
teger exponent
i
atio
n
.
.
.
commit
|
commitdiff
|
tree
2022-01-05
Yannick M
o
y
[
A
da]
R
e
n
ame parameter-depende
n
t con
s
tant
s
in ge
n
eric
.
.
.
commit
|
commitdiff
|
tree
2022-01-05
Yann
i
ck Moy
[Ada]
F
i
x
l
e
mma in g
e
neri
c
uni
t
System
.
A
r
ith_Doubl
e
commit
|
commitdiff
|
tree
2021-12-02
Yannick Mo
y
[Ada] Proof of System
.
A
rith_32 for doub
l
e a
r
it
h
metic
.
.
.
commit
|
commitdiff
|
tree
2021-12-02
Yann
i
ck Moy
[Ada] Amend proof of S
y
stem
.
Arith_Double to rem
o
ve
.
.
.
commit
|
commitdiff
|
tree
2021-12-02
Yannick Moy
[
Ada] Add
p
r
a
gma Annotate f
o
r CodePee
r
analysis
commit
|
commitdiff
|
tree
2021-12-02
Yannick Moy
[Ada]
Proo
f
of support u
n
its for 'Width
o
n
sign
e
d integ
e
rs
commit
|
commitdiff
|
tree
2021-12-02
Yanni
c
k
Moy
[Ada
]
P
roof of Interfaces
.
C w
i
th SPARK
commit
|
commitdiff
|
tree
2021-12-02
Yannick Mo
y
[
A
d
a] Pro
o
f of Syste
m
.
Val_Util utilities for 'V
a
lue
.
.
.
commit
|
commitdiff
|
tree
2021-12-02
Yan
n
ick
M
oy
[Ada] Proof of Boolean'Image and Boolean'Value
commit
|
commitdiff
|
tree
2021-12-01
Yannick Moy
[Ada] I
m
p
rove
error messages for dot no
t
ati
o
n
w
h
en
.
.
.
commit
|
commitdiff
|
tree
2021-12-01
Yanni
c
k Moy
[Ada]
A
dd query
f
or ext
e
nded precision f
l
oating-point
.
.
.
commit
|
commitdiff
|
tree
2021-12-01
Yannick Moy
[Ad
a
] Impro
v
e
m
e
s
s
ag
e
s
o
n incorrect s
t
ate refinement
.
.
.
commit
|
commitdiff
|
tree
2021-11-10
Yannick
M
oy
[Ada] Create explicit
g
h
o
st mirr
o
r uni
t
f
o
r
b
ig integers
commit
|
commitdiff
|
tree
2021-11-10
Yannick Mo
y
[Ada
]
Bette
r
error message on missing
par
e
n
theses
commit
|
commitdiff
|
tree
2021-11-09
Yanni
c
k Moy
[Ada] Com
p
le
t
e support fo
r
pref
i
xed call on s
u
btypes
.
.
.
commit
|
commitdiff
|
tree
2021-11-09
Yan
n
ick M
o
y
[Ada] Fix supp
o
rt for prefixed call
w
i
th incomplet
e
.
.
.
commit
|
commitdiff
|
tree
2021-10-25
Y
a
n
nick Moy
[A
d
a] I
s
su
e
error on
i
n
v
alid use of
G
host inside
p
ra
g
ma
.
.
.
commit
|
commitdiff
|
tree
2021-10-20
Y
ann
i
ck Moy
[Ada] Pr
o
of
of th
e
run
t
i
me
suppo
r
t fo
r
attribu
t
e
'
W
idth
commit
|
commitdiff
|
tree
2021-10-20
Yanni
c
k
M
oy
[
Ada] Provide dummy body for big
in
t
ege
r
s library used
.
.
.
commit
|
commitdiff
|
tree
next