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 incorrect quoting in documentation
2023-11-28
Yannick Moy
ada: Remove
dependency on S
y
st
e
m
.
Val
_
Bool in Syste
m
.
.
.
commit
|
commitdiff
|
tree
2023-11-21
Yan
n
ic
k
Moy
ada: Fix
t
ype for S
P
A
R
K expansion on deep delta
aggregates
commit
|
commitdiff
|
tree
2023-11-07
Yanni
c
k M
o
y
ada: Rename Is_Li
m
ited_V
i
ew to
r
efl
e
ct
actual que
r
y
commit
|
commitdiff
|
tree
2023-10-19
Y
a
nni
c
k Moy
ad
a
: Support new SPARK
aspect Side_
E
ff
e
cts
commit
|
commitdiff
|
tree
2023-09-26
Yannick Moy
ada: Cl
a
rify RM references that justi
f
y
a constraint
.
.
.
commit
|
commitdiff
|
tree
2023-09-14
Y
a
nnick Moy
ada: Improve
d
etec
t
ion of d
e
ac
t
ivated c
o
de fo
r
warnin
g
s
.
.
.
commit
|
commitdiff
|
tree
2023-08-07
Yannick M
o
y
ada: C
r
ash in
G
NATprove due to w
r
ong dete
c
tion of inlining
commit
|
commitdiff
|
tree
2023-08-01
Y
annick Mo
y
ada: Fix pri
n
tin
g
of
n
u
mbers
in JSON outp
u
t for data
.
.
.
commit
|
commitdiff
|
tree
2023-08-01
Yanni
c
k Moy
ada: Disable in
l
ining of subp
r
o
g
rams with Ski
p
(_Flow_And
.
.
.
commit
|
commitdiff
|
tree
2023-08-01
Yanni
c
k Moy
a
d
a: Fix generation
o
f JSON output
f
o
r d
a
ta represe
n
tation
commit
|
commitdiff
|
tree
2023-07-18
Yannick Moy
a
d
a
:
A
l
low warnings with e
x
plain code
commit
|
commitdiff
|
tree
2023-07-10
Ya
n
nic
k
Moy
ada: Simplify
a
s
sertio
n
to remove CodePeer message
commit
|
commitdiff
|
tree
2023-07-10
Yannick Moy
ada:
A
dapt pr
o
of o
f
System
.
Arith_Do
u
ble t
o
re
m
ove CVC4
commit
|
commitdiff
|
tree
2023-07-06
Y
a
n
nick Moy
ada
:
Im
p
ro
v
e
e
r
ror me
s
s
a
ge on v
i
olatio
n
of SPARK_Mode
.
.
.
commit
|
commitdiff
|
tree
2023-07-04
Yannic
k
M
oy
ada:
F
ix
l
ist of
i
nherited subprograms in query fo
r
.
.
.
commit
|
commitdiff
|
tree
2023-06-20
Yannick Moy
ada: Fix
crash on inlining in GNAT
p
r
ove
commit
|
commitdiff
|
tree
2023-06-20
Y
a
nnic
k
Moy
ada: Do not issue
w
arning on postcondition in so
m
e
.
.
.
commit
|
commitdiff
|
tree
2023-06-20
Yannic
k
M
o
y
ada: Add th
e
abi
l
it
y
t
o
a
dd
err
o
r
c
odes
t
o
e
rror messages
commit
|
commitdiff
|
tree
2023-06-20
Yann
i
ck Moy
ada: Update annotatio
n
s
in runtim
e
f
or pro
o
f
commit
|
commitdiff
|
tree
2023-06-15
Yannick
M
oy
ada: Reject
L
oop_Entry inside pre
f
ix of
Loop_Entry
commit
|
commitdiff
|
tree
2023-06-13
Y
a
nnick Mo
y
ada:
Mark attribute Initialized as
ghos
t
code
commit
|
commitdiff
|
tree
2023-06-13
Yannic
k
Moy
ada: Us
e
ghost predicate in s
t
andard l
i
brary
commit
|
commitdiff
|
tree
2023-06-13
Yannick Moy
ada: Suppo
r
t new G
N
AT-specific aspec
t
Ghost_Pre
d
i
cate
commit
|
commitdiff
|
tree
2023-05-29
Yannick
Moy
a
d
a: Res
t
ore SPARK_Mode On f
o
r numerical
functi
o
ns
commit
|
commitdiff
|
tree
2023-05-26
Yannick
M
o
y
ada: Default initialize e
n
tity to avoid Code
P
ee
r
m
e
s
s
age
commit
|
commitdiff
|
tree
2023-05-26
Yanni
c
k Moy
ada: Minor doc clar
i
fication
commit
|
commitdiff
|
tree
2023-05-26
Ya
n
nick M
o
y
a
d
a: Complete contrac
t
s
o
f
SPARK units
commit
|
commitdiff
|
tree
2023-05-23
Yannick Moy
ada: Ad
d
defau
l
t
v
alue at initialization for
CodePeer
commit
|
commitdiff
|
tree
2023-05-23
Yannick
Mo
y
ada:
F
acilitat
e
proof of Interfaces
.
C
.
T
o
_Ada
commit
|
commitdiff
|
tree
2023-05-16
Y
a
nni
c
k
Moy
ada:
Upda
t
e proof of runtime units
commit
|
commitdiff
|
tree
2023-05-16
Yanni
c
k Moy
ada:
S
implify
d
ramatically g
h
ost co
d
e
fo
r
p
roof of
.
.
.
commit
|
commitdiff
|
tree
2023-05-16
Yannick Moy
ada:
A
dd
i
ntermediate assertions for proof of S
u
pe
r
_Tail
commit
|
commitdiff
|
tree
2023-05-16
Yannick Moy
ada: Set Loop_Variant assertion po
l
icy t
o
Ignore in
.
.
.
commit
|
commitdiff
|
tree
2023-05-16
Yannick
M
oy
ada: Re
s
tore proof of System
.
Arith_Double
commit
|
commitdiff
|
tree
2023-05-15
Yannick Moy
ada: Add a
n
notation
s
for
p
roo
f
o
f
ter
m
ina
t
i
o
n of runtime
.
.
.
commit
|
commitdiff
|
tree
2023-05-15
Yannick Moy
a
da:
R
ecove
r
p
r
oof of
r
untime uni
t
s
commit
|
commitdiff
|
tree
2023-05-15
Ya
n
nic
k
M
o
y
ada:
Recover proof
o
f
Interfaces
.
C
for termina
t
ion
commit
|
commitdiff
|
tree
2023-05-15
Yannick Moy
a
d
a: U
p
date
c
omment af
t
er SPARK RM
c
h
ange
commit
|
commitdiff
|
tree
2023-05-15
Yanni
c
k Moy
ada: Fix handl
i
n
g
of pragma War
n
ings
(
To
o
l
name, Off/On)
commit
|
commitdiff
|
tree
2023-05-15
Yannick
M
oy
ada: Al
l
ow pragmas A
n
no
t
ate between lo
o
p pragmas
commit
|
commitdiff
|
tree
2022-12-06
Y
annick Moy
ada:
Allow
No_Caching on volatile
t
ypes
commit
|
commitdiff
|
tree
2022-11-28
Y
a
nnick Moy
a
d
a
: Impleme
n
t change t
o
SPAR
K
RM rule o
n
state refineme
n
t
commit
|
commitdiff
|
tree
2022-11-14
Y
a
nnick Moy
ada:
F
ix error on SPA
R
K_Mode on library-leve
l
se
p
arate
.
.
.
commit
|
commitdiff
|
tree
2022-11-14
Y
a
nnick Moy
ada
:
I
mprove lo
c
ation of error me
s
sages in i
n
s
tantiations
commit
|
commitdiff
|
tree
2022-10-06
Yannick Moy
ada: Do not
i
ssue co
m
pil
e
r warnings in GN
A
Tprov
e
m
o
d
e
commit
|
commitdiff
|
tree
2022-09-12
Yannick Moy
[Ad
a
] Justify false alarm
from
CodePeer analysis of
.
.
.
commit
|
commitdiff
|
tree
2022-09-12
Yan
n
i
c
k Moy
[Ada]
A
ccept
expli
c
it SPARK_Mode Auto as configuration
.
.
.
commit
|
commitdiff
|
tree
2022-09-12
Y
ann
i
ck Moy
[Ad
a
]
Rej
e
ct use in
S
PARK o
f
Asm
in
t
rinsics
for code
.
.
.
commit
|
commitdiff
|
tree
2022-09-02
Yannick Moy
[
Ada] Recover proof
of Scaled_Divide
i
n
Syste
m
.
Ar
i
th_64
commit
|
commitdiff
|
tree
2022-07-13
Yannick M
o
y
[Ada] Fix incorrect handling of Ghost
a
s
p
ect
commit
|
commitdiff
|
tree
2022-07-13
Y
annick Moy
[Ada] Fi
x
proof
o
f runtim
e
uni
t
System
.
Arith_64
commit
|
commitdiff
|
tree
2022-07-13
Yannick Moy
[Ada
]
Fix automatic proof on System
.
A
rith_32
commit
|
commitdiff
|
tree
2022-07-12
Y
a
n
n
ick Moy
[Ada] Ign
o
re switches for
controlling fro
n
tend warnings
.
.
.
commit
|
commitdiff
|
tree
2022-07-06
Y
annick Moy
[Ada] D
e
ferred constant con
s
idered
a
s
not preelabora
b
l
e
commit
|
commitdiff
|
tree
2022-07-06
Yanni
c
k Moy
[Ada] Support ghost generic
formal
p
arameters
commit
|
commitdiff
|
tree
2022-07-05
Y
anni
c
k Moy
[
A
da] F
i
x spu
r
ious error on o
b
ject renam
i
ng wi
t
h
ghost
.
.
.
commit
|
commitdiff
|
tree
2022-07-05
Yannick Moy
[Ada] Spurious
e
rr
o
r on qualified prefi
x
in Pack
.
Func
.
.
.
commit
|
commitdiff
|
tree
2022-06-02
Y
annick Moy
[Ada]
F
ix spurio
u
s err
o
rs on ghost co
d
e in gene
r
ics
commit
|
commitdiff
|
tree
2022-06-02
Yan
n
i
ck Moy
[A
d
a] Issue
e
rrors on wrong co
n
text fo
r
ghost entities
commit
|
commitdiff
|
tree
2022-06-02
Ya
n
nick Moy
[Ada]
Removal of
dead code Ana
l
yze_Label_Entity
commit
|
commitdiff
|
tree
2022-06-01
Yann
i
ck M
o
y
[Ada
]
Allow
c
on
f
irm
i
n
g
volat
i
le prope
r
ties on No_Cac
h
ing
.
.
.
commit
|
commitdiff
|
tree
2022-06-01
Y
a
n
n
ick
M
oy
[Ad
a
]
Fix classificat
i
on of Subprogr
a
m_Varian
t
as as
s
ertio
n
.
.
.
commit
|
commitdiff
|
tree
2022-06-01
Y
a
nnick Moy
[Ada] Issue a warn
i
ng on entity hid
d
en in use_clause
.
.
.
commit
|
commitdiff
|
tree
2022-06-01
Yannick Mo
y
[
Ad
a
] Issu
e
bett
e
r
error messa
g
e f
o
r
o
ut-
o
f-orde
r
key
w
or
d
s
.
.
.
commit
|
commitdiff
|
tree
2022-05-30
Yannick Moy
[Ada
]
U
pda
t
e pr
o
ofs
o
f
d
o
uble ar
i
thmet
i
c
unit after
.
.
.
commit
|
commitdiff
|
tree
2022-05-30
Y
a
nnick Moy
[Ada] Adapt proof of runtime unit s-a
r
it32
commit
|
commitdiff
|
tree
2022-05-30
Y
a
nni
c
k Moy
[Ada]
P
R
ada/105303 Fix use of Assertion_Pol
i
cy i
n
.
.
.
commit
|
commitdiff
|
tree
2022-05-19
Yan
n
ick Moy
[Ada] Furth
e
r adapt
p
roof of
double arithmetic runtime
.
.
.
commit
|
commitdiff
|
tree
2022-05-18
Yann
i
c
k Moy
[
Ada] Ada
p
t p
r
oo
f
o
f
double a
r
ithmetic
runtime
u
nit
commit
|
commitdiff
|
tree
2022-05-18
Y
a
n
nick Moy
[
Ada] F
i
x
proof of runtime un
i
ts
commit
|
commitdiff
|
tree
2022-05-18
Yann
i
ck Moy
[Ada]
Spurious error on freezing of tagged
t
ypes in
.
.
.
commit
|
commitdiff
|
tree
2022-05-17
Yannick Moy
[Ad
a
]
All
o
w inlining for pro
o
f
i
ns
i
de
g
enerics
commit
|
commitdiff
|
tree
2022-05-17
Yan
n
ick Moy
[Ad
a
] Fix ins
e
rt
i
on
o
f declaratio
n
inside qua
n
tified
.
.
.
commit
|
commitdiff
|
tree
2022-05-16
Yannic
k
Mo
y
[Ad
a
] Fix pr
o
of
o
f do
u
bl
e
arithmetic units
commit
|
commitdiff
|
tree
2022-05-16
Ya
n
ni
c
k M
o
y
[Ada] Update comment j
u
s
ti
f
y
ing non-inl
i
n
ing for pr
o
of
.
.
.
commit
|
commitdiff
|
tree
2022-05-13
Yan
n
ick Moy
[Ada] Simp
l
i
f
y he
l
p
e
r u
n
i
t
s for formal
hashed sets
.
.
.
commit
|
commitdiff
|
tree
2022-05-13
Yannick
M
o
y
[Ada
]
Adapt body of
form
a
l
set
s
and m
a
ps
f
or SPARK
commit
|
commitdiff
|
tree
2022-05-13
Yannick Moy
[Ada] Remove dependen
c
y on
t
amperi
n
g
c
hecks a
n
d contr
o
lled
.
.
.
commit
|
commitdiff
|
tree
2022-05-13
Y
anni
c
k
Mo
y
[Ada] Facilitate proof of Overwrite in bounded strings
.
.
.
commit
|
commitdiff
|
tree
2022-05-12
Yannic
k
Moy
[Ada] Remov
e
useless pragma
W
a
r
n
i
ngs Off fro
m
runtime
.
.
.
commit
|
commitdiff
|
tree
2022-05-12
Y
annick
M
oy
[
Ada] Do not issue a warning on a post
c
ondition
o
f
.
.
.
commit
|
commitdiff
|
tree
2022-05-12
Yannick Moy
[Ada
]
Add ghost code to facilit
a
t
e
proof wit
h
SPARK
commit
|
commitdiff
|
tree
2022-05-12
Yannic
k
Moy
[Ada] Rem
o
v
e
use of us
e
-
clauses in loaded runt
i
m
e
u
n
i
t
s
commit
|
commitdiff
|
tree
2022-05-12
Yanni
c
k Moy
[A
d
a] A
d
apt C
o
d
ePeer analysis of GNAT t
o
changes
i
n
.
.
.
commit
|
commitdiff
|
tree
2022-05-12
Yanni
c
k M
o
y
[Ada] Proof o
f
'
Image supp
o
r
t
for signe
d
integers
commit
|
commitdiff
|
tree
2022-05-11
Ya
n
n
ick Moy
[Ada] Proo
f
of 'Image support f
o
r u
n
sig
n
ed integer
s
commit
|
commitdiff
|
tree
2022-05-11
Y
a
nnick Moy
[Ada] Adap
t
proo
f
o
f
Syste
m
.
Ar
i
th_D
o
uble after update
.
.
.
commit
|
commitdiff
|
tree
2022-05-10
Yan
n
ick
M
oy
[Ada] F
i
x indenta
t
i
o
n to follow uniform sty
l
e
acros
s
.
.
.
commit
|
commitdiff
|
tree
2022-05-09
Yannick
M
oy
[Ada]
S
ug
g
est use of Fir
s
t_Valid/L
a
st_Valid
o
n type
.
.
.
commit
|
commitdiff
|
tree
2022-05-09
Ya
n
nick
Moy
[Ada]
Set Error_Msg_
W
arn before use of << insertion
commit
|
commitdiff
|
tree
2022-01-11
Yannick Mo
y
[Ada] Ad
a
p
t proof o
f
S
y
stem
.
A
r
ith_Dou
b
l
e
commit
|
commitdiff
|
tree
2022-01-11
Ya
n
nic
k
Moy
[Ada
]
Recover proof of Ada
.
Strings
.
Fixe
d
wi
t
h asser
t
ions
commit
|
commitdiff
|
tree
2022-01-11
Yannick Moy
[Ada]
Proof of unit
S
y
stem
.
Case
_
U
t
il
commit
|
commitdiff
|
tree
2022-01-11
Yannick
M
o
y
[
A
da] Ad
a
pt
g
h
ost co
d
e to maintain proof
commit
|
commitdiff
|
tree
2022-01-11
Yannick Moy
[Ada] Pr
o
of o
f
System
.
Vectors
.
Boolean_
O
per
a
tions
commit
|
commitdiff
|
tree
2022-01-06
Yannick Mo
y
[Ada] Proof o
f
Sy
s
tem
.
Gene
r
ic_A
r
ray_Operations at silver
.
.
.
commit
|
commitdiff
|
tree
2022-01-06
Yann
i
ck Moy
[Ad
a
] Justi
f
y false
p
o
s
itive message from Co
d
ePeer
.
.
.
commit
|
commitdiff
|
tree
2022-01-06
Yann
i
c
k
Moy
[Ada] Proof o
f
runti
m
e unit for
non
-
b
i
n
ar
y
modular
.
.
.
commit
|
commitdiff
|
tree
2022-01-06
Yanni
c
k Moy
[Ada] Proof of runti
m
e units
for bina
r
y mod
u
lar ex
p
onentiati
o
n
commit
|
commitdiff
|
tree
2022-01-05
Y
a
nnick Moy
[Ada] Add contracts for the
p
roof of Sy
s
tem
.
A
rith_128
commit
|
commitdiff
|
tree
next