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 pragma Annotate for GNATcheck exemptions
2023-07-06
Claire Dross
ada: Add
s
pecifica
t
ion source files of
r
untime
u
n
its
commit
|
commitdiff
|
tree
2023-07-06
Claire
Dross
ada: Refactor the
pr
o
o
f
of the
V
a
l
ue and Image runtime
.
.
.
commit
|
commitdiff
|
tree
2023-06-27
Cl
a
ir
e
Dr
o
ss
ada: Correct the contract
o
f Ada
.
Tex
t
_
IO
.
Get_L
i
n
e
commit
|
commitdiff
|
tree
2023-06-20
C
laire
D
ross
ada: Rem
o
ve references to Might_No
t
_Re
t
urn and Always_
R
e
t
u
rn
commit
|
commitdiff
|
tree
2023-05-23
Claire Dross
ada:
Update gho
s
t code for pro
o
f of integer input fu
n
c
t
ions
commit
|
commitdiff
|
tree
2023-05-22
Claire Dross
a
da: Support call
s
throu
g
h dereferences in Find_
A
ctual
commit
|
commitdiff
|
tree
2023-05-15
C
l
a
ire
D
ross
ada: Fi
x
proof of runtime u
n
i
t
System
.
Value*
commit
|
commitdiff
|
tree
2022-11-28
Cla
i
re Dr
o
s
s
ada: A
n
notate GNAT
.
Sourc
e
_Info with an ab
s
t
ract stat
e
commit
|
commitdiff
|
tree
2022-09-02
Clair
e
Dross
[Ada] Add l
o
op
var
i
ants to Ad
a
.
Strings
.
Search and Ada
.
.
.
commit
|
commitdiff
|
tree
2022-09-02
Claire Dross
[Ada]
Fix proof of runtime unit S
y
stem
.
Exp_Mod
commit
|
commitdiff
|
tree
2022-09-02
Claire Dross
[
Ada] Fix
proof
o
f r
u
n
t
ime unit
System
.
Wid_*
commit
|
commitdiff
|
tree
2022-09-02
C
l
aire D
r
oss
[Ada] Fix proof of ru
n
ti
m
e unit
S
y
s
t
e
m
.
Value* and Sys
t
em
.
.
.
commit
|
commitdiff
|
tree
2022-07-04
Claire Dross
[Ada] Update
t
he
d
o
c
umentation
o
f f
u
nc
t
ional c
o
ntainers
commit
|
commitdiff
|
tree
2022-07-04
Claire Dross
[Ada] Add GNA
T
specific pragm
a
s to
t
h
e
equivale
n
t Assertion_
.
.
.
commit
|
commitdiff
|
tree
2022-06-02
C
l
aire
Dross
[Ada] Re
n
ame
GNATprove anno
t
ate p
r
agma for
term
i
n
ation
.
.
.
commit
|
commitdiff
|
tree
2022-06-02
Clair
e
D
r
oss
[Ad
a
]
Fix
i
terati
o
n on formal
ve
c
to
r
s
commit
|
commitdiff
|
tree
2022-05-19
C
l
aire Dross
[Ada
]
Fix
pr
o
of
o
f
runtime unit
a
-strfix
and a-strsup
commit
|
commitdiff
|
tree
2022-05-18
Cl
a
i
r
e D
r
oss
[
A
da] Fix proof
o
f ru
n
time unit
s
-imageu
commit
|
commitdiff
|
tree
2022-05-18
Claire Dross
[
A
da] Fix proof
of runtime u
n
i
t
s
-
v
a
leu
commit
|
commitdiff
|
tree
2022-05-10
Clair
e
Dross
[
Ad
a
] Acc
e
pt Structural
in aspect
S
ubpr
o
gr
a
m_Va
r
i
ant
.
.
.
commit
|
commitdiff
|
tree
2022-05-10
Clair
e
Dross
[
A
da] Proo
f
of S
y
stem
.
Val_Int
at
g
old level
commit
|
commitdiff
|
tree
2022-01-11
Claire
D
ross
[Ada]
P
r
oof of
Sy
s
tem
.
V
a
l_Uns at gold level
commit
|
commitdiff
|
tree
2022-01-05
Claire Dross
[Ada]
I
n
t
roduce exp
r
ession
f
unctions for contract of
.
.
.
commit
|
commitdiff
|
tree
2021-10-05
Claire Dross
[Ada] Disable con
t
r
a
ct c
a
ses on formal cont
a
iners
commit
|
commitdiff
|
tree
2021-09-20
Claire Dross
[
A
da] Add
S
P
A
R
K_Mode => Off to System
.
File_Contr
o
l
_Block
commit
|
commitdiff
|
tree
2021-07-05
Claire Dross
[Ada] Add Reference and
Constant_Reference fu
n
c
tions
.
.
.
commit
|
commitdiff
|
tree
2021-06-29
Clai
r
e Dross
[A
d
a] Dis
a
ble Pre/Post
i
n fo
r
m
a
l containers
commit
|
commitdiff
|
tree
2021-05-07
Claire Dross
[Ada] Mo
v
e Has_Inferable_Discriminants to S
e
m_Util
commit
|
commitdiff
|
tree
2020-10-21
Clair
e
Dross
[Ad
a
] Rais
e
Capacity_Error o
n
formal vector inse
r
t
ion
commit
|
commitdiff
|
tree
2020-10-20
Claire Dross
[A
d
a
]
Mak
e
at
t
ribu
t
e Up
d
at
e
an obsolescent feat
u
re
commit
|
commitdiff
|
tree
2020-06-18
Claire D
r
oss
[
Ada]
T
h
e
definition
o
f constants
in decl
a
re expr
e
ss
i
on
s
.
.
.
2020-06-18
Claire Dross
<dross@adacore.com>
commit
|
commitdiff
|
tree
2020-06-08
Claire Dross
[Ada] Sile
n
ce sp
u
rious
w
arning on i
n
stances of formal
.
.
.
2020-06-08
Claire Dross
<dross@adacore.com>
commit
|
commitdiff
|
tree
2020-06-08
C
l
aire Dros
s
[Ada] Add Depends
c
ontracts to Delete pr
o
cedures of
.
.
.
2020-06-08
Claire Dross
<dross@adacore.com>
commit
|
commitdiff
|
tree
2019-12-12
Claire Dro
s
s
[Ada
]
U
se correct subtype f
o
r call
t
o
L
ast in f
o
r
mal
.
.
.
2019-12-12
Claire Dross
<dross@adacore.com>
commit
|
commitdiff
|
tree
2019-09-18
C
l
aire Dross
[Ada] Factor out co
d
e fo
r
deciding statically known
.
.
.
2019-09-18
Claire Dross
<dross@adacore.com>
commit
|
commitdiff
|
tree
2019-09-18
Claire Dross
[Ada
]
Fix style issues in functi
o
nal
maps
2019-09-18
Claire Dross
<dross@adacore.com>
commit
|
commitdiff
|
tree
2019-09-17
C
l
aire Dross
[Ada] Add Remove primitive on fu
n
ctio
n
a
l
maps
2019-09-17
Claire Dross
<dross@adacore.com>
commit
|
commitdiff
|
tree
2019-09-17
C
laire Dross
[Ada] Sup
p
ort c
h
a
ined ca
l
ls to
t
raver
s
al
f
u
nctions
.
.
.
2019-09-17
Claire Dross
<dross@adacore.com>
commit
|
commitdiff
|
tree
2019-08-21
Claire Dros
s
[Ada]
A
llo
w
for of iteration on form
a
l
v
e
c
tors
2019-08-21
Claire Dross
<dross@adacore.com>
commit
|
commitdiff
|
tree
2019-08-19
Cla
i
re Dross
[Ada]
Allo
w
r
e
adi
n
g a b
o
rrowe
d
object insid
e
a
c
all
.
.
.
2019-08-19
Claire Dross
<dross@adacore.com>
commit
|
commitdiff
|
tree
2019-08-13
Claire Dr
o
ss
[Ada] Ext
e
nd range type
in search primitives of formal
.
.
.
2019-08-13
Claire Dross
<dross@adacore.com>
commit
|
commitdiff
|
tree
2019-07-11
Claire
D
r
oss
[
A
da] Refactor ow
n
ership poi
n
ter checking in SPARK
.
.
.
2019-07-11
Claire Dross
<dross@adacore.com>
commit
|
commitdiff
|
tree
2019-07-11
Claire D
r
o
ss
[
Ada]
M
emory corrupti
o
n when using formal hashed sets
.
.
.
2019-07-11
Claire Dross
<dross@adacore.com>
commit
|
commitdiff
|
tree
2019-07-10
Claire Dro
s
s
[A
d
a] Fix possible
c
r
ash
e
s in GNATprove
analysis of
.
.
.
2019-07-10
Claire Dross
<dross@adacore.com>
commit
|
commitdiff
|
tree
2019-07-05
Claire Dross
[
A
da]
Ad
a
.
Contai
n
er
s
.
Fo
r
mal_Vectors: make vec
t
ors always
.
.
.
2019-07-05
Claire Dross
<dross@adacore.com>
commit
|
commitdiff
|
tree
2018-10-09
Claire Dro
s
s
[Ada] Functi
o
nal_Vecto
r
s: remove
d
e
fault
v
alu
e
f
o
r
.
.
.
2018-10-09
Claire Dross
<dross@adacore.com>
commit
|
commitdiff
|
tree
2018-05-28
C
laire Dross
[Ada] A
l
low for GNATp
r
ov
e
specific versio
n
s
of routines
.
.
.
2018-05-28
Claire Dross
<dross@adacore.com>
commit
|
commitdiff
|
tree
2017-04-27
Claire Dross
a-cfo
r
ma
.
adb,
[
.
.
.
] (=): Gener
i
c p
a
r
ameter removed
.
.
.
2017-04-27
Claire Dross
<dross@adacore.com>
commit
|
commitdiff
|
tree
2017-04-27
Claire Dross
a-cofuba
.
ad
s
(
A
dd): Take as an addi
t
ional i
n
put p
a
r
a
m
eter
.
.
.
2017-04-27
Claire Dross
<dross@adacore.com>
commit
|
commitdiff
|
tree
2017-01-23
Claire D
r
oss
exp_
s
park
.
a
d
b
(Expand_SP
A
RK_A
t
tr
i
b
u
te_Reference): F
o
r
.
.
.
2017-01-23
Claire Dross
<dross@adacore.com>
commit
|
commitdiff
|
tree
2017-01-19
Claire Dross
ex
p
_ch7
.
adb
(
Bui
l
d_I
n
vari
a
nt_Procedure_Body): Semi
.
.
.
2017-01-19
Claire Dross
<dross@adacore.com>
commit
|
commitdiff
|
tree