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] Set Error_Msg_Warn before use of << insertion
2022-05-09
Yannick Moy
[Ada
]
Set Error_Msg_Warn before use of << insert
i
o
n
commit
|
commitdiff
|
tree
2022-01-11
Yannick M
o
y
[Ada]
Adapt
p
roo
f
of Syste
m
.
Ari
t
h_Double
commit
|
commitdiff
|
tree
2022-01-11
Y
a
nn
i
ck Mo
y
[Ada] Recover proof of Ada
.
St
r
ings
.
Fixed wit
h
assertions
commit
|
commitdiff
|
tree
2022-01-11
Yan
n
i
c
k
Moy
[Ada]
Proof
o
f
unit
S
yst
e
m
.
Case_Util
commit
|
commitdiff
|
tree
2022-01-11
Y
annick Moy
[Ada] Adapt ghos
t
c
ode to m
a
intain proof
commit
|
commitdiff
|
tree
2022-01-11
Yanni
c
k Moy
[Ada] Proof
o
f
S
y
st
e
m
.
Vect
o
rs
.
B
oo
l
ean_Operat
i
ons
commit
|
commitdiff
|
tree
2022-01-06
Ya
n
nick Moy
[
A
d
a
] Proo
f
of System
.
Generic_
A
rra
y
_Operations at silver
.
.
.
commit
|
commitdiff
|
tree
2022-01-06
Yannick
Moy
[Ada] Justify false p
o
sitive message from CodePeer
.
.
.
commit
|
commitdiff
|
tree
2022-01-06
Yannick Moy
[Ada]
Proof of run
t
ime unit for non-
b
i
nary modular
.
.
.
commit
|
commitdiff
|
tree
2022-01-06
Yan
n
ick Moy
[A
d
a] Proof of runt
i
m
e uni
t
s fo
r
b
inary
m
odular exponentia
t
i
on
commit
|
commitdiff
|
tree
2022-01-05
Yannick Moy
[Ada] Add
c
ontracts
for the
proof of System
.
Arith_128
commit
|
commitdiff
|
tree
2022-01-05
Yanni
c
k
M
oy
[
A
d
a
] Proof of run
t
ime units for integer exponentiation
.
.
.
commit
|
commitdiff
|
tree
2022-01-05
Yanni
c
k
M
oy
[Ada] P
r
oof of runtime units
for int
e
ger
exponentiation
.
.
.
commit
|
commitdiff
|
tree
2022-01-05
Y
a
nnick
Moy
[A
d
a
] Rename param
e
ter-dependent constants in ge
n
eri
c
.
.
.
commit
|
commitdiff
|
tree
2022-01-05
Yannick Moy
[Ad
a
] Fix lemma in generic unit
S
y
s
t
e
m
.
A
rith_D
o
uble
commit
|
commitdiff
|
tree
2021-12-02
Yannick Moy
[Ada
]
Pro
o
f
of System
.
Arit
h
_32 for double
arithmetic
.
.
.
commit
|
commitdiff
|
tree
2021-12-02
Y
a
nnick Moy
[Ada]
A
mend pr
o
of of System
.
Arith_Double to remove
.
.
.
commit
|
commitdiff
|
tree
2021-12-02
Yanni
c
k Moy
[
Ada] Add prag
m
a Annotate for CodePeer ana
l
ysis
commit
|
commitdiff
|
tree
2021-12-02
Yannick M
o
y
[Ada] Proof
of support units
for
'W
i
dth on signed integers
commit
|
commitdiff
|
tree
2021-12-02
Yann
i
c
k Moy
[Ada] Proof of Interfac
e
s
.
C with S
P
ARK
commit
|
commitdiff
|
tree
2021-12-02
Y
a
nnick
Moy
[
Ada
]
Proof of
System
.
Val_Util utilities for
'Value
.
.
.
commit
|
commitdiff
|
tree
2021-12-02
Yan
n
ick Moy
[Ada]
P
roof o
f
Bool
e
an'Im
a
ge
and Bool
e
an'Va
l
ue
commit
|
commitdiff
|
tree
2021-12-01
Yannick Moy
[Ada] Improve error me
s
sa
g
es for dot notation when
.
.
.
commit
|
commitdiff
|
tree
2021-12-01
Yanni
c
k
Moy
[Ada] Add query
for ext
e
nde
d
p
r
eci
s
ion floating-point
.
.
.
commit
|
commitdiff
|
tree
2021-12-01
Yannick M
o
y
[
A
da]
I
mprove messages on incorre
c
t state refinement
.
.
.
commit
|
commitdiff
|
tree
2021-11-10
Yann
i
ck Moy
[Ada] Creat
e
explicit ghost mirror unit for big integers
commit
|
commitdiff
|
tree
2021-11-10
Yannick Moy
[Ada]
Better
e
rror message on missin
g
parentheses
commit
|
commitdiff
|
tree
2021-11-09
Yannick Mo
y
[Ada] Complete
s
u
p
port for pref
i
xed call
on
s
ubtypes
.
.
.
commit
|
commitdiff
|
tree
2021-11-09
Yannick Moy
[Ada] Fix support fo
r
prefixed call with incomplete
.
.
.
commit
|
commitdiff
|
tree
2021-10-25
Yan
n
ick Mo
y
[Ada] Issue error on in
v
alid use
o
f
G
h
ost inside pragma
.
.
.
commit
|
commitdiff
|
tree
2021-10-20
Y
a
nnick Moy
[
A
da]
P
roof of the runtime suppor
t
for attribute 'Width
commit
|
commitdiff
|
tree
2021-10-20
Yannic
k
M
oy
[Ada] Provide dummy bod
y
for bi
g
int
e
gers l
i
brary used
.
.
.
commit
|
commitdiff
|
tree
2021-10-20
Yanni
c
k M
o
y
[A
d
a
]
Issue war
n
ing on unused quantifi
e
d
e
xpressi
o
n
commit
|
commitdiff
|
tree
2021-10-05
Ya
n
nick Moy
[Ada] Impr
o
ve error me
s
sage o
n
array aggregates
commit
|
commitdiff
|
tree
2021-10-05
Yannick Mo
y
[Ada] Improve error message on
missi
n
g all/for in quanti
f
i
e
d
.
.
.
commit
|
commitdiff
|
tree
2021-10-05
Y
a
nnick Moy
[Ada] Proof of
A
da
.
St
r
i
ngs
.
Maps
commit
|
commitdiff
|
tree
2021-10-05
Yannick
Moy
[
A
da]
P
roof of Ada
.
Characte
r
s
.
Handling
commit
|
commitdiff
|
tree
2021-10-04
Yannick Moy
[Ada]
M
ark Ada
.
Text_IO in SPARK
commit
|
commitdiff
|
tree
2021-10-04
Yannick M
o
y
[
Ada
]
Add Ad
a
RM description of
Ada
.
Strin
g
s
.
Bounded
.
.
.
commit
|
commitdiff
|
tree
2021-09-23
Yan
n
ick Moy
[
A
da]
Mini
m
ize parts
o
f Ada
.
Strings
.
Fix
e
d marked SPARK_Mode
.
.
.
commit
|
commitdiff
|
tree
2021-09-22
Yannick Moy
[Ada] Simplify contract of
Ada
.
Strings
.
Fi
x
ed
.
Trim for
.
.
.
commit
|
commitdiff
|
tree
2021-09-22
Ya
n
n
ick Moy
[Ad
a
] Spuri
o
us err
o
r
on deferred constant
with
pre
d
icate
commit
|
commitdiff
|
tree
2021-09-22
Yannick Moy
[
Ad
a
]
C
larify
pa
r
ts of Ada
.
S
t
rings
.
Unbounded in SPA
R
K
.
.
.
commit
|
commitdiff
|
tree
2021-09-22
Y
annick Moy
[
Ada]
A
dd
a
dequate guard before
c
allin
g
Firs
t
_Rep_Item
commit
|
commitdiff
|
tree
2021-09-22
Yannick Moy
[Ada] Fi
x
infinit
e
l
oop in compi
l
ation of illegal code
commit
|
commitdiff
|
tree
2021-09-22
Yannick
M
oy
[A
d
a
]
More pr
e
cise analysis of function renaming
s
in
.
.
.
commit
|
commitdiff
|
tree
2021-09-22
Y
a
nn
i
ck
Moy
[Ada]
Fix access to predicated parent
i
n
Itype
commit
|
commitdiff
|
tree
2021-09-22
Yannick Moy
[
A
da
]
Fix obsolete comm
e
n
ts/name
referring to
girder
.
.
.
commit
|
commitdiff
|
tree
2021-09-21
Ya
n
nick
M
o
y
[
Ada] Rename "optional"
n
ode subtypes that
a
llow Empty
commit
|
commitdiff
|
tree
2021-09-21
Yannick M
o
y
[Ada]
Exception raised on
empty fi
l
e
i
n
GNA
T
prove
m
ode
commit
|
commitdiff
|
tree
2021-07-08
Y
annick Moy
[Ada] Sk
i
p ty
p
es in error for test
t
o compute array
.
.
.
commit
|
commitdiff
|
tree
2021-07-08
Yannic
k
Moy
[Ada] F
i
x on
c
o
m
putation of packed array size in case
.
.
.
commit
|
commitdiff
|
tree
2021-07-08
Ya
n
nick Mo
y
[Ada] Compute size
s
whe
n
possib
l
e for pac
k
ed ar
r
ay
.
.
.
commit
|
commitdiff
|
tree
2021-07-07
Yannick Moy
[Ada] Simpli
f
y
han
d
ling
o
f sure
errors in GN
A
Tprove
.
.
.
commit
|
commitdiff
|
tree
2021-07-07
Yannick Moy
[
A
da] Fix precondition
o
f
Co
t
for code analyz
e
rs
commit
|
commitdiff
|
tree
2021-07-06
Yann
i
ck Moy
[Ada] M
i
s
s
i
ng
s
pa
c
e
i
n error message for patt
e
rn matching
commit
|
commitdiff
|
tree
2021-07-05
Yanni
c
k Moy
[Ada] Adapt SPARK RM rule on n
o
n-effecti
v
ely vol
a
t
ile
.
.
.
commit
|
commitdiff
|
tree
2021-07-05
Yannick Moy
[
Ada] Adapt SPARK
che
c
k
i
ng after cha
n
ge in rules regarding
.
.
.
commit
|
commitdiff
|
tree
2021-06-16
Yannick Mo
y
[Ada] Do
not genera
t
e an I
t
ype_Refe
r
e
nce node fo
r
slice
s
.
.
.
commit
|
commitdiff
|
tree
2021-06-15
Yann
i
ck Moy
[Ada] Extend function to retrieve firs
t
/last
n
odes
.
.
.
commit
|
commitdiff
|
tree
2021-06-15
Yann
i
ck Moy
[Ada]
C
larify the semantics of sig
n
ed intrinsic shift
.
.
.
commit
|
commitdiff
|
tree
2021-05-07
Yannick
M
o
y
[Ada]
Generate w
a
rning fo
r
negative l
i
teral of a mo
d
ular
.
.
.
commit
|
commitdiff
|
tree
2021-05-04
Yannick M
o
y
[Ada] Minor twe
a
k
in pretty
-
pri
n
t
ing of expres
s
ion
s
commit
|
commitdiff
|
tree
2021-05-04
Y
anni
c
k M
o
y
[Ada
]
Move match fun
c
tion fo
r
pragma Warnings to p
u
blic
.
.
.
commit
|
commitdiff
|
tree
2021-05-04
Y
a
n
n
ick Moy
[Ada] Use error marke
r
for messages in GNATprove mode
commit
|
commitdiff
|
tree
2021-05-04
Yannick Moy
[Ada] Fix continuati
o
n message f
o
r missing ALL in a
c
cess
.
.
.
commit
|
commitdiff
|
tree
2021-04-29
Ya
n
nick Moy
[Ada] Add co
l
ors t
o
GNATprove mess
a
ges output to a
.
.
.
commit
|
commitdiff
|
tree
2021-04-29
Yannick
Moy
[Ada] Fix evalu
a
tion of expressions in inlined cod
e
commit
|
commitdiff
|
tree
2021-04-29
Y
annick Moy
[Ada]
Fixes i
n
the use of spans for e
r
ror l
o
cations
commit
|
commitdiff
|
tree
2021-04-28
Yann
i
ck
M
oy
[Ada] Use
s
pans instead of
l
ocations
f
or compiler
d
iagn
o
stics
commit
|
commitdiff
|
tree
2021-04-28
Yannick Moy
[Ada
]
I
m
prov
e
error message f
o
r ghost
in predic
a
te
commit
|
commitdiff
|
tree
2020-12-17
Yannick Moy
[Ada] Fixes
f
or G
N
AT error/warning message
s
commit
|
commitdiff
|
tree
2020-12-16
Yan
n
ick Moy
[Ada] Mark generic body outside of SPARK
commit
|
commitdiff
|
tree
2020-12-15
Yannick Moy
[A
d
a] Mark g
e
neri
c
body
o
utsi
d
e of
SPARK
commit
|
commitdiff
|
tree
2020-12-14
Yannick Moy
[Ada] Fix
warn
i
ng control cha
r
a
c
ter for
m
e
s
s
age on
.
.
.
commit
|
commitdiff
|
tree
2020-12-14
Yan
n
ic
k
Moy
[Ada] Refine
error m
e
ssages on illegal Re
f
ine
d
_
State
.
.
.
commit
|
commitdiff
|
tree
2020-12-14
Y
annick
Moy
[Ada] Co
r
rectly
mark subprogra
m
as
not al
w
ays inli
n
ed
.
.
.
commit
|
commitdiff
|
tree
2020-11-30
Yannick Moy
[Ada] Add comment on
special Heap
v
ariabl
e
use
d
in
.
.
.
commit
|
commitdiff
|
tree
2020-11-30
Yannick Moy
[A
d
a] Add continuation mes
s
age w
h
en othe
r
s choice not
.
.
.
commit
|
commitdiff
|
tree
2020-11-27
Yannick Moy
[Ada] Do not
apply rang
e
checks inside gen
e
r
i
cs in
.
.
.
commit
|
commitdiff
|
tree
2020-11-26
Yan
n
ick Mo
y
[Ada] New warning on questionable m
i
ssing
par
e
ntheses
commit
|
commitdiff
|
tree
2020-11-26
Yannick Moy
[Ada]
I
s
sue advice for error
regarding Old/Loo
p
_Entry
.
.
.
commit
|
commitdiff
|
tree
2020-11-25
Yannick Moy
[Ada] Minim
i
ze si
d
e-effect removal in GNATprove mode
commit
|
commitdiff
|
tree
2020-11-25
Yann
i
ck Moy
[Ada] Fix internal compila
t
io
n
erro
r
on c
i
rcular
type
.
.
.
commit
|
commitdiff
|
tree
2020-11-24
Yannick Moy
[Ada] Fix crash in G
N
ATpro
v
e
o
n inline
d
su
b
program
.
.
.
commit
|
commitdiff
|
tree
2020-11-24
Yannick
M
oy
[Ada]
H
andle correctly current insta
n
ce of PO
in local
.
.
.
commit
|
commitdiff
|
tree
2020-11-24
Yannick M
o
y
[
A
da] Fix
spur
i
ou
s
error on ch
i
l
d library-leve
l
subpro
g
r
a
m
.
.
.
commit
|
commitdiff
|
tree
2020-11-24
Yanni
c
k Moy
[Ada]
Rejec
t
G
l
oba
l
/Depends
co
n
tracts on nul
l
proce
d
u
res
commit
|
commitdiff
|
tree
2020-10-26
Yan
n
ick
M
o
y
[Ada
]
F
i
x G
N
ATpro
v
e crash on generics with access type
s
commit
|
commitdiff
|
tree
2020-10-26
Y
a
nnick
Moy
[A
d
a] Do not instantiate generic b
o
dies outside of
.
.
.
commit
|
commitdiff
|
tree
2020-10-21
Yann
i
ck Moy
[
A
da] Fix target configurat
i
on
f
ile used for Code
P
eer
.
.
.
commit
|
commitdiff
|
tree
2020-10-20
Yannick Moy
[A
d
a] F
i
x
e
s for pretty comm
a
nd-
l
i
ne GNATpro
v
e o
u
tput
.
.
.
commit
|
commitdiff
|
tree
2020-10-20
Yannick Moy
[Ad
a
] Fix com
m
ents as vo
l
atility propert
i
es can apply
.
.
.
commit
|
commitdiff
|
tree
2020-10-20
Yannick Moy
[A
d
a]
D
isplay so
u
r
c
e c
o
de
p
o
inti
n
g at
l
o
c
atio
n
s in
.
.
.
commit
|
commitdiff
|
tree
2020-10-19
Yannick Moy
[Ada] Alter
n
ati
v
e d
i
splay of m
u
lti-line mess
a
ges fo
r
.
.
.
commit
|
commitdiff
|
tree
2020-10-19
Yanni
c
k Moy
[Ada] Reject use
o
f Relaxed_Initi
a
liza
t
i
on on scalar
.
.
.
commit
|
commitdiff
|
tree
2020-10-19
Ya
n
nick Moy
[Ada] Clarify protec
t
ion offer
e
d by pr
e
condit
i
ons on
.
.
.
commit
|
commitdiff
|
tree
2020-10-19
Yannic
k
Moy
[Ada] Clari
f
y cu
r
r
ent design of Errout wrt globa
l
variable
.
.
.
commit
|
commitdiff
|
tree
2020-10-16
Ya
n
nick Moy
[A
d
a
] SPARK: up
d
ate for effectively vo
l
atile
ty
p
es
.
.
.
commit
|
commitdiff
|
tree
2020-07-15
Y
a
nnick Moy
[A
d
a] Mark standard containers as
n
ot in SPARK
commit
|
commitdiff
|
tree
next