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: Add the ability to add error codes to error messages
2023-06-20
Yanni
c
k Moy
ada:
Ad
d
th
e
ability t
o
ad
d
error c
o
des t
o
error m
e
ssages
commit
|
commitdiff
|
tree
2023-06-20
Yannick Moy
ada
:
Update annotations in runtime
for proof
commit
|
commitdiff
|
tree
2023-06-15
Yannic
k
Mo
y
ada: Reject Loop
_
Entry inside p
r
efix of Loop_Entry
commit
|
commitdiff
|
tree
2023-06-13
Ya
n
nick Mo
y
ada: Mark
a
ttribu
t
e Initialized as gh
o
st cod
e
commit
|
commitdiff
|
tree
2023-06-13
Yan
n
ick Moy
a
d
a: Use
g
host pre
d
icate in s
t
andard library
commit
|
commitdiff
|
tree
2023-06-13
Yannick Moy
ada: Support new G
N
AT-specif
i
c aspect G
h
ost_Predi
c
ate
commit
|
commitdiff
|
tree
2023-05-29
Ya
n
nick Moy
ada:
Resto
r
e SPARK_Mode On fo
r
numerical fun
c
t
io
n
s
commit
|
commitdiff
|
tree
2023-05-26
Yan
n
ic
k
Mo
y
ada: Default in
i
t
i
alize ent
i
ty to
av
o
id CodePeer
m
essage
commit
|
commitdiff
|
tree
2023-05-26
Yanni
c
k
M
o
y
ada:
M
i
n
or
doc clarification
commit
|
commitdiff
|
tree
2023-05-26
Yannick
M
o
y
ad
a
: Complete contract
s
of SPARK u
n
its
commit
|
commitdiff
|
tree
2023-05-23
Yannick M
o
y
ada
:
A
d
d default
v
alue
a
t initialization for Cod
e
Pe
e
r
commit
|
commitdiff
|
tree
2023-05-23
Yannick Moy
a
da: Facilitat
e
proof of Interfa
c
es
.
C
.
T
o
_Ada
commit
|
commitdiff
|
tree
2023-05-16
Yann
i
c
k Moy
ada: Update
p
r
o
of
o
f ru
n
time units
commit
|
commitdiff
|
tree
2023-05-16
Yannick Moy
ada:
Simp
l
ify
d
r
a
matically ghos
t
code for proof of
.
.
.
commit
|
commitdiff
|
tree
2023-05-16
Yannick Mo
y
ada:
A
d
d
interm
e
diate assertions for proof of Super_Tail
commit
|
commitdiff
|
tree
2023-05-16
Ya
n
nick Moy
ada: Set Loop_Varian
t
asserti
o
n policy to
I
g
nore in
.
.
.
commit
|
commitdiff
|
tree
2023-05-16
Yannick Moy
ada: Restore proof
o
f System
.
A
rith
_
D
o
u
ble
commit
|
commitdiff
|
tree
2023-05-15
Yannick M
o
y
ada: Add annotatio
n
s for proof
o
f termina
t
ion o
f
r
untime
.
.
.
commit
|
commitdiff
|
tree
2023-05-15
Yannick Moy
ada: Recover proof of ru
n
time units
commit
|
commitdiff
|
tree
2023-05-15
Yannick M
o
y
ada: Recover p
r
o
o
f of Int
e
rfaces
.
C f
o
r termin
a
tio
n
commit
|
commitdiff
|
tree
2023-05-15
Yannick Mo
y
ada: Update
comment
a
f
ter SPARK R
M
change
commit
|
commitdiff
|
tree
2023-05-15
Ya
n
n
i
ck Moy
ada: Fix han
d
ling of pragma Warnings (Toolname, Off/On)
commit
|
commitdiff
|
tree
2023-05-15
Yannick Moy
ada: Allow p
r
agmas
Anno
t
ate between loop pragmas
commit
|
commitdiff
|
tree
2022-12-06
Yanni
c
k
Moy
ada: A
l
low No_Ca
c
hing on volat
i
le
types
commit
|
commitdiff
|
tree
2022-11-28
Ya
n
nick Moy
ada:
I
mpleme
n
t change to
SPARK
RM rule on state r
e
finement
commit
|
commitdiff
|
tree
2022-11-14
Yannick Moy
a
d
a: Fix
err
o
r
o
n
S
P
ARK_
M
ode on l
i
b
rary-level s
e
parate
.
.
.
commit
|
commitdiff
|
tree
2022-11-14
Yan
n
ick Moy
ada: I
m
prov
e
loca
t
ion
o
f error messages in instanti
a
tions
commit
|
commitdiff
|
tree
2022-10-06
Yannick Moy
ada: Do not is
s
ue compiler
warnings in GNATprove mode
commit
|
commitdiff
|
tree
2022-09-12
Yannick Moy
[Ada] Justify false alarm
f
rom CodePeer analysis
o
f
.
.
.
commit
|
commitdiff
|
tree
2022-09-12
Yannic
k
M
oy
[Ada] Acc
e
pt expli
c
it S
P
ARK_Mode
A
ut
o
a
s configuration
.
.
.
commit
|
commitdiff
|
tree
2022-09-12
Ya
n
nick M
o
y
[Ada] Re
j
ec
t
use in
SPARK of
Asm intr
i
nsics
f
or code
.
.
.
commit
|
commitdiff
|
tree
2022-09-02
Y
a
nnick Mo
y
[Ada] Recover proof of Scaled_Divide in System
.
Arith_64
commit
|
commitdiff
|
tree
2022-07-13
Yann
i
ck Moy
[A
d
a] Fix inco
r
rect handli
n
g o
f
Gh
o
st aspect
commit
|
commitdiff
|
tree
2022-07-13
Yannick
M
o
y
[
A
da] Fix pro
o
f
o
f r
u
ntime unit Syst
e
m
.
A
r
ith
_
64
commit
|
commitdiff
|
tree
2022-07-13
Yan
n
ic
k
M
o
y
[A
d
a] Fix automatic p
r
o
of on System
.
A
r
i
th_32
commit
|
commitdiff
|
tree
2022-07-12
Yannick Moy
[Ada] Ignore sw
i
t
c
hes for controlling fron
t
e
n
d
w
arnings
.
.
.
commit
|
commitdiff
|
tree
2022-07-06
Yannick
M
oy
[
A
da]
D
e
f
er
r
ed c
o
nstant c
o
nsidered as not preelabor
a
b
l
e
commit
|
commitdiff
|
tree
2022-07-06
Yanni
c
k Moy
[
Ad
a
]
S
upport
g
host generic
fo
r
mal parameter
s
commit
|
commitdiff
|
tree
2022-07-05
Y
a
nnick Moy
[Ada] Fix spurio
u
s erro
r
on ob
j
ec
t
r
enaming with g
h
ost
.
.
.
commit
|
commitdiff
|
tree
2022-07-05
Y
annick Moy
[
A
da] Spuriou
s
error
o
n qualified prefix in Pack
.
Func
.
.
.
commit
|
commitdiff
|
tree
2022-06-02
Yannick Moy
[
A
da]
F
ix spu
r
iou
s
e
r
r
ors o
n
ghos
t
code in generics
commit
|
commitdiff
|
tree
2022-06-02
Yannick Moy
[Ada] Issue errors
o
n wrong context for ghos
t
e
n
tities
commit
|
commitdiff
|
tree
2022-06-02
Y
annick
M
oy
[Ada]
R
emova
l
of dea
d
code Analyze_
L
abel_Entity
commit
|
commitdiff
|
tree
2022-06-01
Y
annick Moy
[Ad
a
] Allow conf
i
rming volatile pr
o
per
t
ies on No_Caching
.
.
.
commit
|
commitdiff
|
tree
2022-06-01
Yannick Moy
[Ada] Fix classification of
S
u
bpro
g
ram_Varian
t
as assertio
n
.
.
.
commit
|
commitdiff
|
tree
2022-06-01
Y
a
n
n
ick
Moy
[A
d
a] Is
s
ue a w
a
rnin
g
on entity hi
d
d
en in use_clau
s
e
.
.
.
commit
|
commitdiff
|
tree
2022-06-01
Ya
n
n
i
c
k Moy
[Ada
]
Issue better error me
s
sage f
o
r
o
ut-of-
o
r
d
er keywords
.
.
.
commit
|
commitdiff
|
tree
2022-05-30
Yannick
Moy
[Ada] Update proofs of double arithme
t
ic
u
nit aft
e
r
.
.
.
commit
|
commitdiff
|
tree
2022-05-30
Y
annick Moy
[Ada] Adapt pro
o
f of runt
i
me unit s
-
ari
t
3
2
commit
|
commitdiff
|
tree
2022-05-30
Yannick Moy
[
Ada] PR ada/10
5
303 Fix us
e
of Assert
i
on_Po
l
icy in
.
.
.
commit
|
commitdiff
|
tree
2022-05-19
Y
a
nnick Moy
[A
d
a] F
u
rt
h
er
a
da
p
t
pr
o
of of dou
b
le arithmetic runtime
.
.
.
commit
|
commitdiff
|
tree
2022-05-18
Yannick Mo
y
[Ada] Adapt proof of double arithmetic runtime unit
commit
|
commitdiff
|
tree
2022-05-18
Ya
n
n
ic
k
Moy
[A
d
a] Fix pro
o
f
of runti
m
e
units
commit
|
commitdiff
|
tree
2022-05-18
Yannick
M
oy
[
Ada] Spu
r
ious error on
f
reezing of t
a
gge
d
types in
.
.
.
commit
|
commitdiff
|
tree
2022-05-17
Y
annick Moy
[Ad
a
] Allow
inli
n
ing for
p
r
oof ins
i
de gener
i
cs
commit
|
commitdiff
|
tree
2022-05-17
Yannick Moy
[Ada] Fi
x
insertion of declara
t
ion inside qua
n
tified
.
.
.
commit
|
commitdiff
|
tree
2022-05-16
Yannick Moy
[Ad
a
] Fix
proof of doubl
e
ari
t
hmetic units
commit
|
commitdiff
|
tree
2022-05-16
Y
annick
M
oy
[Ada]
U
pdate comment justif
y
i
ng non-in
l
ining for proo
f
.
.
.
commit
|
commitdiff
|
tree
2022-05-13
Yannick Moy
[A
d
a] Simpl
i
fy help
e
r units
f
or formal hashed sets
.
.
.
commit
|
commitdiff
|
tree
2022-05-13
Yannick
Moy
[
Ada] Adapt
b
ody of formal sets a
n
d ma
p
s
for
S
PA
R
K
commit
|
commitdiff
|
tree
2022-05-13
Y
annick
M
oy
[A
d
a] Remove
dependency on tampe
r
ing c
h
e
cks and contro
l
l
e
d
.
.
.
commit
|
commitdiff
|
tree
2022-05-13
Yanni
c
k Moy
[A
d
a]
F
acilitate
proof of Ov
e
rwrite in bound
e
d strings
.
.
.
commit
|
commitdiff
|
tree
2022-05-12
Yann
i
ck Moy
[Ada] Remove useles
s
prag
m
a War
n
ings Of
f
f
r
om runtime
.
.
.
commit
|
commitdiff
|
tree
2022-05-12
Yanni
c
k
Moy
[Ada] D
o
not issue a warning on a post
c
ondi
t
io
n
o
f
.
.
.
commit
|
commitdiff
|
tree
2022-05-12
Yannick
M
oy
[Ad
a
] Ad
d
ghost code to
f
a
c
i
l
itate proof with
S
P
A
RK
commit
|
commitdiff
|
tree
2022-05-12
Yannick Moy
[Ada
]
Re
m
ove u
s
e of us
e
-c
l
auses in
loade
d
runtime units
commit
|
commitdiff
|
tree
2022-05-12
Yan
n
i
c
k Moy
[Ada
]
A
d
apt Co
d
ePee
r
a
n
alysis of GNAT to
changes in
.
.
.
commit
|
commitdiff
|
tree
2022-05-12
Y
an
n
i
ck Moy
[
Ada] Pro
o
f of '
I
mage support f
o
r signed int
e
gers
commit
|
commitdiff
|
tree
2022-05-11
Yan
n
ick Mo
y
[Ada] Pro
o
f of 'Im
a
ge support for un
s
ig
n
ed
integers
commit
|
commitdiff
|
tree
2022-05-11
Yannick
M
oy
[Ada] Adapt proof
o
f System
.
Arith_D
o
uble after upd
a
t
e
.
.
.
commit
|
commitdiff
|
tree
2022-05-10
Yannic
k
Moy
[Ada]
Fix indentation to fol
l
ow uniform style across
.
.
.
commit
|
commitdiff
|
tree
2022-05-09
Y
ann
i
c
k Moy
[A
d
a
] Suggest
u
se of First_Va
l
id/Last_Valid on type
.
.
.
commit
|
commitdiff
|
tree
2022-05-09
Yannick
M
oy
[A
d
a] S
e
t Error_Msg_Warn b
e
f
ore use of
<
<
in
s
ert
i
on
commit
|
commitdiff
|
tree
2022-01-11
Y
a
nnick Moy
[
Ada] Adap
t
proof of
System
.
Arith_Doub
l
e
commit
|
commitdiff
|
tree
2022-01-11
Ya
n
nick
M
oy
[Ada] Rec
o
ve
r
proof of Ada
.
S
trings
.
Fixed wit
h
a
s
sertions
commit
|
commitdiff
|
tree
2022-01-11
Yannick Moy
[Ada] Proof of unit System
.
C
ase_U
t
i
l
commit
|
commitdiff
|
tree
2022-01-11
Yannick Mo
y
[Ada
]
Ada
p
t ghost code to maint
a
in
proof
commit
|
commitdiff
|
tree
2022-01-11
Yannick Moy
[Ada] Proof
o
f System
.
V
e
ctors
.
Boolean_Operations
commit
|
commitdiff
|
tree
2022-01-06
Yannic
k
Moy
[A
d
a] Proof of
Syst
e
m
.
G
eneric_Array_Opera
t
ions at silver
.
.
.
commit
|
commitdiff
|
tree
2022-01-06
Yannick Moy
[
A
d
a] Justify
f
alse p
o
sitive mess
a
ge from CodePeer
.
.
.
commit
|
commitdiff
|
tree
2022-01-06
Yannick Moy
[Ada] Proof of ru
n
t
i
me unit for non-binary
m
odular
.
.
.
commit
|
commitdiff
|
tree
2022-01-06
Yannick
M
oy
[Ada
]
P
roof of r
u
nti
m
e un
i
ts for binar
y
modular
exponentiation
commit
|
commitdiff
|
tree
2022-01-05
Y
ann
i
ck Moy
[Ada] Add contracts for the
proof o
f
Syste
m
.
Ar
i
th_
1
28
commit
|
commitdiff
|
tree
2022-01-05
Yannick Moy
[Ad
a
]
P
roof of runtime u
n
its for
integer expone
n
ti
a
tion
.
.
.
commit
|
commitdiff
|
tree
2022-01-05
Y
annick Moy
[Ada] P
r
oof of r
u
ntim
e
units for
i
n
teger exponentiati
o
n
.
.
.
commit
|
commitdiff
|
tree
2022-01-05
Yannick Mo
y
[Ad
a
] Ren
a
me parameter-dependen
t
constants in generi
c
.
.
.
commit
|
commitdiff
|
tree
2022-01-05
Yannick Moy
[Ada] Fix lemma in generic unit System
.
Arith_
D
ouble
commit
|
commitdiff
|
tree
2021-12-02
Yannick Moy
[
A
da
]
Proof of System
.
Arith_3
2
for
d
o
u
b
le arithme
t
ic
.
.
.
commit
|
commitdiff
|
tree
2021-12-02
Yannick Moy
[Ada] Amend
proof
of
Sy
s
tem
.
Arith_Double to
r
e
move
.
.
.
commit
|
commitdiff
|
tree
2021-12-02
Yannick Moy
[Ada] Add
p
ragma Annotate for CodePeer
analysis
commit
|
commitdiff
|
tree
2021-12-02
Yannick M
o
y
[
Ada] Proof of s
u
p
port
units for 'Width on s
i
gned
in
t
egers
commit
|
commitdiff
|
tree
2021-12-02
Yan
n
ick Moy
[Ada]
Proof of Interfaces
.
C with SPARK
commit
|
commitdiff
|
tree
2021-12-02
Yannick Moy
[Ada] Proof of System
.
Val_Util util
i
ti
e
s for 'Val
u
e
.
.
.
commit
|
commitdiff
|
tree
2021-12-02
Yanni
c
k Moy
[Ada] Pr
o
of of B
o
olean'Image
a
nd Boolean'V
a
l
u
e
commit
|
commitdiff
|
tree
2021-12-01
Y
anni
c
k Moy
[Ada] Improve error messages for dot
n
otati
o
n when
.
.
.
commit
|
commitdiff
|
tree
2021-12-01
Yannick Mo
y
[Ada] Add q
u
ery for extended pr
e
cision f
l
oating-po
i
nt
.
.
.
commit
|
commitdiff
|
tree
2021-12-01
Y
annic
k
Moy
[Ada] Imp
r
ov
e
mess
a
ges on incorrect state refinement
.
.
.
commit
|
commitdiff
|
tree
2021-11-10
Yannick Moy
[Ad
a
] Create explicit ghost mi
r
ror uni
t
for big integers
commit
|
commitdiff
|
tree
2021-11-10
Yan
n
ick Moy
[
A
da] Better er
r
or me
s
sage on mi
s
sin
g
p
arentheses
commit
|
commitdiff
|
tree
2021-11-09
Yannick Moy
[
A
d
a] Compl
e
t
e supp
o
rt fo
r
prefixed call
on subtyp
e
s
.
.
.
commit
|
commitdiff
|
tree
next