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 renaming of predefined equality operator for unchecked union types
2023-06-27
Claire Dr
o
ss
ada: Correct the contract of Ada
.
T
e
xt_IO
.
Get_Line
commit
|
commitdiff
|
tree
2023-06-20
Claire Dross
ad
a
: R
e
move r
e
ferences to Might_Not_Return and
A
lways_Return
commit
|
commitdiff
|
tree
2023-05-23
C
l
aire Dross
ada: Update ghost
code f
o
r p
r
o
of
of
integer inpu
t
functions
commit
|
commitdiff
|
tree
2023-05-22
C
lair
e
Dross
ad
a
:
S
upport calls
t
hrough dereferences in Fin
d
_
A
ctual
commit
|
commitdiff
|
tree
2023-05-15
C
l
air
e
Dross
ada: Fix proo
f
of runtim
e
unit
System
.
Value
*
commit
|
commitdiff
|
tree
2022-11-28
Claire Dross
ada: A
n
notate GNAT
.
Source_Info with an abstract
state
commit
|
commitdiff
|
tree
2022-09-02
Claire Dross
[A
d
a
]
Ad
d
loop variants to Ad
a
.
Strings
.
S
e
a
rch an
d
Ada
.
.
.
commit
|
commitdiff
|
tree
2022-09-02
C
laire Dross
[Ada] Fix proof of runtime unit System
.
Exp_Mod
commit
|
commitdiff
|
tree
2022-09-02
Claire Dro
s
s
[Ada
]
F
i
x proof
of runtime unit
System
.
W
id_*
commit
|
commitdiff
|
tree
2022-09-02
Claire Dro
s
s
[Ada
]
Fix proof of runtime unit S
y
s
t
em
.
V
a
lue* and Sys
t
em
.
.
.
commit
|
commitdiff
|
tree
2022-07-04
Claire
D
r
o
ss
[Ada] Update th
e
documenta
t
ion
o
f
f
u
n
ctional contai
n
er
s
commit
|
commitdiff
|
tree
2022-07-04
Claire Dr
o
ss
[
Ada
]
Add GNAT specific pragm
a
s to the equivalent Assertion_
.
.
.
commit
|
commitdiff
|
tree
2022-06-02
Claire Dross
[Ada] Re
n
am
e
GNATp
r
ove annotat
e
p
r
a
g
ma for
t
ermination
.
.
.
commit
|
commitdiff
|
tree
2022-06-02
Claire Dro
s
s
[Ada] Fix
it
e
ration on formal vectors
commit
|
commitdiff
|
tree
2022-05-19
C
l
aire
Dross
[Ada]
Fix pro
o
f of
runtime unit a-str
f
ix a
n
d a-strs
u
p
commit
|
commitdiff
|
tree
2022-05-18
Claire Dross
[Ada] Fix proof of runtim
e
unit s-ima
g
eu
commit
|
commitdiff
|
tree
2022-05-18
C
laire D
r
o
s
s
[Ada
]
Fix proof
of run
t
ime unit s-valeu
commit
|
commitdiff
|
tree
2022-05-10
Claire Dross
[Ada] Accept Structura
l
in asp
e
ct Subprogram_V
a
r
iant
.
.
.
commit
|
commitdiff
|
tree
2022-05-10
Claire
D
r
oss
[Ada] Proof
o
f
S
ystem
.
Va
l
_Int at gol
d
level
commit
|
commitdiff
|
tree
2022-01-11
Claire Dross
[Ada]
P
roof o
f
S
ystem
.
Val_Uns at gold level
commit
|
commitdiff
|
tree
2022-01-05
C
l
aire Dro
s
s
[
A
da] Introd
u
c
e
e
x
pression functions for co
n
tr
a
ct of
.
.
.
commit
|
commitdiff
|
tree
2021-10-05
Clair
e
Dross
[
A
da] Disab
l
e
c
o
n
tract cases on formal co
n
tain
e
rs
commit
|
commitdiff
|
tree
2021-09-20
Claire Dross
[Ada] Add SPARK_Mode => Off to
Syst
e
m
.
Fi
l
e
_Contro
l
_Block
commit
|
commitdiff
|
tree
2021-07-05
Claire Dross
[A
d
a] Add Reference and Consta
n
t_Re
f
erence functions
.
.
.
commit
|
commitdiff
|
tree
2021-06-29
Cla
i
r
e
Dro
s
s
[
A
d
a
] Disable
Pre/P
o
st i
n
form
a
l con
t
ainers
commit
|
commitdiff
|
tree
2021-05-07
Cla
i
re Dross
[Ada] Move Has
_
I
nferable_Disc
r
i
m
inants to Sem_Util
commit
|
commitdiff
|
tree
2020-10-21
Claire
Dros
s
[Ada] Raise
C
a
pa
c
ity_Er
r
or on
f
o
rmal vector inser
t
io
n
commit
|
commitdiff
|
tree
2020-10-20
Cla
i
r
e
Dross
[Ada] Make attribute Updat
e
a
n
obsolescent f
e
ature
commit
|
commitdiff
|
tree
2020-06-18
Claire Dross
[Ada] The definition of constants in
declare
e
xpression
s
.
.
.
2020-06-18
Claire Dross
<dross@adacore.com>
commit
|
commitdiff
|
tree
2020-06-08
Claire Dross
[Ada]
S
ilence
s
p
u
r
i
ous warni
n
g on
i
nstances of formal
.
.
.
2020-06-08
Claire Dross
<dross@adacore.com>
commit
|
commitdiff
|
tree
2020-06-08
Claire Dross
[Ada] Add
D
epends contr
a
cts to
D
e
l
et
e
p
rocedure
s
of
.
.
.
2020-06-08
Claire Dross
<dross@adacore.com>
commit
|
commitdiff
|
tree
2019-12-12
C
laire Dross
[A
d
a]
U
se correct subtype
f
o
r call to La
s
t
in
f
ormal
.
.
.
2019-12-12
Claire Dross
<dross@adacore.com>
commit
|
commitdiff
|
tree
2019-09-18
Claire
D
ros
s
[Ada] Factor out co
d
e
for deciding statica
l
ly known
.
.
.
2019-09-18
Claire Dross
<dross@adacore.com>
commit
|
commitdiff
|
tree
2019-09-18
Claire Dross
[Ada
]
Fix style issues in functional m
a
ps
2019-09-18
Claire Dross
<dross@adacore.com>
commit
|
commitdiff
|
tree
2019-09-17
Cla
i
re Dross
[Ad
a
]
A
dd Remov
e
primitive on functional maps
2019-09-17
Claire Dross
<dross@adacore.com>
commit
|
commitdiff
|
tree
2019-09-17
Clai
r
e Dross
[Ada] S
u
p
port c
h
a
ined calls to trave
r
sal
functions
.
.
.
2019-09-17
Claire Dross
<dross@adacore.com>
commit
|
commitdiff
|
tree
2019-08-21
Cl
a
ire Dross
[Ada] Allow for of iteration on fo
r
mal vect
o
rs
2019-08-21
Claire Dross
<dross@adacore.com>
commit
|
commitdiff
|
tree
2019-08-19
Claire Dross
[Ada] Allow reading a borrowed ob
j
ect i
n
s
i
de a call
.
.
.
2019-08-19
Claire Dross
<dross@adacore.com>
commit
|
commitdiff
|
tree
2019-08-13
Claire Dross
[Ada] Exte
n
d range type
i
n
search
p
r
imitives of form
a
l
.
.
.
2019-08-13
Claire Dross
<dross@adacore.com>
commit
|
commitdiff
|
tree
2019-07-11
Claire Dross
[
A
d
a] Refa
c
t
or ownership pointer checki
n
g in
S
PARK
.
.
.
2019-07-11
Claire Dross
<dross@adacore.com>
commit
|
commitdiff
|
tree
2019-07-11
Cla
i
r
e Dro
s
s
[
A
da] Me
m
ory co
r
ruption when using form
a
l hashed sets
.
.
.
2019-07-11
Claire Dross
<dross@adacore.com>
commit
|
commitdiff
|
tree
2019-07-10
Claire Dross
[Ada] Fix possible crash
e
s in GNATpro
v
e analysis of
.
.
.
2019-07-10
Claire Dross
<dross@adacore.com>
commit
|
commitdiff
|
tree
2019-07-05
Claire Dross
[Ada] Ada
.
Containers
.
F
ormal
_
Vectors: make vectors always
.
.
.
2019-07-05
Claire Dross
<dross@adacore.com>
commit
|
commitdiff
|
tree
2018-10-09
Claire D
r
oss
[
A
d
a] F
u
n
ctio
n
al_Vector
s
: remove defau
l
t valu
e
for
.
.
.
2018-10-09
Claire Dross
<dross@adacore.com>
commit
|
commitdiff
|
tree
2018-05-28
Cl
a
ire
Dross
[A
d
a] Allo
w
for GNATprove speci
f
ic
versions
o
f routines
.
.
.
2018-05-28
Claire Dross
<dross@adacore.com>
commit
|
commitdiff
|
tree
2017-04-27
Clai
r
e Dross
a-c
f
o
r
m
a
.
a
d
b
,
[
.
.
.
]
(=):
G
ener
i
c pa
r
ameter r
e
moved
.
.
.
2017-04-27
Claire Dross
<dross@adacore.com>
commit
|
commitdiff
|
tree
2017-04-27
Claire Dro
s
s
a-cofuba
.
ads (A
d
d
): T
a
ke as an a
d
ditional input
p
aramete
r
.
.
.
2017-04-27
Claire Dross
<dross@adacore.com>
commit
|
commitdiff
|
tree
2017-01-23
Claire Dross
exp_spark
.
adb (Exp
a
nd_SP
A
R
K_At
t
r
ibute_Referen
c
e): F
o
r
.
.
.
2017-01-23
Claire Dross
<dross@adacore.com>
commit
|
commitdiff
|
tree
2017-01-19
Claire Dross
exp_ch7
.
adb (Build_Invariant_Proced
u
re_Bo
d
y): Semi
.
.
.
2017-01-19
Claire Dross
<dross@adacore.com>
commit
|
commitdiff
|
tree