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: Remove references to Might_Not_Return and Always_Return
2023-06-20
Cla
i
re Dross
ada:
Remove
r
eferences to Might
_
N
o
t
_
Return an
d
Alw
a
ys_Retu
r
n
commit
|
commitdiff
|
tree
2023-05-23
C
l
aire
Dross
a
d
a: Update
g
host co
d
e for proof of integer i
n
put funct
i
ons
commit
|
commitdiff
|
tree
2023-05-22
C
l
aire Dross
ad
a
:
S
upport calls th
r
oug
h
d
e
referen
c
es in Fi
n
d_Actual
commit
|
commitdiff
|
tree
2023-05-15
Claire Dross
ada: Fix
p
r
o
of of
r
untime uni
t
S
ys
t
em
.
Value*
commit
|
commitdiff
|
tree
2022-11-28
Clair
e
Dross
ada
:
A
n
notate GNAT
.
Source
_
Info with an abstract
s
tate
commit
|
commitdiff
|
tree
2022-09-02
Claire
D
r
oss
[A
d
a] Add loop variant
s
to Ada
.
Strings
.
Search and A
d
a
.
.
.
commit
|
commitdiff
|
tree
2022-09-02
Claire
Dross
[Ada]
F
ix pro
o
f of ru
n
time unit Syst
e
m
.
Exp_M
o
d
commit
|
commitdiff
|
tree
2022-09-02
Claire
D
r
oss
[A
d
a] Fix pr
o
of of runti
m
e u
n
it System
.
Wid_*
commit
|
commitdiff
|
tree
2022-09-02
Claire D
r
o
s
s
[Ada] Fix proof
o
f runtime unit S
y
s
t
em
.
Value* and
S
yste
m
.
.
.
commit
|
commitdiff
|
tree
2022-07-04
Claire Dross
[A
d
a] Upda
t
e the documen
t
ation of fun
c
tional containers
commit
|
commitdiff
|
tree
2022-07-04
Claire Dross
[Ada]
A
dd GNAT specif
i
c
pragmas to
t
he equivalent Assert
i
on
_
.
.
.
commit
|
commitdiff
|
tree
2022-06-02
C
lai
r
e Dro
s
s
[Ada] Renam
e
G
N
ATprove annota
t
e pragma for
termination
.
.
.
commit
|
commitdiff
|
tree
2022-06-02
Cl
a
i
r
e Dross
[
Ada] Fix
iteration on formal
v
e
ctors
commit
|
commitdiff
|
tree
2022-05-19
Claire Dross
[
Ada]
F
ix proof of
runtime
u
nit a-strfix an
d
a-strs
u
p
commit
|
commitdiff
|
tree
2022-05-18
Clai
r
e Dross
[Ada
]
Fix pr
o
of of run
t
im
e
u
nit s-imageu
commit
|
commitdiff
|
tree
2022-05-18
Claire Dros
s
[Ada] Fix proof of runt
i
me unit
s
-va
l
eu
commit
|
commitdiff
|
tree
2022-05-10
Claire
D
r
oss
[Ada] Accept Structural in aspe
c
t S
u
bpr
o
gram_Variant
.
.
.
commit
|
commitdiff
|
tree
2022-05-10
Claire Dross
[
Ada]
P
roof of
S
yst
e
m
.
V
a
l_Int at gol
d
l
evel
commit
|
commitdiff
|
tree
2022-01-11
Claire
D
ross
[A
d
a]
P
roof of System
.
V
al_Uns at g
o
ld leve
l
commit
|
commitdiff
|
tree
2022-01-05
Claire Dross
[A
d
a] Introduce expr
e
ssion f
u
nctions
for c
o
ntra
c
t
of
.
.
.
commit
|
commitdiff
|
tree
2021-10-05
Clai
r
e
D
ross
[Ada] Disable contrac
t
cases on form
a
l c
o
n
t
a
iners
commit
|
commitdiff
|
tree
2021-09-20
Claire Dro
s
s
[Ada
]
Add
S
PARK_Mode =
>
Of
f
to Sys
t
em
.
File_C
o
nt
r
ol_Block
commit
|
commitdiff
|
tree
2021-07-05
Clai
r
e Dross
[A
d
a] Add Refere
n
ce and Constant_R
e
ference functions
.
.
.
commit
|
commitdiff
|
tree
2021-06-29
Claire Dross
[Ada
]
D
i
sable
Pre/P
o
st in formal containers
commit
|
commitdiff
|
tree
2021-05-07
C
l
aire Dross
[Ada
]
Mo
v
e H
a
s
_
In
f
erable_Discriminants to Sem_Util
commit
|
commitdiff
|
tree
2020-10-21
Clai
r
e Dross
[Ada] Raise Capacity_Error o
n
f
o
r
mal vector insertion
commit
|
commitdiff
|
tree
2020-10-20
Claire Dross
[Ada] Make
at
t
ribute Update an obsolescent feature
commit
|
commitdiff
|
tree
2020-06-18
Clai
r
e Dross
[Ada] T
h
e def
i
nition of
constan
t
s in
d
eclare e
x
press
i
o
ns
.
.
.
2020-06-18 Claire Dross <
dross@adacore.com
>
commit
|
commitdiff
|
tree
2020-06-08
Cla
i
re Dross
[Ad
a
]
Silence
s
purious w
a
r
n
i
ng on instances of fo
r
m
a
l
.
.
.
2020-06-08 Claire Dross <
dross@adacore.com
>
commit
|
commitdiff
|
tree
2020-06-08
Clai
r
e Dross
[Ad
a
] Add Dep
e
nds contr
a
cts
to Delete
p
roce
d
ures of
.
.
.
2020-06-08 Claire Dross <
dross@adacore.com
>
commit
|
commitdiff
|
tree
2019-12-12
Clair
e
Dr
o
s
s
[Ada] Use cor
r
ect su
b
type for call to Last
in formal
.
.
.
2019-12-12 Claire Dross <
dross@adacore.com
>
commit
|
commitdiff
|
tree
2019-09-18
Claire Dros
s
[Ada] F
a
ctor out co
d
e for deciding s
t
atically known
.
.
.
2019-09-18 Claire Dross <
dross@adacore.com
>
commit
|
commitdiff
|
tree
2019-09-18
Claire Dross
[
Ada] Fix style
issues
in fun
c
tional map
s
2019-09-18 Claire Dross <
dross@adacore.com
>
commit
|
commitdiff
|
tree
2019-09-17
Claire
D
ross
[
Ada]
A
d
d Remove primiti
v
e
o
n functi
o
n
al ma
p
s
2019-09-17 Claire Dross <
dross@adacore.com
>
commit
|
commitdiff
|
tree
2019-09-17
Clair
e
Dross
[Ada] Suppor
t
chained cal
l
s
t
o
t
raver
s
al functions
.
.
.
2019-09-17 Claire Dross <
dross@adacore.com
>
commit
|
commitdiff
|
tree
2019-08-21
Cla
i
re
D
r
oss
[Ada] Allow for of iterati
o
n on formal vector
s
2019-08-21 Claire Dross <
dross@adacore.com
>
commit
|
commitdiff
|
tree
2019-08-19
Claire Dross
[Ada]
Allow rea
d
ing a b
o
r
rowed object inside a call
.
.
.
2019-08-19 Claire Dross <
dross@adacore.com
>
commit
|
commitdiff
|
tree
2019-08-13
Clai
r
e
Dr
o
s
s
[Ada]
E
xtend range type in search primitives of formal
.
.
.
2019-08-13 Claire Dross <
dross@adacore.com
>
commit
|
commitdiff
|
tree
2019-07-11
Claire Dross
[Ada
]
Refactor own
e
rsh
i
p
po
i
n
t
er
checking in
S
PARK
.
.
.
2019-07-11 Claire Dross <
dross@adacore.com
>
commit
|
commitdiff
|
tree
2019-07-11
Claire
Dross
[Ada] Memory corruption when
u
sing
f
ormal hashed
s
ets
.
.
.
2019-07-11 Claire Dross <
dross@adacore.com
>
commit
|
commitdiff
|
tree
2019-07-10
C
laire Dro
s
s
[Ada] Fix possible cras
h
es
in GNATprove analysis of
.
.
.
2019-07-10 Claire Dross <
dross@adacore.com
>
commit
|
commitdiff
|
tree
2019-07-05
Claire Dros
s
[Ad
a
] Ada
.
Containers
.
Formal_Vectors:
m
ake v
e
cto
r
s
always
.
.
.
2019-07-05 Claire Dross <
dross@adacore.com
>
commit
|
commitdiff
|
tree
2018-10-09
Claire Dross
[Ada] Fu
n
ctional_Vectors
:
remove def
a
u
l
t value for
.
.
.
2018-10-09 Claire Dross <
dross@adacore.com
>
commit
|
commitdiff
|
tree
2018-05-28
Claire Dr
o
ss
[
A
d
a
] Allow for GNATprove specific versi
o
ns of routines
.
.
.
2018-05-28 Claire Dross <
dross@adacore.com
>
commit
|
commitdiff
|
tree
2017-04-27
Cl
a
ire Dros
s
a-cforma
.
adb,
[
.
.
.
] (=
)
:
Generic p
a
rameter r
e
m
oved
.
.
.
2017-04-27 Claire Dross <
dross@adacore.com
>
commit
|
commitdiff
|
tree
2017-04-27
Claire Dross
a-cofuba
.
a
ds (Add
)
: Take as a
n
additiona
l
input parameter
.
.
.
2017-04-27 Claire Dross <
dross@adacore.com
>
commit
|
commitdiff
|
tree
2017-01-23
Clair
e
Dross
exp_spark
.
ad
b
(Expand_SPARK_Attr
i
but
e
_Ref
e
renc
e
)
: Fo
r
.
.
.
2017-01-23 Claire Dross <
dross@adacore.com
>
commit
|
commitdiff
|
tree
2017-01-19
Claire Dros
s
exp_ch
7
.
adb (
B
u
i
l
d
_Invariant_Pro
c
edure_
B
ody
)
: Semi
.
.
.
2017-01-19 Claire Dross <
dross@adacore.com
>
commit
|
commitdiff
|
tree
