Skip to content
GitLab
Explore
Sign in
Primary navigation
Search or go to…
Project
F
Frama Clang
Manage
Activity
Members
Labels
Plan
Issues
Issue boards
Milestones
Wiki
Code
Merge requests
Repository
Branches
Commits
Tags
Repository graph
Compare revisions
Snippets
Deploy
Releases
Package Registry
Container Registry
Model registry
Operate
Terraform modules
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 Clang
Commits
e50d9d75
Commit
e50d9d75
authored
2 years ago
by
Allan Blanchard
Browse files
Options
Downloads
Patches
Plain Diff
No more Extlib.swap, Extlib.opt_fold, Extlib.filter_map
parent
5b6794aa
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
convert.ml
+35
-35
35 additions, 35 deletions
convert.ml
convert_acsl.ml
+2
-2
2 additions, 2 deletions
convert_acsl.ml
with
37 additions
and
37 deletions
convert.ml
+
35
−
35
View file @
e50d9d75
...
...
@@ -91,7 +91,7 @@ let cv_to_attr = function
let
rec
protect_array_type
al
dim
d
=
match
d
with
|
JUSTBASE
->
ARRAY
(
d
,
al
,
dim
)
|
PARENTYPE
(
al1
,
d'
,
al2
)
->
|
PARENTYPE
(
al1
,
d'
,
al2
)
->
PARENTYPE
(
al1
,
protect_array_type
al
dim
d'
,
al2
)
|
ARRAY
(
d'
,
al'
,
dim'
)
->
(* array dim of array dim' of d' is d' foo[dim][dim'] *)
...
...
@@ -141,7 +141,7 @@ let make_integral_constant_kind k v =
let
s
=
match
k
with
|
IBool
|
IChar_s
|
ISChar
|
IWChar_s
|
IWSChar
|
IChar_s
|
ISChar
|
IWChar_s
|
IWSChar
|
IChar
|
IWChar
|
IShort
|
IInt
->
""
|
IChar_u
|
IUChar
|
IChar16
|
IChar32
|
IWChar_u
|
IWUChar
|
IUShort
|
IUInt
->
"U"
...
...
@@ -205,7 +205,7 @@ let make_closure_access env id_name is_ref =
let
access
=
MEMBEROFPTR
(
mk_var
env
closure_name
,
id_name
)
in
if
is_ref
then
UNARY
(
MEMOF
,
mk_expr
env
access
)
else
access
let
mk_signature
res_type
param_types
=
let
mk_signature
res_type
param_types
=
{
result
=
res_type
;
parameter
=
param_types
;
variadic
=
false
}
let
mk_arg_decl
ty
name
loc
=
...
...
@@ -268,7 +268,7 @@ let convert_binary kind assgn e1 e2 =
|
BOLogicalAnd
,
AKRValue
->
BINARY
(
AND
,
e1
,
e2
)
|
BOLogicalOr
,
AKRValue
->
BINARY
(
OR
,
e1
,
e2
)
|
BOComma
,
AKRValue
->
COMMA
[
e1
;
e2
]
|
_
,
AKAssign
->
|
_
,
AKAssign
->
Frama_Clang_option
.
fatal
"Binary operator is not supposed to have an assign kind"
...
...
@@ -286,7 +286,7 @@ let is_unary_assign = function
let
rec
make_addrof
e
=
match
e
.
expr_node
with
|
VARIABLE
_
|
INDEX
_
|
MEMBEROF
_
|
MEMBEROFPTR
_
->
|
VARIABLE
_
|
INDEX
_
|
MEMBEROF
_
|
MEMBEROFPTR
_
->
{
e
with
expr_node
=
UNARY
(
ADDROF
,
e
)
}
(* I think this is handled well by cabs2cil. *)
|
QUESTION
_
->
{
e
with
expr_node
=
UNARY
(
ADDROF
,
e
)
}
...
...
@@ -302,7 +302,7 @@ let rec make_addrof e =
|
[]
->
Frama_Clang_option
.
fatal
"Trying to take the address of an empty expression"
|
a
::
l
->
|
a
::
l
->
{
e
with
expr_node
=
COMMA
(
List
.
rev
((
make_addrof
a
)
::
l
))})
|
NOTHING
|
UNARY
_
|
LABELADDR
_
|
BINARY
_
|
CALL
_
|
CONSTANT
_
|
EXPR_SIZEOF
_
|
TYPE_SIZEOF
_
|
EXPR_ALIGNOF
_
|
TYPE_ALIGNOF
_
...
...
@@ -546,9 +546,9 @@ let mk_compound_init env lv typ init =
let
rec
aux_struct
acc
lfields
linit
=
match
lfields
,
linit
with
|
_
,
[]
->
acc
|
[]
,_
->
|
[]
,_
->
Convert_env
.
fatal
env
"Too many initializers for class %a"
env
"Too many initializers for class %a"
Fclang_datatype
.
Qualified_name
.
pretty
(
name
,
tk
)
|
(
fname
,
ftype
)
::
lfields
,
(
what
,
i
)
::
linit
->
assert
(
what
=
NEXT_INIT
);
...
...
@@ -596,7 +596,7 @@ let rec convert_base_type env spec decl typ does_remove_virtual =
|
Int
ISChar
->
(
List
.
map
spec_type
[
Tsigned
;
Tchar
])
@
spec
,
decl
(* TODO: intKindForSize returns a type of exactly 16 bits. There is no
function for providing an ikind of at least 16 bits yet. This should
be added to Cil. Indeed, it could theoretically be possible that
be added to Cil. Indeed, it could theoretically be possible that
intKindForSize 2 fails while there exist types of a strictly
greater size. *)
|
Int
IChar16
->
spec_of_ikind
(
Cil
.
intKindForSize
2
true
)
@
spec
,
decl
...
...
@@ -687,7 +687,7 @@ let rec convert_base_type env spec decl typ does_remove_virtual =
(
fun
d
->
rt_decl
(
PROTO
(
decl
(
protect_ptr_type
attrs
d
)
,
args
,
[]
,
variadic
)))
|
Pointer
(
PStandardMethodPointer
_
)
|
LVReference
(
PStandardMethodPointer
_
)
|
LVReference
(
PStandardMethodPointer
_
)
|
RVReference
(
PStandardMethodPointer
_
)
->
Frama_Clang_option
.
not_yet_implemented
"pointer to member"
|
Pointer
(
PVirtualMethodPointer
_
)
...
...
@@ -695,11 +695,11 @@ let rec convert_base_type env spec decl typ does_remove_virtual =
|
RVReference
(
PVirtualMethodPointer
_
)
->
Frama_Clang_option
.
not_yet_implemented
"pointer to member"
|
Array
a
->
let
is
_array_attribute
=
function
|
SpecCV
_
->
true
|
_
->
fals
e
let
get
_array_
cv_
attribute
=
function
|
SpecCV
_
as
cv
->
Some
(
cv_to_attr
cv
)
|
_
->
Non
e
in
let
attrs
=
Extlib
.
filter_map
is
_array_attribute
cv_to_attr
spec
in
let
attrs
=
List
.
filter_map
get
_array_
cv_
attribute
spec
in
convert_type
env
(
fun
d
->
...
...
@@ -751,7 +751,7 @@ and convert_fptr env s does_remove_virtual =
and
convert_signature
env
l
does_remove_virtual
=
match
l
with
|
[]
->
(* in C++, an empty list is strictly equivalent to (void), i.e. no
(* in C++, an empty list is strictly equivalent to (void), i.e. no
argument at all. In C, a prototype with no argument means that the
arguments are not specified, so that a subsequent declaration could
provides one or more arguments. We thus normalize that to (void) for
...
...
@@ -1156,7 +1156,7 @@ and convert_expr_node ?(drop_temp=false) env aux e does_remove_virtual =
{
eloc
=
Convert_env
.
get_clang_loc
env
;
econtent
=
(
Variable
(
Global
(
Global
{
prequalification
=
List
.
append
origin_name
.
prequalification
[
origin_qualification
];
...
...
@@ -1169,7 +1169,7 @@ and convert_expr_node ?(drop_temp=false) env aux e does_remove_virtual =
let
target_name
,
ttd
=
Convert_env
.
get_class_name_from_pointer
env
target
.
plain_type
in
let
target_qualification
=
let
target_qualification
=
match
ttd
with
|
TStandard
->
QStructOrClass
(
target_name
.
decl_name
)
|
TTemplateInstance
params
->
...
...
@@ -1538,11 +1538,11 @@ and convert_expr_node ?(drop_temp=false) env aux e does_remove_virtual =
match
exp
.
econtent
with
|
Static_call
(
n
,
t
,
(
FKConstructor
_
as
kind
)
,
args
,
tm
,_
)
->
(* clang seems to insert the temporary in the list
of arguments, but only randomly...
of arguments, but only randomly...
Note that the parameter's list never contain the receiver
argument.
*)
let
args
=
let
args
=
if
List
.
length
args
=
List
.
length
t
.
parameter
then
{
eloc
=
exp
.
eloc
;
econtent
=
...
...
@@ -1976,7 +1976,7 @@ and combine_trunc l1 l2 =
and
find_type_list
env
typ
l
=
let
rec
aux
typ
=
match
typ
with
|
Void
|
Int
_
|
Enum
_
|
Float
_
|
Pointer
_
|
Void
|
Int
_
|
Enum
_
|
Float
_
|
Pointer
_
|
LVReference
_
|
RVReference
_
|
Lambda
_
->
Convert_env
.
fatal
env
"Using compound initialization for a scalar value"
|
Array
typ
->
...
...
@@ -2369,7 +2369,7 @@ and convert_statement env st does_remove_virtual =
|
None
->
def
|
Some
stmt
->
SEQUENCE
(
make_stmt
env
def
,
stmt
,
cloc
))
|
_
->
(* We put all these declarations in a special block,
(* We put all these declarations in a special block,
but the initial declaration itself need to stay out of it.
*)
let
def
=
DEFINITION
(
decl
NO_INIT
)
in
...
...
@@ -2623,7 +2623,7 @@ let make_class_decl env name tkind kind inherits fields body has_virtual =
|
Some
inherits
->
List
.
fold_left
(
fun
result
inherits
->
match
inherits
.
is_virtual
with
|
VStandard
->
|
VStandard
->
append_bases
(
Class
.
get_virtual_base_classes
(
inherits
.
base
,
inherits
.
templated_kind
))
result
|
VVirtual
->
...
...
@@ -2635,7 +2635,7 @@ let make_class_decl env name tkind kind inherits fields body has_virtual =
let
virtual_inherited_fields
=
List
.
fold_left
(
fun
result
(
base
,
tb
)
->
let
n
,
t
=
Convert_env
.
typedef_normalize
env
base
tb
in
let
n'
=
let
n'
=
if
Class
.
has_virtual_base_class
(
base
,
tb
)
then
bare_qname
n
else
n
in
(
FIELD
([
SpecType
...
...
@@ -2663,11 +2663,11 @@ let make_class_decl env name tkind kind inherits fields body has_virtual =
has_virtual
||
Convert_env
.
struct_has_virtual
env
(
n
,
t
)
in
match
inherits
.
is_virtual
with
|
VStandard
->
|
VStandard
->
let
n
,
t
=
Convert_env
.
typedef_normalize
env
inherits
.
base
inherits
.
templated_kind
in
let
n'
=
let
n'
=
if
Class
.
has_virtual_base_class
(
inherits
.
base
,
inherits
.
templated_kind
)
then
bare_qname
n
...
...
@@ -2710,7 +2710,7 @@ let make_class_decl env name tkind kind inherits fields body has_virtual =
match
virtual_base_classes
with
|
[]
->
None
,
env
|
_
->
let
bcfields
,
bfields_typ
=
let
bcfields
,
bfields_typ
=
(
List
.
fold_left
create_field
([]
,
[]
)
(
List
.
append
fields
inherited_fields
))
in
...
...
@@ -2907,13 +2907,13 @@ let rec add_bare_to_qualification qualif = match qualif with
|
[
QTemplateInstance
(
name
,
prms
)]
->
[
QTemplateInstance
(
bare_suf
name
,
prms
)]
|
x
::
l
->
x
::
(
add_bare_to_qualification
l
)
(* functions required by the generic implicit body builder to
(* functions required by the generic implicit body builder to
create a given implicit member function. *)
type
implicit_operation
=
type
implicit_operation
=
{
is_copy
:
bool
;
(* is this a copy/move operation or default constructor or destructor *)
get_op
:
Convert_env
.
env
->
bool
->
qualified_name
*
tkind
->
Convert_env
.
env
->
bool
->
qualified_name
*
tkind
->
(
qualified_name
*
signature
)
option
;
add_op
:
Convert_env
.
env
->
bool
->
qualified_name
->
...
...
@@ -3480,7 +3480,7 @@ let add_special_member env name kind rt args =
(
if
d
then
Convert_env
.
add_default_constructor
else
Convert_env
.
add_default_constructor_base
)
env
name
(
signature
l
)
|
FKConstructor
d
,
|
FKConstructor
d
,
_
::
({
arg_type
=
{
plain_type
=
LVReference
(
PDataPointer
t
)
}}
::
l
as
args
)
when
is_own_class
t
&&
List
.
for_all
has_default_value
l
->
(
if
d
then
Convert_env
.
add_copy_constructor
...
...
@@ -3511,7 +3511,7 @@ let add_special_member env name kind rt args =
let
add_arg_names
l
=
let
new_name
idx
=
if
idx
=
-
1
then
"x"
else
"x"
^
(
string_of_int
idx
)
in
List
.
rev
List
.
rev
(
fst
(
List
.
fold_left
(
fun
(
acc
,
idx
)
arg
->
...
...
@@ -3762,10 +3762,10 @@ and convert_class env name tkind kind inherits body has_virtual =
(* implicit definitions might depend on internal defs, in particular in
presence of nested classes that occur as data member of the current class.
*)
let
add_glob
=
Extlib
.
swa
p
Convert_env
.
add_c_global
in
let
add_glob
=
Fun
.
fli
p
Convert_env
.
add_c_global
in
new_env
|>
List
.
fold_right
add_glob
types
|>
Extlib
.
opt_fold
add_glob
bare_decl
|>
Option
.
fold
~
some
:
add_glob
~
none
:
Fun
.
id
bare_decl
|>
add_glob
decl
|>
List
.
fold_right
add_glob
others
|>
List
.
fold_right
add_glob
my_implicits
|>
...
...
@@ -3893,9 +3893,9 @@ let add_glob_temp env defs (def,init_stmt) =
let
is_frama_clang_array_init_name
=
function
|
Implementation
{
decl_name
}
->
let
prefix
=
"__fc_init_array"
in
let
l
=
String
.
length
prefix
in
let
l
=
String
.
length
prefix
in
l
<=
String
.
length
decl_name
&&
String
.
sub
decl_name
0
l
=
prefix
|
Declaration
_
->
false
|
Declaration
_
->
false
(* NB: we should have a loc for the declaration itself
as well as for the body*)
let
rec
convert_global
env
glob
=
...
...
This diff is collapsed.
Click to expand it.
convert_acsl.ml
+
2
−
2
View file @
e50d9d75
...
...
@@ -741,9 +741,9 @@ let rec convert_annot env annot =
let
mangle
name
signature
=
let
name
,
t
=
Convert_env
.
typedef_normalize
env
name
TStandard
in
Mangling
.
mangle
name
t
signature
in
let
read
=
Option
.
map
(
Extlib
.
swa
p
mangle
None
)
let
read
=
Option
.
map
(
Fun
.
fli
p
mangle
None
)
read
in
let
write
=
Option
.
map
(
Extlib
.
swa
p
mangle
None
)
let
write
=
Option
.
map
(
Fun
.
fli
p
mangle
None
)
write
in
LDvolatile
(
mem
,
(
read
,
write
))
,
env
|
Daxiomatic
(
loc
,
s
,
annots
)
->
...
...
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