From 812a7bc4799cea0032840292503c31e385b7d511 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Mon, 31 Jan 2022 17:48:55 +0100
Subject: [PATCH] [C translation] preliminary options for obtaining reparseable
output
---
frama_Clang_option.ml | 8 ++++++++
frama_Clang_option.mli | 4 ++++
frama_Clang_register.ml | 19 +++++++++++++++----
3 files changed, 27 insertions(+), 4 deletions(-)
diff --git a/frama_Clang_option.ml b/frama_Clang_option.ml
index 12405a98..da1bb319 100644
--- a/frama_Clang_option.ml
+++ b/frama_Clang_option.ml
@@ -52,6 +52,7 @@ module Clang_extra_args =
module Unmangling:
sig
+ val add_hook_on_update: (unit -> unit) -> unit
val set: string -> unit
val get: unit -> string
val clear: unit -> unit
@@ -66,6 +67,7 @@ end
let name = "Unmangling"
let default () = "short"
end)
+ let add_hook_on_update f = Rep.add_hook_on_update (fun _ -> f ())
let available_opt = Hashtbl.create 7
let set s = if Hashtbl.mem available_opt s then Rep.set s
let clear () = Rep.clear ()
@@ -113,6 +115,12 @@ let () =
UnmanglingShort.add_set_hook (add_unmangling_option "short");
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 =
String(
struct
diff --git a/frama_Clang_option.mli b/frama_Clang_option.mli
index 387872fc..75c4b4d1 100644
--- a/frama_Clang_option.mli
+++ b/frama_Clang_option.mli
@@ -30,11 +30,15 @@ module Clang_extra_args: Parameter_sig.String_list
(** state of the demangling options. *)
module Unmangling:
sig
+ val add_hook_on_update: (unit -> unit) -> unit
val set: string -> unit
val get_val: unit -> (string -> string)
val register_mangling_func: string -> (string->string) -> unit
end
+(** -cxx-parseable-output *)
+module ParseableOutput: Parameter_sig.Bool
+
(** -cxx-cstdlib-path option *)
module C_std_headers: Parameter_sig.String
diff --git a/frama_Clang_register.ml b/frama_Clang_register.ml
index b277f812..e98a6524 100644
--- a/frama_Clang_register.ml
+++ b/frama_Clang_register.ml
@@ -127,14 +127,25 @@ end
(* we avoid any side effect on the kernel unless we are parsing explicitly
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 init_cxx_normalization () =
if not !is_initialized then begin
is_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);
+ init_cxx_printer ();
(* enable exception removal unless it has explicitely been set to false
on the command line.
*)
@@ -145,7 +156,7 @@ let init_cxx_normalization () =
(* C++ allows this *)
Cil.set_acceptEmptyCompinfo ()
end
-
+
let parse_cxx file =
init_cxx_normalization ();
Frama_Clang_option.feedback
--
GitLab