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
812a7bc4
Commit
812a7bc4
authored
3 years ago
by
Virgile Prevosto
Browse files
Options
Downloads
Patches
Plain Diff
[C translation] preliminary options for obtaining reparseable output
parent
3a8151b5
No related branches found
No related tags found
No related merge requests found
Changes
3
Hide whitespace changes
Inline
Side-by-side
Showing
3 changed files
frama_Clang_option.ml
+8
-0
8 additions, 0 deletions
frama_Clang_option.ml
frama_Clang_option.mli
+4
-0
4 additions, 0 deletions
frama_Clang_option.mli
frama_Clang_register.ml
+15
-4
15 additions, 4 deletions
frama_Clang_register.ml
with
27 additions
and
4 deletions
frama_Clang_option.ml
+
8
−
0
View file @
812a7bc4
...
@@ -52,6 +52,7 @@ module Clang_extra_args =
...
@@ -52,6 +52,7 @@ module Clang_extra_args =
module
Unmangling
:
module
Unmangling
:
sig
sig
val
add_hook_on_update
:
(
unit
->
unit
)
->
unit
val
set
:
string
->
unit
val
set
:
string
->
unit
val
get
:
unit
->
string
val
get
:
unit
->
string
val
clear
:
unit
->
unit
val
clear
:
unit
->
unit
...
@@ -66,6 +67,7 @@ end
...
@@ -66,6 +67,7 @@ end
let
name
=
"Unmangling"
let
name
=
"Unmangling"
let
default
()
=
"short"
let
default
()
=
"short"
end
)
end
)
let
add_hook_on_update
f
=
Rep
.
add_hook_on_update
(
fun
_
->
f
()
)
let
available_opt
=
Hashtbl
.
create
7
let
available_opt
=
Hashtbl
.
create
7
let
set
s
=
if
Hashtbl
.
mem
available_opt
s
then
Rep
.
set
s
let
set
s
=
if
Hashtbl
.
mem
available_opt
s
then
Rep
.
set
s
let
clear
()
=
Rep
.
clear
()
let
clear
()
=
Rep
.
clear
()
...
@@ -113,6 +115,12 @@ let () =
...
@@ -113,6 +115,12 @@ let () =
UnmanglingShort
.
add_set_hook
(
add_unmangling_option
"short"
);
UnmanglingShort
.
add_set_hook
(
add_unmangling_option
"short"
);
UnmanglingNo
.
add_set_hook
(
add_unmangling_option
"id"
);
UnmanglingNo
.
add_set_hook
(
add_unmangling_option
"id"
);
module
ParseableOutput
=
False
(
struct
let
option_name
=
"-cxx-parseable-output"
let
help
=
"set up Frama-C pretty-printer to output C code that can be reparsed by Frama-C"
end
)
module
C_std_headers
=
module
C_std_headers
=
String
(
String
(
struct
struct
...
...
This diff is collapsed.
Click to expand it.
frama_Clang_option.mli
+
4
−
0
View file @
812a7bc4
...
@@ -30,11 +30,15 @@ module Clang_extra_args: Parameter_sig.String_list
...
@@ -30,11 +30,15 @@ module Clang_extra_args: Parameter_sig.String_list
(** state of the demangling options. *)
(** state of the demangling options. *)
module
Unmangling
:
module
Unmangling
:
sig
sig
val
add_hook_on_update
:
(
unit
->
unit
)
->
unit
val
set
:
string
->
unit
val
set
:
string
->
unit
val
get_val
:
unit
->
(
string
->
string
)
val
get_val
:
unit
->
(
string
->
string
)
val
register_mangling_func
:
string
->
(
string
->
string
)
->
unit
val
register_mangling_func
:
string
->
(
string
->
string
)
->
unit
end
end
(** -cxx-parseable-output *)
module
ParseableOutput
:
Parameter_sig
.
Bool
(** -cxx-cstdlib-path option *)
(** -cxx-cstdlib-path option *)
module
C_std_headers
:
Parameter_sig
.
String
module
C_std_headers
:
Parameter_sig
.
String
...
...
This diff is collapsed.
Click to expand it.
frama_Clang_register.ml
+
15
−
4
View file @
812a7bc4
...
@@ -127,14 +127,25 @@ end
...
@@ -127,14 +127,25 @@ end
(* we avoid any side effect on the kernel unless we are parsing explicitly
(* we avoid any side effect on the kernel unless we are parsing explicitly
a C++ file. *)
a C++ file. *)
let
is_cxx_printer_initialized
=
ref
false
let
init_cxx_printer
()
=
if
not
!
is_cxx_printer_initialized
then
begin
is_cxx_printer_initialized
:=
true
;
Cil_printer
.
register_shallow_attribute
Convert
.
fc_implicit_attr
;
Cil_printer
.
register_shallow_attribute
Convert
.
fc_pure_template_decl_attr
;
Printer
.
update_printer
(
module
Cxx_printer
);
end
let
()
=
Frama_Clang_option
.
Unmangling
.
add_hook_on_update
init_cxx_printer
let
is_initialized
=
ref
false
let
is_initialized
=
ref
false
let
init_cxx_normalization
()
=
let
init_cxx_normalization
()
=
if
not
!
is_initialized
then
begin
if
not
!
is_initialized
then
begin
is_initialized
:=
true
;
is_initialized
:=
true
;
Cil_printer
.
register_shallow_attribute
Convert
.
fc_implicit_attr
;
init_cxx_printer
()
;
Cil_printer
.
register_shallow_attribute
Convert
.
fc_pure_template_decl_attr
;
Printer
.
update_printer
(
module
Cxx_printer
);
(* enable exception removal unless it has explicitely been set to false
(* enable exception removal unless it has explicitely been set to false
on the command line.
on the command line.
*)
*)
...
@@ -145,7 +156,7 @@ let init_cxx_normalization () =
...
@@ -145,7 +156,7 @@ let init_cxx_normalization () =
(* C++ allows this *)
(* C++ allows this *)
Cil
.
set_acceptEmptyCompinfo
()
Cil
.
set_acceptEmptyCompinfo
()
end
end
let
parse_cxx
file
=
let
parse_cxx
file
=
init_cxx_normalization
()
;
init_cxx_normalization
()
;
Frama_Clang_option
.
feedback
Frama_Clang_option
.
feedback
...
...
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