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 wrong expansion of array aggregate with noncontiguous choices
2023-05-29
Yannick M
o
y
ada: Restore SPARK_Mode On for nume
r
ica
l
fun
c
tions
commit
|
commitdiff
|
tree
2023-05-26
Y
annick Moy
ada: Defa
u
lt initi
a
l
i
ze
en
t
ity to avoid Code
P
eer message
commit
|
commitdiff
|
tree
2023-05-26
Yannick Moy
ada: Minor do
c
cla
r
ification
commit
|
commitdiff
|
tree
2023-05-26
Y
a
nnick Moy
ada: Com
p
l
e
t
e
con
t
r
a
cts
of SPARK units
commit
|
commitdiff
|
tree
2023-05-23
Yanni
c
k Moy
ada:
A
d
d default val
u
e
at initializatio
n
for
C
ode
P
eer
commit
|
commitdiff
|
tree
2023-05-23
Yannick Moy
ada: Facilitate proof of Interfaces
.
C
.
To_Ada
commit
|
commitdiff
|
tree
2023-05-16
Yannick M
o
y
a
d
a: Update p
r
oo
f
of runtime units
commit
|
commitdiff
|
tree
2023-05-16
Y
a
nni
c
k Moy
ada
:
Simplify d
r
amatically ghost code f
o
r proof
of
.
.
.
commit
|
commitdiff
|
tree
2023-05-16
Yannick Moy
a
da: Add inter
m
ediat
e
asserti
o
ns f
o
r proof of Super_Tail
commit
|
commitdiff
|
tree
2023-05-16
Yan
n
ick Moy
ada: Set L
o
op_Variant
a
ssertion policy to Ignor
e
in
.
.
.
commit
|
commitdiff
|
tree
2023-05-16
Yannick Moy
a
da: Restor
e
proof
of Sys
t
em
.
Arith
_
Double
commit
|
commitdiff
|
tree
2023-05-15
Yannick M
o
y
ada: Add
a
nnot
a
t
ions
for pr
o
o
f of termination of
r
untime
.
.
.
commit
|
commitdiff
|
tree
2023-05-15
Y
annick Moy
ada
:
R
e
cove
r
proof of runtime
u
ni
t
s
commit
|
commitdiff
|
tree
2023-05-15
Yannick
M
oy
ada: Recover
p
roof of
Interfa
c
es
.
C
for termination
commit
|
commitdiff
|
tree
2023-05-15
Y
a
nnick Moy
ada: Update
co
m
ment after
S
PARK RM ch
a
nge
commit
|
commitdiff
|
tree
2023-05-15
Yan
n
ick
Moy
ada: Fix handling of pragma Warning
s
(To
o
l
n
ame,
O
ff/On)
commit
|
commitdiff
|
tree
2023-05-15
Yanni
c
k Moy
ada:
Allow pragma
s
Annotate between loop pragmas
commit
|
commitdiff
|
tree
2022-12-06
Yannick Moy
a
da:
A
l
l
ow No_Cach
i
ng on volatile types
commit
|
commitdiff
|
tree
2022-11-28
Ya
n
nick Moy
ada: Implem
e
nt change to SPARK RM rule on state refine
m
ent
commit
|
commitdiff
|
tree
2022-11-14
Yannick Moy
ada: Fix e
r
ror on
SPARK_Mode
o
n lib
r
ary-le
v
e
l
separate
.
.
.
commit
|
commitdiff
|
tree
2022-11-14
Yannick Mo
y
a
da: Improve location of error me
s
sag
e
s in
instantiat
i
ons
commit
|
commitdiff
|
tree
2022-10-06
Yann
i
ck
M
oy
ada: Do not issue
c
o
mpiler
warnin
g
s
i
n GN
A
T
prove mode
commit
|
commitdiff
|
tree
2022-09-12
Y
a
nnick
Moy
[Ada] Justify false alarm from Code
P
eer analysi
s
of
.
.
.
commit
|
commitdiff
|
tree
2022-09-12
Yannick M
o
y
[Ada] A
c
cept explicit
S
PARK_Mod
e
Auto as configuration
.
.
.
commit
|
commitdiff
|
tree
2022-09-12
Yan
n
ick Moy
[Ada]
R
eject u
s
e in SPARK of
A
s
m
i
ntrinsics
f
o
r
code
.
.
.
commit
|
commitdiff
|
tree
2022-09-02
Yannick
M
oy
[Ada] Recover proof o
f
S
c
aled_
D
ivid
e
in Sys
t
em
.
A
r
i
t
h_64
commit
|
commitdiff
|
tree
2022-07-13
Yannick
M
oy
[Ada] F
i
x incorre
c
t
h
a
ndling of
Ghost aspect
commit
|
commitdiff
|
tree
2022-07-13
Yannic
k
Moy
[Ada] Fix proof of runtime unit
Syst
e
m
.
Arith_64
commit
|
commitdiff
|
tree
2022-07-13
Yannick Moy
[
Ada] F
i
x automatic proo
f
on
System
.
Arith
_
32
commit
|
commitdiff
|
tree
2022-07-12
Y
a
nn
i
ck Moy
[Ada] Ign
o
re
switches for controlling fronte
n
d wa
r
nings
.
.
.
commit
|
commitdiff
|
tree
2022-07-06
Yannick Moy
[Ada] Deferred
cons
t
ant considered as not preelabo
r
able
commit
|
commitdiff
|
tree
2022-07-06
Yannick
Moy
[Ada]
Supp
o
r
t g
h
ost gen
e
ric fo
r
mal parameters
commit
|
commitdiff
|
tree
2022-07-05
Yann
i
ck Moy
[Ada]
F
i
x spur
i
ous error on obje
c
t renaming with g
h
ost
.
.
.
commit
|
commitdiff
|
tree
2022-07-05
Ya
n
nick
Moy
[Ada] Spurious error on
quali
f
ied prefix in Pack
.
F
u
nc
.
.
.
commit
|
commitdiff
|
tree
2022-06-02
Y
a
n
ni
c
k M
o
y
[Ada] Fix spurious errors on gh
o
s
t co
d
e in g
e
ner
i
cs
commit
|
commitdiff
|
tree
2022-06-02
Yannick Moy
[Ada] I
s
sue errors on wron
g
con
t
ext
f
o
r ghost en
t
iti
e
s
commit
|
commitdiff
|
tree
2022-06-02
Y
a
nnick Moy
[Ada]
Removal of
d
ead code Ana
l
yze_
L
abel_Entity
commit
|
commitdiff
|
tree
2022-06-01
Y
an
n
ick
M
oy
[Ada] Al
l
o
w
c
onfirming volatile
properti
e
s on
N
o_Caching
.
.
.
commit
|
commitdiff
|
tree
2022-06-01
Yannick M
o
y
[Ad
a
] Fi
x
classific
a
tion of Subprogram
_
Var
i
a
nt as asse
r
tion
.
.
.
commit
|
commitdiff
|
tree
2022-06-01
Yannic
k
M
o
y
[Ada] Issue a warning on entit
y
hi
d
den in us
e
_clause
.
.
.
commit
|
commitdiff
|
tree
2022-06-01
Yannick
M
oy
[Ada] Issue better error message for
out-of-order
k
e
ywords
.
.
.
commit
|
commitdiff
|
tree
2022-05-30
Yannick Moy
[Ada]
Update proofs of doubl
e
arithmetic unit after
.
.
.
commit
|
commitdiff
|
tree
2022-05-30
Yanni
c
k Moy
[Ada]
A
dap
t
pr
o
of of runtim
e
unit s-arit32
commit
|
commitdiff
|
tree
2022-05-30
Yannick Mo
y
[Ada]
P
R ad
a
/10
5
3
03 F
i
x
u
s
e
of Assertion_Polic
y
in
.
.
.
commit
|
commitdiff
|
tree
2022-05-19
Yannick Moy
[
A
da] Furthe
r
adapt proo
f
o
f
doubl
e
a
rithmetic runtime
.
.
.
commit
|
commitdiff
|
tree
2022-05-18
Yannick Moy
[Ada
]
Adapt p
r
oof of
dou
b
le
a
rithmetic runtime unit
commit
|
commitdiff
|
tree
2022-05-18
Yan
n
ic
k
Moy
[Ada] Fix
p
roof
o
f
runtime
u
nits
commit
|
commitdiff
|
tree
2022-05-18
Yannick Moy
[Ada] S
p
urious er
r
or on freezing of t
a
gged types in
.
.
.
commit
|
commitdiff
|
tree
2022-05-17
Y
a
n
nick
M
o
y
[Ada] Allow inl
i
ning f
o
r proof insid
e
g
e
nerics
commit
|
commitdiff
|
tree
2022-05-17
Y
a
nnick M
o
y
[
Ada]
Fix i
n
sertion
of decla
r
ation inside qua
n
tified
.
.
.
commit
|
commitdiff
|
tree
2022-05-16
Yannick Moy
[
A
da]
F
i
x proof of double
arithmetic uni
t
s
commit
|
commitdiff
|
tree
2022-05-16
Y
a
nn
i
ck
Moy
[Ada] Update c
o
mment ju
s
tifyin
g
non-inlining for pr
o
o
f
.
.
.
commit
|
commitdiff
|
tree
2022-05-13
Ya
n
nick
M
oy
[Ada] Simplify helper units for formal ha
s
h
e
d
s
e
t
s
.
.
.
commit
|
commitdiff
|
tree
2022-05-13
Yannick Moy
[Ada] Adapt bo
d
y of form
a
l sets and maps
f
or SPARK
commit
|
commitdiff
|
tree
2022-05-13
Y
a
nnick
M
oy
[Ada
]
Remo
v
e dependency
on
t
ampering chec
k
s
a
nd c
o
nt
r
olled
.
.
.
commit
|
commitdiff
|
tree
2022-05-13
Yanni
c
k Moy
[Ada
]
Fac
i
litate
pr
o
o
f of Over
w
rite
in bou
n
d
e
d strings
.
.
.
commit
|
commitdiff
|
tree
2022-05-12
Ya
n
n
ick Moy
[Ada] Rem
o
v
e useless
pragma Warnin
g
s
Off fr
o
m runtime
.
.
.
commit
|
commitdiff
|
tree
2022-05-12
Yannick Moy
[Ada] Do not i
s
sue a w
a
rni
n
g
o
n
a
postco
n
dition of
.
.
.
commit
|
commitdiff
|
tree
2022-05-12
Yannick Moy
[
A
da] Add ghos
t
code to f
a
cilitate
proof with
S
P
ARK
commit
|
commitdiff
|
tree
2022-05-12
Yannick M
o
y
[Ada]
R
e
m
ove u
s
e of
u
se-cl
a
u
s
es in loa
d
e
d
runtime units
commit
|
commitdiff
|
tree
2022-05-12
Yannic
k
Moy
[Ada] Adap
t
C
o
dePee
r
an
a
ly
s
is
of GNAT to changes i
n
.
.
.
commit
|
commitdiff
|
tree
2022-05-12
Yannick Moy
[Ad
a
]
Proof of 'I
m
age support
for
s
i
gned integer
s
commit
|
commitdiff
|
tree
2022-05-11
Ya
n
nic
k
M
o
y
[Ada
]
Proof of 'Image support for unsigned in
t
egers
commit
|
commitdiff
|
tree
2022-05-11
Yannick Moy
[Ada] A
d
ap
t
pro
o
f of System
.
Ari
t
h
_Double after upda
t
e
.
.
.
commit
|
commitdiff
|
tree
2022-05-10
Yan
n
ick Moy
[Ad
a
]
Fix indenta
t
ion to follow u
n
iform style across
.
.
.
commit
|
commitdiff
|
tree
2022-05-09
Yann
i
ck Moy
[
A
da] Sugg
e
st use of
F
irst_Valid/Last_
V
a
lid
o
n typ
e
.
.
.
commit
|
commitdiff
|
tree
2022-05-09
Yannick Moy
[Ada] Set Error_Msg_
W
arn before use of <<
i
nse
r
tion
commit
|
commitdiff
|
tree
2022-01-11
Yannick Moy
[
Ada] Adapt proof of Syste
m
.
Arith_Doub
l
e
commit
|
commitdiff
|
tree
2022-01-11
Ya
n
nick Moy
[Ada
]
Recover proof o
f
Ada
.
String
s
.
Fixed w
i
th assert
i
ons
commit
|
commitdiff
|
tree
2022-01-11
Ya
n
ni
c
k
M
oy
[Ada] Proof of unit
S
ystem
.
Cas
e
_Util
commit
|
commitdiff
|
tree
2022-01-11
Yannick Moy
[A
d
a] Adapt ghost code to maint
a
in proof
commit
|
commitdiff
|
tree
2022-01-11
Y
ann
i
ck Moy
[
Ada]
P
r
o
of of System
.
Vectors
.
Boo
l
e
an_
O
p
e
r
atio
n
s
commit
|
commitdiff
|
tree
2022-01-06
Yanni
c
k Moy
[
A
d
a] Proof of System
.
Generi
c
_
Array_Opera
t
ions at silver
.
.
.
commit
|
commitdiff
|
tree
2022-01-06
Ya
n
nick Moy
[Ada] Justify f
a
lse posi
t
ive message from CodePeer
.
.
.
commit
|
commitdiff
|
tree
2022-01-06
Y
a
n
n
i
ck Moy
[Ada] Proof of runtime unit for non-binary modular
.
.
.
commit
|
commitdiff
|
tree
2022-01-06
Yannick Mo
y
[Ada] Pr
o
of of
r
u
n
time units for binary modular ex
p
onentiation
commit
|
commitdiff
|
tree
2022-01-05
Yannick M
o
y
[Ad
a
]
Add
contracts f
o
r the pr
o
of of
S
y
s
t
e
m
.
Arith_128
commit
|
commitdiff
|
tree
2022-01-05
Yannick Moy
[Ada] Proof of ru
n
ti
m
e units fo
r
integer exponentiat
i
on
.
.
.
commit
|
commitdiff
|
tree
2022-01-05
Y
annick Moy
[
Ada] Proof of runtime units f
o
r
integer e
x
ponentiation
.
.
.
commit
|
commitdiff
|
tree
2022-01-05
Yannick Mo
y
[Ada] Rename paramet
e
r-dependen
t
c
onstants i
n
generic
.
.
.
commit
|
commitdiff
|
tree
2022-01-05
Yan
n
ick Moy
[Ada] Fix
l
emma i
n
gen
e
r
ic unit S
y
s
t
e
m
.
Arith_Doub
l
e
commit
|
commitdiff
|
tree
2021-12-02
Yannick Moy
[Ada] P
r
oo
f
of
S
ystem
.
Ar
i
th_32 for double
arithmetic
.
.
.
commit
|
commitdiff
|
tree
2021-12-02
Y
a
nnick Moy
[Ada] Amend
p
r
o
o
f
o
f S
y
stem
.
A
r
i
th_Double to rem
o
ve
.
.
.
commit
|
commitdiff
|
tree
2021-12-02
Yanni
c
k Moy
[Ada] Add pragma Annotate for CodePeer analysis
commit
|
commitdiff
|
tree
2021-12-02
Yannick Moy
[Ada] Proof of support units
f
or
'Width
o
n
signed i
n
tegers
commit
|
commitdiff
|
tree
2021-12-02
Y
an
n
ick Mo
y
[Ada] Pr
o
of of Interfaces
.
C with SPARK
commit
|
commitdiff
|
tree
2021-12-02
Y
a
nnick Moy
[
A
d
a
] Proof of
System
.
Val_Util ut
i
l
ities for 'Value
.
.
.
commit
|
commitdiff
|
tree
2021-12-02
Ya
n
nick Moy
[
Ada] Proof of Boolean'I
m
age
a
nd B
o
olean'Value
commit
|
commitdiff
|
tree
2021-12-01
Yannick Mo
y
[Ada]
I
mprove error m
e
ss
a
g
e
s fo
r
dot notatio
n
when
.
.
.
commit
|
commitdiff
|
tree
2021-12-01
Yannick Moy
[Ada] A
d
d
qu
e
ry for
extend
e
d precisi
o
n f
l
o
ati
n
g-point
.
.
.
commit
|
commitdiff
|
tree
2021-12-01
Yann
i
ck Moy
[Ad
a
]
I
mprove messages on incorrect state
r
efinem
e
n
t
.
.
.
commit
|
commitdiff
|
tree
2021-11-10
Ya
n
nick Moy
[Ada] Crea
t
e explicit ghost mi
r
ror unit
f
o
r
b
i
g integers
commit
|
commitdiff
|
tree
2021-11-10
Yannick
M
oy
[Ada] Better error messag
e
on missin
g
pa
r
entheses
commit
|
commitdiff
|
tree
2021-11-09
Y
a
nnick Mo
y
[A
d
a] Complete support
f
or prefixed call
on s
u
btypes
.
.
.
commit
|
commitdiff
|
tree
2021-11-09
Yannick Moy
[Ada] Fix support for p
r
ef
i
xed call with i
n
complete
.
.
.
commit
|
commitdiff
|
tree
2021-10-25
Y
annick
M
oy
[Ada] Issue error
on invalid use of
Ghost inside p
r
agma
.
.
.
commit
|
commitdiff
|
tree
2021-10-20
Y
annick Mo
y
[Ada] Proof of the ru
n
tim
e
support for attribute 'Width
commit
|
commitdiff
|
tree
2021-10-20
Yannick Moy
[Ada]
P
rovide d
u
mm
y
body for
big int
e
gers
l
ibrary used
.
.
.
commit
|
commitdiff
|
tree
2021-10-20
Ya
n
nick Moy
[
A
da] I
s
s
u
e w
a
rnin
g
o
n
u
nused quanti
f
ied exp
r
ession
commit
|
commitdiff
|
tree
2021-10-05
Yannick Moy
[Ada] Improve
e
rror m
e
ssage on
a
rray aggrega
t
es
commit
|
commitdiff
|
tree
next