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 exception raised on invalid contract in generic package
2023-06-13
Yannick Moy
ad
a
: Mark
a
ttribu
t
e Initialized as ghost code
commit
|
commitdiff
|
tree
2023-06-13
Yan
n
ick Mo
y
ada: Use ghost predicate in standar
d
library
commit
|
commitdiff
|
tree
2023-06-13
Yannick Moy
ada: Support new GN
A
T-specific aspect Ghost_Predicate
commit
|
commitdiff
|
tree
2023-05-29
Yan
n
ick M
o
y
ada:
R
estore S
P
A
RK
_
M
ode On fo
r
n
u
mer
i
ca
l
funct
i
ons
commit
|
commitdiff
|
tree
2023-05-26
Y
a
nnick
M
oy
a
d
a: Defa
u
l
t
initi
a
l
i
ze
e
ntity to avoid C
o
d
eP
e
e
r mes
s
age
commit
|
commitdiff
|
tree
2023-05-26
Yannick Moy
ada: Mi
n
or doc clarifi
c
ati
o
n
commit
|
commitdiff
|
tree
2023-05-26
Yannic
k
Moy
ada: Com
p
lete contracts of SPARK units
commit
|
commitdiff
|
tree
2023-05-23
Yannick Moy
ad
a
: Add d
e
faul
t
va
l
ue at initializatio
n
for CodePeer
commit
|
commitdiff
|
tree
2023-05-23
Yannick Moy
ada
:
Faci
l
itate p
r
oof o
f
Interfaces
.
C
.
To_Ada
commit
|
commitdiff
|
tree
2023-05-16
Yann
i
ck Mo
y
ada
:
Updat
e
proof of runtime unit
s
commit
|
commitdiff
|
tree
2023-05-16
Yan
n
ick
M
oy
ada:
Sim
p
lif
y
d
r
amatically ghost
c
ode for
p
roof of
.
.
.
commit
|
commitdiff
|
tree
2023-05-16
Yan
n
ic
k
M
o
y
a
d
a: Add intermediate assertions for
p
r
oof
of Su
p
er_Ta
i
l
commit
|
commitdiff
|
tree
2023-05-16
Yannick Moy
ad
a
: Set Loop_Varia
n
t assertion
policy to Ignore in
.
.
.
commit
|
commitdiff
|
tree
2023-05-16
Y
a
nnick Moy
ada: Resto
r
e proof of S
y
stem
.
Arith
_
D
o
uble
commit
|
commitdiff
|
tree
2023-05-15
Yannick
M
oy
a
da:
A
dd
a
nnotations
f
or pr
o
of of termination of runtime
.
.
.
commit
|
commitdiff
|
tree
2023-05-15
Yanni
c
k
M
o
y
ada: Re
c
ov
e
r proof of r
u
nti
m
e
units
commit
|
commitdiff
|
tree
2023-05-15
Yannick Moy
ad
a
: Recover proof of
I
nt
e
rfaces
.
C
for termination
commit
|
commitdiff
|
tree
2023-05-15
Yannick Moy
ada: Updat
e
com
m
ent
a
f
t
er S
P
ARK RM
change
commit
|
commitdiff
|
tree
2023-05-15
Yann
i
ck Moy
ada:
Fix ha
n
dling of pragm
a
Wa
r
nings
(Toolname, Off/On)
commit
|
commitdiff
|
tree
2023-05-15
Yannick Moy
a
d
a: Allow
pragmas An
n
otate between loop pragmas
commit
|
commitdiff
|
tree
2022-12-06
Yannic
k
Moy
ada:
Allow No_Cac
h
ing on
v
olatile t
y
pes
commit
|
commitdiff
|
tree
2022-11-28
Yann
i
ck Moy
ada: Implement c
h
ange
t
o SPARK RM rul
e
on state refinement
commit
|
commitdiff
|
tree
2022-11-14
Yan
n
ick M
o
y
ad
a
: Fix error on SPARK_Mode on library
-
lev
e
l separate
.
.
.
commit
|
commitdiff
|
tree
2022-11-14
Yannick Moy
ada: Impro
v
e
l
oc
a
tion of error
m
es
s
a
ges in
i
nstant
i
ations
commit
|
commitdiff
|
tree
2022-10-06
Yannick
M
o
y
ada:
Do not i
s
sue compiler warnings in
GNATprove mode
commit
|
commitdiff
|
tree
2022-09-12
Yannick Moy
[Ada
]
Jus
t
i
f
y false alarm from CodeP
e
er analysis
o
f
.
.
.
commit
|
commitdiff
|
tree
2022-09-12
Yannick Moy
[Ada] Accept e
x
plici
t
S
P
A
RK_Mode Auto as configuration
.
.
.
commit
|
commitdiff
|
tree
2022-09-12
Yannick
M
oy
[Ada] Reject use in SPARK of Asm intrinsics for code
.
.
.
commit
|
commitdiff
|
tree
2022-09-02
Yanni
c
k Moy
[Ada] Recover
p
r
o
of of Scaled_
D
ivid
e
in S
y
ste
m
.
Arith_64
commit
|
commitdiff
|
tree
2022-07-13
Y
an
n
ick Moy
[Ada] Fix incorrect handling of
G
host aspect
commit
|
commitdiff
|
tree
2022-07-13
Yan
n
ick
Moy
[Ada]
F
ix proof of r
u
n
t
ime u
n
it Syst
e
m
.
Ar
i
th_
6
4
commit
|
commitdiff
|
tree
2022-07-13
Y
a
n
nick Moy
[Ada]
F
i
x automa
t
ic pro
o
f
o
n S
y
stem
.
Ari
t
h_3
2
commit
|
commitdiff
|
tree
2022-07-12
Yannick Moy
[
A
da] Ig
n
ore
switch
e
s fo
r
cont
r
olling frontend warn
i
ngs
.
.
.
commit
|
commitdiff
|
tree
2022-07-06
Yannick Mo
y
[
A
da] Def
e
r
red constant considered as not preelabora
b
l
e
commit
|
commitdiff
|
tree
2022-07-06
Ya
n
nick Moy
[Ada] Support ghost generic forma
l
parameters
commit
|
commitdiff
|
tree
2022-07-05
Yanni
c
k
Moy
[Ada]
F
ix sp
u
riou
s
error on object renaming wit
h
ghos
t
.
.
.
commit
|
commitdiff
|
tree
2022-07-05
Yannick Moy
[Ada]
Spurio
u
s error on qu
a
li
f
ied prefix in P
a
ck
.
F
u
nc
.
.
.
commit
|
commitdiff
|
tree
2022-06-02
Yanni
c
k
M
oy
[Ada] Fix spuriou
s
errors on
g
host code
i
n generics
commit
|
commitdiff
|
tree
2022-06-02
Yanni
c
k
Moy
[A
d
a]
Issue errors on wrong co
n
text for ghost entiti
e
s
commit
|
commitdiff
|
tree
2022-06-02
Yannick Moy
[Ada]
Removal o
f
dead code Analyze_L
a
bel_Entity
commit
|
commitdiff
|
tree
2022-06-01
Yannick Moy
[Ada] Allow confirming volatil
e
prop
e
rties on N
o
_Caching
.
.
.
commit
|
commitdiff
|
tree
2022-06-01
Y
a
nnick Moy
[Ada] Fix class
i
f
ication of Subp
r
o
g
ram_Variant as
a
s
se
r
tion
.
.
.
commit
|
commitdiff
|
tree
2022-06-01
Yannick Moy
[Ada] Issu
e
a w
a
rning on entity hidden
in use_clause
.
.
.
commit
|
commitdiff
|
tree
2022-06-01
Yannick Moy
[Ada]
I
ssue bett
e
r error
m
essage
f
or out-
o
f
-
o
rder keywords
.
.
.
commit
|
commitdiff
|
tree
2022-05-30
Yanni
c
k Moy
[
Ada] Up
d
ate
p
roofs of d
o
u
bl
e
arith
m
e
t
ic unit aft
e
r
.
.
.
commit
|
commitdiff
|
tree
2022-05-30
Ya
n
nick Moy
[Ada] Adapt proof
of
r
untime unit s-arit32
commit
|
commitdiff
|
tree
2022-05-30
Y
a
nnick Moy
[Ada] PR a
d
a/1
0
5303 Fix use
o
f
A
ssertion_
P
olicy in
.
.
.
commit
|
commitdiff
|
tree
2022-05-19
Y
a
nnick
M
oy
[
A
da] F
u
rther adapt proof of dou
b
le
a
r
i
thme
t
ic runtime
.
.
.
commit
|
commitdiff
|
tree
2022-05-18
Yannic
k
Moy
[Ada] Adapt proof
o
f double arit
h
metic
r
u
ntime
u
n
i
t
commit
|
commitdiff
|
tree
2022-05-18
Yannick M
o
y
[Ad
a
] Fix
p
roof of runt
i
me
units
commit
|
commitdiff
|
tree
2022-05-18
Yanni
c
k Moy
[Ada]
S
purio
u
s err
o
r on fr
e
e
z
ing
o
f tag
g
e
d
t
y
pe
s
i
n
.
.
.
commit
|
commitdiff
|
tree
2022-05-17
Ya
n
nic
k
Moy
[Ada] A
l
l
o
w inlining for proof in
s
ide generics
commit
|
commitdiff
|
tree
2022-05-17
Yanni
c
k Moy
[A
d
a] Fix inserti
o
n of decl
a
ration
i
ns
i
de q
u
antified
.
.
.
commit
|
commitdiff
|
tree
2022-05-16
Yannic
k
Moy
[Ada] Fix proof of doub
l
e arithme
t
ic units
commit
|
commitdiff
|
tree
2022-05-16
Yannick Moy
[Ada] Update comment
j
ustifying non-inlin
i
ng for
p
roof
.
.
.
commit
|
commitdiff
|
tree
2022-05-13
Yannick
M
oy
[Ad
a
] Simplify
hel
p
er units fo
r
formal hashed sets
.
.
.
commit
|
commitdiff
|
tree
2022-05-13
Yannick
Moy
[Ada] Adapt body of
f
o
rmal sets and maps for SPARK
commit
|
commitdiff
|
tree
2022-05-13
Yannick Moy
[Ada] Remove de
p
ende
n
c
y on tam
p
ering checks and controlled
.
.
.
commit
|
commitdiff
|
tree
2022-05-13
Y
annick Moy
[A
d
a] Facilitate proof of
Ov
e
rwrite in
bounded strings
.
.
.
commit
|
commitdiff
|
tree
2022-05-12
Yannick Moy
[Ada] Remove usel
e
ss
pragma War
n
ings Of
f
f
ro
m
runtime
.
.
.
commit
|
commitdiff
|
tree
2022-05-12
Yannick
Moy
[Ada] Do no
t
iss
u
e a war
n
i
ng on
a
p
o
stcondition of
.
.
.
commit
|
commitdiff
|
tree
2022-05-12
Yannick Moy
[
A
da]
A
dd ghost code
t
o fa
c
ili
t
a
t
e proof w
i
th SPARK
commit
|
commitdiff
|
tree
2022-05-12
Y
annick Moy
[Ada] Remove use of use-clause
s
in loaded runtime units
commit
|
commitdiff
|
tree
2022-05-12
Yannick Moy
[Ada] Ada
p
t Co
d
ePeer analysis
o
f GNAT to changes in
.
.
.
commit
|
commitdiff
|
tree
2022-05-12
Yannick Moy
[Ada] Proof of '
I
mage support for
s
igned in
t
egers
commit
|
commitdiff
|
tree
2022-05-11
Yan
n
ick Moy
[Ada
]
Proof of 'Image su
p
por
t
for unsigned
int
e
gers
commit
|
commitdiff
|
tree
2022-05-11
Yannick Mo
y
[Ad
a
]
A
dapt pro
o
f of System
.
Arith_
D
ouble af
t
er up
d
ate
.
.
.
commit
|
commitdiff
|
tree
2022-05-10
Yannick Mo
y
[Ada]
Fix indentation to follow uniform styl
e
acr
o
ss
.
.
.
commit
|
commitdiff
|
tree
2022-05-09
Yannick Moy
[Ada] Suggest use o
f
First_Valid/Las
t
_Valid on type
.
.
.
commit
|
commitdiff
|
tree
2022-05-09
Yannick Moy
[Ada]
S
et Error_Msg_Warn before use
o
f << insertion
commit
|
commitdiff
|
tree
2022-01-11
Yannick
Moy
[Ada] Ada
p
t
proof of
S
ystem
.
Arith_Do
u
ble
commit
|
commitdiff
|
tree
2022-01-11
Yan
n
i
c
k Moy
[
A
da] Recover proof
of
A
da
.
Strings
.
Fi
x
e
d
wit
h
assertions
commit
|
commitdiff
|
tree
2022-01-11
Yannick Moy
[
A
da] Proof
o
f
unit Syst
e
m
.
Case_Ut
i
l
commit
|
commitdiff
|
tree
2022-01-11
Y
a
n
n
i
ck
M
oy
[Ada
]
Adapt gh
o
st code to
maintai
n
proof
commit
|
commitdiff
|
tree
2022-01-11
Yannick Moy
[A
d
a] Pro
o
f
of Sys
t
em
.
Ve
c
tors
.
Boolean_Operations
commit
|
commitdiff
|
tree
2022-01-06
Yannick Moy
[Ada] Proof of S
y
st
e
m
.
Generic_Array_Ope
r
ation
s
at si
l
ver
.
.
.
commit
|
commitdiff
|
tree
2022-01-06
Ya
n
nick Moy
[Ada] Justify fals
e
posit
i
ve message
from CodePeer
.
.
.
commit
|
commitdiff
|
tree
2022-01-06
Yann
i
ck
M
oy
[
Ada] Proof of
ru
n
time unit for n
o
n-b
i
nary mod
u
lar
.
.
.
commit
|
commitdiff
|
tree
2022-01-06
Y
a
n
nic
k
M
oy
[Ada] Proof of runtime units for binary modular exponent
i
ation
commit
|
commitdiff
|
tree
2022-01-05
Y
a
nnick Moy
[Ada]
A
dd contracts for the p
r
oof of System
.
A
r
it
h
_128
commit
|
commitdiff
|
tree
2022-01-05
Yannic
k
Moy
[Ada] Proof
of r
u
ntime
unit
s
for int
e
ger expone
n
ti
a
tion
.
.
.
commit
|
commitdiff
|
tree
2022-01-05
Yannick Moy
[Ada] Proof of runtime
units for integer e
x
ponen
t
i
a
tion
.
.
.
commit
|
commitdiff
|
tree
2022-01-05
Yannic
k
Moy
[Ada] Ren
a
me pa
r
ame
t
er-dependent cons
t
an
t
s i
n
gener
i
c
.
.
.
commit
|
commitdiff
|
tree
2022-01-05
Yannick Moy
[Ada] Fix
lemma in gen
e
ric uni
t
Sy
s
tem
.
Arith_Double
commit
|
commitdiff
|
tree
2021-12-02
Yannick
Moy
[Ad
a
] Proof of
Sy
s
tem
.
Arith
_
32 for double arithmetic
.
.
.
commit
|
commitdiff
|
tree
2021-12-02
Yannick
M
oy
[Ada] Amend
pro
o
f
of System
.
A
r
ith_Double to remo
v
e
.
.
.
commit
|
commitdiff
|
tree
2021-12-02
Yannick Moy
[Ada]
A
dd
pragma Annotate for
C
odeP
e
er
a
n
alysis
commit
|
commitdiff
|
tree
2021-12-02
Yann
i
ck M
o
y
[Ada
]
Pro
o
f o
f
support un
i
ts fo
r
'Width on signed integers
commit
|
commitdiff
|
tree
2021-12-02
Y
a
nnick Moy
[A
d
a] Proo
f
of Interfac
e
s
.
C with SPA
R
K
commit
|
commitdiff
|
tree
2021-12-02
Yan
n
ick Moy
[Ada] Proof of System
.
Val
_
Util u
t
iliti
e
s for 'Value
.
.
.
commit
|
commitdiff
|
tree
2021-12-02
Ya
n
nick Moy
[Ada
]
Pr
o
of of B
o
olea
n
'Ima
g
e
a
nd Boolean'Value
commit
|
commitdiff
|
tree
2021-12-01
Y
annick Moy
[Ada] Impr
o
ve
er
r
o
r mess
a
ges for dot notation
w
hen
.
.
.
commit
|
commitdiff
|
tree
2021-12-01
Yannick Moy
[Ada] Add
qu
e
ry for
extended precisio
n
floating-point
.
.
.
commit
|
commitdiff
|
tree
2021-12-01
Yan
n
i
c
k Moy
[Ada] Improve
messages on inco
r
rect state refinement
.
.
.
commit
|
commitdiff
|
tree
2021-11-10
Yannick Mo
y
[A
d
a
] Cre
a
te exp
l
i
cit
gh
o
st mi
r
ror unit
f
o
r big inte
g
ers
commit
|
commitdiff
|
tree
2021-11-10
Yannick
Moy
[Ad
a
]
B
etter error message on mi
s
sing parentheses
commit
|
commitdiff
|
tree
2021-11-09
Yannick M
o
y
[Ada]
C
o
mp
l
e
t
e support for prefixed cal
l
on sub
t
y
pes
.
.
.
commit
|
commitdiff
|
tree
2021-11-09
Yannick M
o
y
[Ada] Fix support
f
or
prefix
e
d cal
l
with
incompl
e
te
.
.
.
commit
|
commitdiff
|
tree
2021-10-25
Yannic
k
M
o
y
[Ada] Issue error on invali
d
use of Ghost insi
d
e
pragma
.
.
.
commit
|
commitdiff
|
tree
2021-10-20
Y
a
n
ni
c
k Moy
[Ad
a
] Proof
o
f
the runt
i
me support for attribute 'Width
commit
|
commitdiff
|
tree
next