Skip to content
GitLab
Explore
Sign in
Primary navigation
Search or go to…
Project
F
frama-c
Manage
Activity
Members
Labels
Plan
Issues
Issue boards
Milestones
Wiki
Code
Merge requests
Repository
Branches
Commits
Tags
Repository graph
Compare revisions
Deploy
Releases
Container Registry
Model registry
Monitor
Incidents
Analyze
Value stream analytics
Contributor analytics
Repository analytics
Model experiments
Help
Help
Support
GitLab documentation
Compare GitLab plans
Community forum
Contribute to GitLab
Provide feedback
Keyboard shortcuts
?
Snippets
Groups
Projects
Show more breadcrumbs
pub
frama-c
Commits
ead88f24
Commit
ead88f24
authored
4 years ago
by
Valentin Perrelle
Committed by
Andre Maroneze
4 years ago
Browse files
Options
Downloads
Patches
Plain Diff
[Variadic] Remove unused functions in Extends
parent
d56831b6
No related branches found
Branches containing commit
No related tags found
Tags containing commit
No related merge requests found
Changes
2
Hide whitespace changes
Inline
Side-by-side
Showing
2 changed files
src/plugins/variadic/extends.ml
+5
-168
5 additions, 168 deletions
src/plugins/variadic/extends.ml
src/plugins/variadic/extends.mli
+4
-92
4 additions, 92 deletions
src/plugins/variadic/extends.mli
with
9 additions
and
260 deletions
src/plugins/variadic/extends.ml
+
5
−
168
View file @
ead88f24
...
...
@@ -22,14 +22,7 @@
open
Cil_types
module
Typ
=
struct
let
attributes_less_equal
t1
t2
=
let
t1
=
Cil
.
typeDeepDropAllAttributes
t1
in
let
t2
=
Cil
.
typeDeepDropAllAttributes
t2
in
Cil_datatype
.
Typ
.
equal
t1
t2
let
params
typ
=
match
Cil
.
unrollType
typ
with
|
TFun
(
_
,
args
,_,_
)
->
Cil
.
argsToList
args
...
...
@@ -45,119 +38,29 @@ module Typ = struct
let
params_count
typ
=
List
.
length
(
params
typ
)
let
is_variadic
typ
=
match
Cil
.
unrollType
typ
with
|
TFun
(
_
,
_
,
b
,
_
)
->
b
|
_
->
false
end
module
Cil
=
struct
include
Cil
let
ptrType
typ
=
TPtr
(
typ
,
[]
)
let
constPtrType
typ
=
TPtr
(
typ
,
[
Attr
(
"const"
,
[]
)])
let
shortType
=
TInt
(
IShort
,
[]
)
let
ushortType
=
TInt
(
IUShort
,
[]
)
let
shortPtrType
=
ptrType
shortType
let
ushortPtrType
=
ptrType
ushortType
let
longPtrType
=
ptrType
longType
let
ulongPtrType
=
ptrType
ulongType
let
longlongPtrType
=
ptrType
longLongType
let
ulonglongPtrType
=
ptrType
ulongLongType
let
doublePtrType
=
ptrType
doubleType
let
signedIntegerTypes
=
[
Cil
.
charType
;
shortType
;
Cil
.
intType
;
Cil
.
longType
;
longLongType
]
let
unsignedIntegerTypes
=
[
ucharType
;
ushortType
;
Cil
.
uintType
;
Cil
.
ulongType
;
Cil
.
ulongLongType
]
let
signedIntegerPtrTypes
=
[
Cil
.
charPtrType
;
shortPtrType
;
Cil
.
intPtrType
;
longPtrType
;
longlongPtrType
]
let
unsignedIntegerPtrTypes
=
[
ucharPtrType
;
ushortPtrType
;
Cil
.
uintPtrType
;
ulongPtrType
;
ulonglongPtrType
]
let
signed_integers_ranking
=
Extlib
.
mapi
(
fun
i
t
->
(
t
,
i
))
signedIntegerTypes
let
unsigned_integers_ranking
=
Extlib
.
mapi
(
fun
i
t
->
(
t
,
i
))
unsignedIntegerTypes
let
is_signed_integer_type
t
=
List
.
mem
t
signedIntegerTypes
let
is_unsigned_integer_type
t
=
List
.
mem
t
unsignedIntegerTypes
let
is_integer_type
t
=
is_signed_integer_type
t
||
is_unsigned_integer_type
t
let
is_signed_ptr_integer_type
t
=
List
.
mem
t
signedIntegerPtrTypes
let
is_unsigned_ptr_integer_type
t
=
List
.
mem
t
unsignedIntegerPtrTypes
let
is_integer_ptr_type
t
=
is_signed_ptr_integer_type
t
||
is_unsigned_ptr_integer_type
t
let
integer_ranking_comp
t1
t2
=
let
rt1
,
rt2
=
if
is_signed_integer_type
t1
&&
is_signed_integer_type
t2
then
List
.
assoc
t1
signed_integers_ranking
,
List
.
assoc
t2
signed_integers_ranking
else
if
is_unsigned_integer_type
t1
&&
is_unsigned_integer_type
t2
then
List
.
assoc
t1
unsigned_integers_ranking
,
List
.
assoc
t2
unsigned_integers_ranking
else
raise
(
Invalid_argument
"rank_comp"
)
in
rt1
-
rt2
let
integer_promotion
t1
t2
=
try
(
integer_ranking_comp
t1
t2
)
<
0
with
Invalid_argument
_
->
false
let
is_folded_zero
e
=
Cil
.
isZero
(
Cil
.
constFold
false
e
)
let
is_function
vi
=
match
vi
.
vtype
with
|
TFun
_
->
true
|
_
->
false
let
is_variadic_function
vi
=
Typ
.
is_variadic
vi
.
vtype
let
get_fundec_return_type
fd
=
match
fd
.
svar
.
vtype
with
|
TFun
(
rt
,
_
,
_
,
_
)
->
rt
|
_
->
Options
.
Self
.
fatal
"Varinfo of fundec does not have function type."
let
get_kf_attributes
kf
=
match
kf
.
fundec
with
|
Definition
(
fd
,
_
)
->
fd
.
svar
.
vattr
|
Declaration
(
_
,
vi
,
_
,
_
)
->
vi
.
vattr
let
get_inst_loc
=
Cil_datatype
.
Instr
.
loc
let
get_stmt_loc
=
Cil_datatype
.
Stmt
.
loc
match
Cil
.
unrollType
vi
.
vtype
with
|
TFun
(
_
,
_
,
b
,
_
)
->
b
|
_
->
false
end
module
List
=
struct
include
List
exception
EmptyList
let
rec
make
n
a
=
if
n
<=
0
then
[]
else
a
::
make
(
n
-
1
)
a
let
to_scalar
=
function
|
[
a
]
->
a
|
_
->
failwith
"to_scalar"
let
of_opt
=
function
|
None
->
[]
|
Some
x
->
[
x
]
let
to_opt
=
function
|
[]
->
None
|
[
a
]
->
Some
a
|
_
->
failwith
"to_opt"
let
first
=
function
|
[]
->
failwith
"first"
|
a
::
_
->
a
exception
EmptyList
let
rec
last
=
function
|
[]
->
raise
EmptyList
|
[
a
]
->
a
...
...
@@ -183,36 +86,6 @@ module List = struct
let
l1
,
l2
=
break
(
n
-
1
)
l
in
(
a
::
l1
,
l2
)
let
rec
filter_map
f
=
function
|
[]
->
[]
|
a
::
l
->
match
f
a
with
|
Some
r
->
r
::
filter_map
f
l
|
None
->
filter_map
f
l
let
iteri
f
l
=
let
i
=
ref
0
in
iter
(
fun
a
->
f
!
i
a
;
incr
i
)
l
let
mapi
f
l
=
let
i
=
ref
0
in
map
(
fun
a
->
let
r
=
f
!
i
a
in
incr
i
;
r
)
l
let
rev_mapi
f
l
=
let
i
=
ref
0
in
let
rec
aux
acc
=
function
|
[]
->
acc
|
a
::
l
->
let
a'
=
f
!
i
a
in
incr
i
;
aux
(
a'
::
acc
)
l
in
aux
[]
l
let
iteri2
f
l1
l2
=
let
i
=
ref
0
in
let
rec
aux
l1
l2
=
match
l1
,
l2
with
|
[]
,
[]
->
()
|
a1
::
l1
,
a2
::
l2
->
f
!
i
a1
a2
;
incr
i
;
aux
l1
l2
|
_
,
_
->
invalid_arg
"List.iteri2"
in
aux
l1
l2
let
mapi2
f
l1
l2
=
let
i
=
ref
0
in
let
rec
aux
l1
l2
=
match
l1
,
l2
with
...
...
@@ -222,46 +95,10 @@ module List = struct
in
aux
l1
l2
let
reduce_left
f
l
=
let
rec
aux
acc
=
function
|
[]
->
acc
|
a
::
l
->
aux
(
f
acc
a
)
l
in
match
l
with
|
[]
->
failwith
"reduce"
|
a
::
l
->
aux
a
l
let
rec
reduce_right
f
=
function
|
[]
->
failwith
"reduce"
|
[
a
]
->
a
|
a
::
l
->
f
a
(
reduce_right
f
l
)
let
map_fold_left
f
acc
l
=
let
rec
aux
acc
r
=
function
|
[]
->
List
.
rev
r
,
acc
|
a
::
l
->
let
a
,
acc
=
f
acc
a
in
aux
acc
(
a
::
r
)
l
in
aux
acc
[]
l
let
ifind
f
l
=
let
i
=
ref
0
in
let
rec
aux
=
function
|
[]
->
raise
Not_found
|
a
::
l
->
if
not
(
f
a
)
then
(
incr
i
;
aux
l
)
in
aux
l
;
!
i
let
rec
unique_sorted
cmp
=
function
|
a1
::
a2
::
l
when
cmp
a1
a2
=
0
->
unique_sorted
cmp
(
a2
::
l
)
|
[]
->
[]
|
a
::
l
->
a
::
unique_sorted
cmp
l
let
sort_unique
cmp
l
=
unique_sorted
cmp
(
sort
cmp
l
)
let
replace
i
v
=
Extlib
.
mapi
(
fun
i'
v'
->
if
i
=
i'
then
v
else
v'
)
end
This diff is collapsed.
Click to expand it.
src/plugins/variadic/extends.mli
+
4
−
92
View file @
ead88f24
...
...
@@ -23,124 +23,36 @@
open
Cil_types
module
Typ
:
sig
val
attributes_less_equal
:
typ
->
typ
->
bool
val
params
:
typ
->
(
string
*
typ
*
attributes
)
list
val
ghost_partitioned_params
:
typ
->
(
string
*
typ
*
attributes
)
list
*
(
string
*
typ
*
attributes
)
list
val
params_types
:
typ
->
typ
list
val
params_count
:
typ
->
int
val
is_variadic
:
typ
->
bool
end
module
Cil
:
sig
module
Cil
:
sig
include
module
type
of
Cil
val
ptrType
:
typ
->
typ
val
constPtrType
:
typ
->
typ
val
shortType
:
typ
val
ushortType
:
typ
val
shortPtrType
:
typ
val
ushortPtrType
:
typ
val
longPtrType
:
typ
val
ulongPtrType
:
typ
val
longlongPtrType
:
typ
val
ulonglongPtrType
:
typ
val
doublePtrType
:
typ
val
is_folded_zero
:
exp
->
bool
(** Standard integer types in C99 (Cf. 6.2.5) *)
val
signedIntegerTypes
:
typ
list
val
unsignedIntegerTypes
:
typ
list
val
signedIntegerPtrTypes
:
typ
list
val
unsignedIntegerPtrTypes
:
typ
list
val
is_signed_integer_type
:
typ
->
bool
val
is_unsigned_integer_type
:
typ
->
bool
val
is_integer_type
:
typ
->
bool
val
is_integer_ptr_type
:
typ
->
bool
val
is_function
:
varinfo
->
bool
val
shortType
:
typ
val
ushortType
:
typ
(** @return [true] if varinfo is a variadic function, [false] if it
is a non-variadic function or if it is not a function. *)
val
is_variadic_function
:
varinfo
->
bool
(** Does not use {! Globals.Functions.get} nor
{! Kernel_function.get_return_type}. *)
val
get_fundec_return_type
:
fundec
->
typ
val
get_kf_attributes
:
kernel_function
->
attributes
(** [integer_ranking_comp t1 t2]
@return
[<0] if [t1 < t2]
[0] if [t1 = t2]
[>0] if [t1 > t2]
@raise Invalid_argument if t1 and t2 are not comparable.
*)
val
integer_ranking_comp
:
typ
->
typ
->
int
(** [integer_promotion t1 t2] returns [true] if [t1 < t2] *)
val
integer_promotion
:
typ
->
typ
->
bool
val
get_inst_loc
:
instr
->
location
val
get_stmt_loc
:
stmt
->
location
end
module
List
:
sig
include
module
type
of
List
(* Constructors *)
val
make
:
int
->
'
a
->
'
a
list
exception
EmptyList
(* Get one element *)
val
to_scalar
:
'
a
list
->
'
a
val
of_opt
:
'
a
option
->
'
a
list
val
to_opt
:
'
a
list
->
'
a
option
val
first
:
'
a
list
->
'
a
val
last
:
'
a
list
->
'
a
(** @raise EmptyList when the list is empty. *)
(* Sublists *)
val
make
:
int
->
'
a
->
'
a
list
val
take
:
int
->
'
a
list
->
'
a
list
val
drop
:
int
->
'
a
list
->
'
a
list
val
break
:
int
->
'
a
list
->
'
a
list
*
'
a
list
(* Iterators *)
val
filter_map
:
(
'
a
->
'
b
option
)
->
'
a
list
->
'
b
list
val
iteri
:
(
int
->
'
a
->
unit
)
->
'
a
list
->
unit
val
mapi
:
(
int
->
'
a
->
'
b
)
->
'
a
list
->
'
b
list
val
rev_mapi
:
(
int
->
'
a
->
'
b
)
->
'
a
list
->
'
b
list
val
iteri2
:
(
int
->
'
a
->
'
b
->
unit
)
->
'
a
list
->
'
b
list
->
unit
val
mapi2
:
(
int
->
'
a
->
'
b
->
'
c
)
->
'
a
list
->
'
b
list
->
'
c
list
val
reduce_left
:
(
'
a
->
'
a
->
'
a
)
->
'
a
list
->
'
a
val
reduce_right
:
(
'
a
->
'
a
->
'
a
)
->
'
a
list
->
'
a
val
map_fold_left
:
(
'
b
->
'
a
->
'
c
*
'
b
)
->
'
b
->
'
a
list
->
'
c
list
*
'
b
(* Search *)
val
ifind
:
(
'
a
->
bool
)
->
'
a
list
->
int
(* Sort *)
val
sort_unique
:
(
'
a
->
'
a
->
int
)
->
'
a
list
->
'
a
list
val
unique_sorted
:
(
'
a
->
'
a
->
int
)
->
'
a
list
->
'
a
list
(*
(** [split k l] when [l] = \[e{_1}; ...; e{_n}\].
@return
(\[e{_1}; ...; e{_k}\], \[e{_k+1}; ...; e{_n}\]) if [0 < k < n],
([\[\]], [l]) if [k <= 0],
([l], [\[\]]) if [k >= n] *)
val split : int -> 'a list -> 'a list * 'a list *)
(** [replace i v l] returns a new list where [l.(i)] = [v] *)
val
replace
:
int
->
'
a
->
'
a
list
->
'
a
list
end
This diff is collapsed.
Click to expand it.
Preview
0%
Loading
Try again
or
attach a new file
.
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Save comment
Cancel
Please
register
or
sign in
to comment