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] Reject use in SPARK of Asm intrinsics for code insertions
2022-09-12
Yannick Mo
y
[Ada] Reject
u
se i
n
SPA
R
K of
A
sm in
t
rinsi
c
s for co
d
e
.
.
.
commit
|
commitdiff
|
tree
2022-09-02
Yanni
c
k
M
oy
[Ada] Rec
o
ver proof
o
f S
c
aled_Divide
i
n Sy
s
t
e
m
.
Ari
t
h_64
commit
|
commitdiff
|
tree
2022-07-13
Yannick Moy
[Ada]
Fix
incorrect handling of Ghost a
s
pect
commit
|
commitdiff
|
tree
2022-07-13
Yannick Moy
[Ad
a
] Fix pr
o
o
f
of runtime unit Sys
t
em
.
Arith_64
commit
|
commitdiff
|
tree
2022-07-13
Ya
n
nick
M
o
y
[Ada]
F
ix automatic pro
o
f on System
.
Arith_32
commit
|
commitdiff
|
tree
2022-07-12
Yann
i
c
k
Moy
[
Ada] Ignore switc
h
e
s for controlling front
e
n
d
warn
i
ng
s
.
.
.
commit
|
commitdiff
|
tree
2022-07-06
Y
a
nnick
M
oy
[Ada]
Deferred co
n
stant consider
e
d as not preelaborable
commit
|
commitdiff
|
tree
2022-07-06
Ya
n
nick M
o
y
[Ada] Sup
p
o
rt gh
o
st
generic form
a
l p
a
rameter
s
commit
|
commitdiff
|
tree
2022-07-05
Yannick Moy
[Ada] Fi
x
spurious
e
rror on obje
c
t renam
i
ng with ghost
.
.
.
commit
|
commitdiff
|
tree
2022-07-05
Yannic
k
Mo
y
[Ada] Spurious er
r
or on qualified pr
e
fix
i
n Pack
.
Func
.
.
.
commit
|
commitdiff
|
tree
2022-06-02
Yannick
Moy
[
Ada] Fix spurious
e
rrors on ghost
c
ode in generics
commit
|
commitdiff
|
tree
2022-06-02
Yannick Moy
[Ada] Issue errors on wrong context for
g
host entities
commit
|
commitdiff
|
tree
2022-06-02
Yanni
c
k Moy
[Ada] Remo
v
al of dead c
o
de Analy
z
e
_
L
a
bel_Entit
y
commit
|
commitdiff
|
tree
2022-06-01
Yannick Moy
[Ada]
Allow confirming volatile properties on No_Caching
.
.
.
commit
|
commitdiff
|
tree
2022-06-01
Ya
n
nic
k
M
o
y
[Ada] Fix classific
a
t
ion of Subprogr
a
m_Vari
a
nt as assertio
n
.
.
.
commit
|
commitdiff
|
tree
2022-06-01
Yannick Moy
[Ada] Issue a
warning o
n
entity hidde
n
in use_claus
e
.
.
.
commit
|
commitdiff
|
tree
2022-06-01
Yannick Moy
[A
d
a] Issue better e
r
ror messag
e
for
o
ut-of-order
keywords
.
.
.
commit
|
commitdiff
|
tree
2022-05-30
Yannick
Moy
[Ada] Updat
e
pro
o
fs of double arith
m
eti
c
u
n
it after
.
.
.
commit
|
commitdiff
|
tree
2022-05-30
Yann
i
ck Moy
[Ada] Adapt
p
r
oof of runtime un
i
t s-ari
t
32
commit
|
commitdiff
|
tree
2022-05-30
Yanni
c
k Moy
[Ada] PR ada/105303 Fix use of Assert
i
on_
P
olicy
i
n
.
.
.
commit
|
commitdiff
|
tree
2022-05-19
Y
a
n
n
i
c
k
M
oy
[Ada]
Furth
e
r
adapt proo
f
of double arithmetic runtime
.
.
.
commit
|
commitdiff
|
tree
2022-05-18
Yann
i
c
k
M
oy
[Ada] Adapt proof of double arithm
e
tic ru
n
time unit
commit
|
commitdiff
|
tree
2022-05-18
Yannick Mo
y
[A
d
a
] Fix
p
roo
f
of ru
n
time units
commit
|
commitdiff
|
tree
2022-05-18
Y
a
n
n
ic
k
Moy
[Ada] Spur
i
o
u
s error on freezing of tagged types i
n
.
.
.
commit
|
commitdiff
|
tree
2022-05-17
Yannic
k
Mo
y
[Ada] Allow inlining for proof inside gener
i
cs
commit
|
commitdiff
|
tree
2022-05-17
Ya
n
nic
k
Moy
[Ada
]
Fix insertion of
d
e
claration inside quantified
.
.
.
commit
|
commitdiff
|
tree
2022-05-16
Yannick M
o
y
[Ada] Fix
p
roof
o
f double
arithmetic units
commit
|
commitdiff
|
tree
2022-05-16
Yannick Moy
[
A
d
a
] Update comment justifying n
o
n
-inl
i
nin
g
for proof
.
.
.
commit
|
commitdiff
|
tree
2022-05-13
Yann
i
ck
Moy
[
A
da] Sim
p
lify helper units f
o
r
f
or
m
al hash
e
d sets
.
.
.
commit
|
commitdiff
|
tree
2022-05-13
Yann
i
ck M
o
y
[Ada]
A
dapt body
o
f
formal sets an
d
maps for SPAR
K
commit
|
commitdiff
|
tree
2022-05-13
Yannick Moy
[Ada] Rem
o
v
e
depen
d
en
c
y on tamperi
n
g checks and
c
ontrolle
d
.
.
.
commit
|
commitdiff
|
tree
2022-05-13
Yannick
Moy
[
A
da
]
Fa
c
ilitat
e
proo
f
of Overwrite in bounded strings
.
.
.
commit
|
commitdiff
|
tree
2022-05-12
Yannick Moy
[Ada
]
Remo
v
e
useless prag
m
a
Warni
n
gs Off from runtime
.
.
.
commit
|
commitdiff
|
tree
2022-05-12
Ya
n
nick Moy
[Ada] Do not
i
ssue a warning on a postcondition of
.
.
.
commit
|
commitdiff
|
tree
2022-05-12
Yann
i
ck M
o
y
[Ada]
A
d
d ghost code
to facilitate proof with SPARK
commit
|
commitdiff
|
tree
2022-05-12
Yannick Moy
[Ada] Remove use of use-cl
a
uses in loade
d
runt
i
me units
commit
|
commitdiff
|
tree
2022-05-12
Yan
n
ick Mo
y
[Ada]
A
d
apt CodePeer anal
y
sis
of GN
A
T
t
o
c
hanges in
.
.
.
commit
|
commitdiff
|
tree
2022-05-12
Yannick Moy
[
A
d
a] Proof o
f
'Image sup
p
o
r
t for si
g
ned integers
commit
|
commitdiff
|
tree
2022-05-11
Yannick Moy
[
A
da] Pr
o
of of 'I
m
age
s
upport
for
unsi
g
ned in
t
egers
commit
|
commitdiff
|
tree
2022-05-11
Y
annick
Moy
[Ada]
A
dapt proof
o
f
System
.
Ar
i
t
h
_
Doub
l
e aft
e
r update
.
.
.
commit
|
commitdiff
|
tree
2022-05-10
Y
a
nnick
M
oy
[Ada] Fix
i
ndentation
to follow unifor
m
sty
l
e across
.
.
.
commit
|
commitdiff
|
tree
2022-05-09
Yannick Moy
[Ada]
S
uggest use of First_Val
i
d/L
a
st_Val
i
d
on type
.
.
.
commit
|
commitdiff
|
tree
2022-05-09
Yannic
k
Mo
y
[Ad
a
] Set Error_Msg_Warn
bef
o
re u
s
e of << ins
e
rtion
commit
|
commitdiff
|
tree
2022-01-11
Yannick Moy
[
Ada] Adapt proof of Sys
t
em
.
Arith_Double
commit
|
commitdiff
|
tree
2022-01-11
Yanni
c
k M
o
y
[Ada]
Recover pr
o
o
f
of Ada
.
String
s
.
Fixed with assertions
commit
|
commitdiff
|
tree
2022-01-11
Yannick Moy
[Ada] Proof of unit Sys
t
em
.
Case_Uti
l
commit
|
commitdiff
|
tree
2022-01-11
Yannick Moy
[Ada] Adapt ghos
t
code to maint
a
in proof
commit
|
commitdiff
|
tree
2022-01-11
Yannick Moy
[Ad
a
]
P
roof of S
y
st
e
m
.
Vecto
r
s
.
B
o
olean_Operati
o
ns
commit
|
commitdiff
|
tree
2022-01-06
Y
annick Moy
[Ad
a
] Proof
of System
.
Generic_Array_Operations at
silver
.
.
.
commit
|
commitdiff
|
tree
2022-01-06
Y
anni
c
k Moy
[
A
da] Jus
t
ify
f
alse positive message f
r
om C
o
dePeer
.
.
.
commit
|
commitdiff
|
tree
2022-01-06
Yannick Moy
[A
d
a] Proof of runtime unit
f
or non-bin
a
r
y modular
.
.
.
commit
|
commitdiff
|
tree
2022-01-06
Yan
n
ick M
o
y
[A
d
a] P
r
oo
f
of
runtime units
for binary modu
l
ar expo
n
enti
a
tion
commit
|
commitdiff
|
tree
2022-01-05
Yannick Mo
y
[
Ada] Add contracts for the proof of System
.
Arith_128
commit
|
commitdiff
|
tree
2022-01-05
Yanni
c
k Mo
y
[Ada] Proof o
f
runtime units
for integer exp
o
n
e
ntiation
.
.
.
commit
|
commitdiff
|
tree
2022-01-05
Y
annick
Moy
[Ad
a
] Proof
o
f
run
t
im
e
unit
s
for integer exponentiat
i
on
.
.
.
commit
|
commitdiff
|
tree
2022-01-05
Yannick Moy
[
A
d
a] Rename parameter-depe
n
dent const
a
nt
s
i
n
gene
r
ic
.
.
.
commit
|
commitdiff
|
tree
2022-01-05
Ya
n
nick
M
oy
[A
d
a] Fix lemma
i
n g
e
neric unit System
.
Arith_Double
commit
|
commitdiff
|
tree
2021-12-02
Yann
i
ck M
o
y
[
A
da] Proof of Sy
s
tem
.
Arith_32 for
double ari
t
hmetic
.
.
.
commit
|
commitdiff
|
tree
2021-12-02
Yannick Moy
[Ada] Ame
n
d
proof of System
.
Arith_Double to remove
.
.
.
commit
|
commitdiff
|
tree
2021-12-02
Y
an
n
ick Moy
[Ada] Ad
d
p
ragm
a
Annotate for Code
P
eer analy
s
i
s
commit
|
commitdiff
|
tree
2021-12-02
Yannick Moy
[
A
da] Proof of supp
o
rt unit
s
f
o
r 'Width on s
i
gne
d
in
t
ege
r
s
commit
|
commitdiff
|
tree
2021-12-02
Yannick
Moy
[Ada] Proo
f
of Interfaces
.
C with SPARK
commit
|
commitdiff
|
tree
2021-12-02
Yannick Moy
[Ada] P
r
oof of System
.
Val
_
Util utilities for '
V
alue
.
.
.
commit
|
commitdiff
|
tree
2021-12-02
Yann
i
ck Moy
[Ada] Pr
o
of of Boolean'Image and Boolean'Value
commit
|
commitdiff
|
tree
2021-12-01
Yannick Moy
[Ada] Improv
e
e
r
ro
r
messages fo
r
dot
n
ot
a
ti
o
n whe
n
.
.
.
commit
|
commitdiff
|
tree
2021-12-01
Yannick Moy
[
A
da] A
d
d
query
fo
r
ext
e
n
d
e
d precision floatin
g
-point
.
.
.
commit
|
commitdiff
|
tree
2021-12-01
Yannick Moy
[Ada] Improve messages on incor
r
ect state refinem
e
nt
.
.
.
commit
|
commitdiff
|
tree
2021-11-10
Y
a
nni
c
k Moy
[Ada] Cre
a
te explicit ghost
m
irro
r
unit for
big integers
commit
|
commitdiff
|
tree
2021-11-10
Yannick
M
oy
[A
d
a
]
Be
t
ter error message
on missing parentheses
commit
|
commitdiff
|
tree
2021-11-09
Yannick
Mo
y
[Ada] Comp
l
ete support for prefixed call
o
n subt
y
pes
.
.
.
commit
|
commitdiff
|
tree
2021-11-09
Yannick
M
oy
[Ada]
Fi
x
suppor
t
fo
r
pr
e
f
ixed call w
i
th incomplete
.
.
.
commit
|
commitdiff
|
tree
2021-10-25
Yan
n
ick M
o
y
[A
d
a] Issu
e
erro
r
on inval
i
d use of Ghost in
s
i
de
p
rag
m
a
.
.
.
commit
|
commitdiff
|
tree
2021-10-20
Yannick Moy
[A
d
a] Proof o
f
the runt
i
me support f
o
r
attribute 'Width
commit
|
commitdiff
|
tree
2021-10-20
Yannick Mo
y
[Ada] Pro
v
i
d
e dummy body for big
int
e
ge
r
s library used
.
.
.
commit
|
commitdiff
|
tree
2021-10-20
Yanni
c
k Moy
[Ada
]
Is
s
ue warning
on un
u
sed quant
i
f
i
ed expression
commit
|
commitdiff
|
tree
2021-10-05
Y
annick Moy
[Ada] Improve err
o
r message on
a
rray aggregates
commit
|
commitdiff
|
tree
2021-10-05
Y
an
n
ick Moy
[Ada
]
Improve er
r
or message on
m
issing all/for in
quantified
.
.
.
commit
|
commitdiff
|
tree
2021-10-05
Yannick Moy
[Ada]
P
roof of Ada
.
Strings
.
M
aps
commit
|
commitdiff
|
tree
2021-10-05
Yannick Mo
y
[Ada]
P
r
o
of
o
f Ada
.
Charact
e
rs
.
Handling
commit
|
commitdiff
|
tree
2021-10-04
Yannick Moy
[Ada]
Mark
A
da
.
Te
x
t_I
O
in SP
A
RK
commit
|
commitdiff
|
tree
2021-10-04
Yann
i
ck Moy
[Ad
a
]
Add Ada
RM descripti
o
n of Ada
.
Strings
.
Bounded
.
.
.
commit
|
commitdiff
|
tree
2021-09-23
Yannic
k
Moy
[Ada]
Minimize p
a
rt
s
of Ada
.
S
trings
.
Fi
x
ed marked SPARK_Mode
.
.
.
commit
|
commitdiff
|
tree
2021-09-22
Yanni
c
k Moy
[Ada]
S
implif
y
contract o
f
Ada
.
Strings
.
F
i
x
ed
.
Trim for
.
.
.
commit
|
commitdiff
|
tree
2021-09-22
Yannick Moy
[A
d
a] Spurious error on defer
r
ed con
s
t
a
n
t
with
p
redicate
commit
|
commitdiff
|
tree
2021-09-22
Yannick Moy
[
Ada]
Clarify parts of Ada
.
Strings
.
Unbounded in SPARK
.
.
.
commit
|
commitdiff
|
tree
2021-09-22
Yannick Moy
[Ada] Ad
d
adequate guard b
e
fo
r
e calling Fi
r
st_R
e
p_
I
tem
commit
|
commitdiff
|
tree
2021-09-22
Yannic
k
Moy
[A
d
a] Fix infini
t
e loop in compilation o
f
illegal
code
commit
|
commitdiff
|
tree
2021-09-22
Yannick Moy
[
A
da] More precis
e
ana
l
y
s
is of function r
e
n
a
mings i
n
.
.
.
commit
|
commitdiff
|
tree
2021-09-22
Yannick Moy
[Ada] Fix
a
c
c
ess
to
p
r
e
d
icated
p
are
n
t in
I
type
commit
|
commitdiff
|
tree
2021-09-22
Y
a
nn
i
c
k
M
o
y
[Ada] Fix obso
l
ete c
o
m
m
ents/name ref
e
rri
n
g
to
girder
.
.
.
commit
|
commitdiff
|
tree
2021-09-21
Y
annick Moy
[Ada] Re
n
ame "optional" node subtypes
that allow
Em
p
t
y
commit
|
commitdiff
|
tree
2021-09-21
Y
a
nnick Moy
[
Ada] Exce
p
tion raise
d
on e
m
pty file
i
n GNATprov
e
m
o
d
e
commit
|
commitdiff
|
tree
2021-07-08
Yannick Moy
[Ada] Skip type
s
i
n
error fo
r
test to comp
u
te array
.
.
.
commit
|
commitdiff
|
tree
2021-07-08
Yannick Moy
[Ada] Fix on computation of packed
a
r
ray size in
c
as
e
.
.
.
commit
|
commitdiff
|
tree
2021-07-08
Yanni
c
k Moy
[
A
da] Compute
s
iz
e
s when possib
l
e for
p
a
c
ked ar
r
a
y
.
.
.
commit
|
commitdiff
|
tree
2021-07-07
Y
a
n
nick Moy
[
Ada] Simplify han
d
li
n
g
o
f sure err
o
rs in GNATprove
.
.
.
commit
|
commitdiff
|
tree
2021-07-07
Yannick Moy
[Ada] Fix precondition of
C
ot for
c
ode analyzers
commit
|
commitdiff
|
tree
2021-07-06
Ya
n
nick Moy
[Ada] Missing space in error
m
essage for pattern matching
commit
|
commitdiff
|
tree
2021-07-05
Y
a
n
n
ick Moy
[
A
da] Adapt SPARK
RM r
u
le on non
-
eff
e
ctively volatile
.
.
.
commit
|
commitdiff
|
tree
2021-07-05
Ya
n
nick
Moy
[Ada] Adapt SPARK checking after change in rules regardi
n
g
.
.
.
commit
|
commitdiff
|
tree
next